+Nat_add n k = case n
- | (succ n) => Nat_add n (succ k)
- | zero => k;
Habituellement, on utilse la forme avec une récursion non-terminale:
Nat_add n k = case n | succ n => succ (Nat_add n k) | zero => k;
pas sûr exactement pourquoi (quoique: voir ci-dessous `len`).
+Nat_eq : Nat -> Nat -> Type; +Nat_eq n k = case (n,k)
- | (succ n,succ k) => Nat_eq n k
- | (zero,zero) => True
- | False;
Je suis content de voir que tu es confortable à construire des types dans une fonction. Mais je crois que cette fonction n'est pas nécessaire.
+type List_n (n : Nat) (a : Type)
- | cons a (List_n sn a) (p ::: (Nat_eq n (succ sn)))
- | nil (p ::: (Nat_eq n zero));
Tu utilises `sn` sans le définir. Plus précisément, tu dois faire:
type List_n (n : Nat) (a : Type) | cons (sn ::: Nat) a (List_n sn a) (p ::: (Nat_eq n (succ sn))) | nil (p ::: (Nat_eq n zero));
Idéalement, tu devrais pouvoir écrire ça comme ça:
type List_n (n : Nat) (a : Type) | cons a (List_n ?sn a) (p ::: (Nat_eq n (succ ?sn))) | nil (p ::: (Nat_eq n zero));
mais j'ai l'impression que c'est pas encore implanté.
Par contre, une autre simplification est que tu devrais pouvoir utiliser `Eq` au lieu de `Nat_eq`.
+len : (n : Nat) ≡> (a : Type) ≡> List_n n a -> Nat; +len xs = case (xs)
- | cons x xs => succ (len xs)
- | nil => zero;
Si tu veux montrer que
∀ l : List_n n α . Eq n (len l)
je pense que la définition de `len` que tu utilises fonctionnera mieux avec l'autre définition de Nat_add (à l'inverse, ta définition de Nat_add fonctionnera mieux avec une définition tail-recursive de `len`).
+%prep : (n : Nat) ≡> a -> List_n n a -> List_n (succ n) a; +%prep x xs = cons (n := (succ n)) x xs (Nat_eq (succ n) (succ n));
^^^^^^^^^^^^^^^^^^^^^^^^^^ devient Eq_refl
-- Stefan