[Git][monnier/typer][graveline] samples/list_n.typer, there must be some mistakes
Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 46381fd8 by Jonathan Graveline at 2018-06-25T18:11:36Z samples/list_n.typer, there must be some mistakes - - - - - 1 changed file: - + samples/list_n.typer Changes: ===================================== samples/list_n.typer ===================================== @@ -0,0 +1,37 @@ +%%% +%%% Size proved list : n_list +%%% + +Nat : Type; + +type Nat + | zero + | succ Nat; + +Nat_add : Nat -> Nat -> Nat; + +Nat_add n k = case n + | (succ n) => Nat_add n (succ k) + | zero => k; + +Nat_eq : Nat -> Nat -> Type; +Nat_eq n k = case (n,k) + | (succ n,succ k) => Nat_eq n k + | (zero,zero) => True + | False; + +one = succ zero; + +List_n : Nat -> Type -> Type; + +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)); + +len : (n : Nat) ≡> (a : Type) ≡> List_n n a -> Nat; +len xs = case (xs) + | cons x xs => succ (len xs) + | nil => zero; + +%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)); View it on GitLab: https://gitlab.com/monnier/typer/commit/46381fd83e2e2651d52d0aa645712b57a0cd... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/46381fd83e2e2651d52d0aa645712b57a0cd... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
+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
participants (2)
-
Jonathan Graveline -
Stefan Monnier