Here's a simple pattern generator that returns a list of 1:nat. lemma_1 proves that there's a 1 in every position of generated lists of arbitrary length. The lng argument for nth_1 had to be introduced because otherwise n would be constrained as n:nat{n < length lst} causing a type conflict with the n in lemma_1 whose type would be n:nat{n < lng}. How could this be solved without the extra parameter?
val length: list 'a -> nat
let rec length lst =
match lst with
| [] -> 0
| _ :: t -> 1 + length t
val nth_1 : lst: list nat {length lst > 0} -> (lng: nat) -> n: nat {n < lng} -> nat
let rec nth_1 lst lng n =
match lst with
| [h] -> h
| h :: t -> if n = 0 then h else nth_1 t (lng - 1) (n - 1)
val gen_1 : lng: nat {lng > 0} -> list nat
let rec gen_1 lng =
match lng with
| 1 -> [1]
| _ -> 1 :: gen_1 (lng - 1)
let rec lemma_1 (lng: nat {lng > 0}) (n: nat {n < lng}) : Lemma ((nth_1 (gen_1 lng) lng n) = 1) =
match n with
| 0 -> ()
| _ -> lemma_1 (lng - 1) (n - 1)
It seems the problem is in connection with the constraint that gen_1 patterns must not be zero length. Is there a better way to express this criterion?
Here is one way to avoid the extra parameter (please see the comments inline):
module Test
val length: list α → ℕ
let rec length lst =
match lst with
| [] → 0
| _ ⸬ t → 1 + length t
//the refinement on n is not really necessary here, the proofs work even without it
//because as soon as we have [h], irrespective of the value of n, we return h
val nth_1 : lst: list ℕ {length lst > 0} → n: ℕ{n < length lst} → ℕ
let rec nth_1 lst n =
match lst with
| [h] → h
| h ⸬ t → if n = 0 then h else nth_1 t (n - 1)
//refine the return type to say that it returns a list of length lng
val gen_1 : lng: pos → (l:list ℕ{length l == lng})
let rec gen_1 lng =
match lng with
| 1 → [1]
| _ → 1 ⸬ gen_1 (lng - 1)
let rec lemma_1 (lng: pos) (n: ℕ {n < lng}) : Lemma ((nth_1 (gen_1 lng) n) = 1) =
match n with
| 0 → ()
| _ → lemma_1 (lng - 1) (n - 1)