Library natlist_dep
Examples of Programming and Proving in Rocq II
Dependent (Parametrized) Inductive Types
Vectors, or: "lists-of-length-n", for n: nat
Section NATLIST_DEP.
Inductive natlist_dep : nat -> Set :=
| nil : natlist_dep O
| cons : forall n : nat, nat -> natlist_dep n -> natlist_dep (S n).
We have to take care of the length as a parameter.
The following doesn't type check.
Definition example_list_1 :=
cons 3 (cons 1 (cons 4 (cons 1 (cons 5 (cons 9 nil))))).
Definition example_list :=
cons 5 3 (cons 4 1 (cons 3 4 (cons 2 1 (cons 1 5 (cons 0 9 nil))))).
Check example_list.
Definition example_list_1 :=
cons _ 3 (cons _ 1 (cons _ 4 (cons _ 1 (cons _ 5 (cons _ 9 nil))))).
Print example_list_1.
Rocq has inferred the missing arguments for us
Notation "[]" := nil.
Notation "x :: ls" := (cons _ x ls).
Definition example_list_2 :=
3 :: 1 :: 4 :: 1 :: 5 :: 9 :: nil.
Lemma simple_eq : example_list_1 = example_list_2.
Proof.
reflexivity.
Qed.
Fixpoint zeroes (n : nat) : natlist_dep n :=
match n with
| O => nil
| S n' => cons n' O (zeroes n')
end.
We define the basic operations of head and tail
NB The match case for nil can be left out;
the type checker knows it doesn't occur
NB Again the match case for nil can be left out;
the type checker knows it doesn't occur
Eval compute in (Head _ example_list_1).
Eval compute in (Tail _ example_list_1).
Fixpoint append(n m : nat)(k : natlist_dep n)(l : natlist_dep m) {struct k}
: natlist_dep (plus n m) :=
match k with
| nil => l
| cons n' h t => cons (plus n' m) h (append n' m t l)
end.
To make reverse type check, we need to "coerce" natlist_dep (n+1)
to natlist_dep (S n)
Lemma plus_one : forall n:nat, n+1 = S n.
Proof.
induction n.
- simpl. auto.
- simpl. rewrite IHn. auto.
Defined.
Lemma help : forall n:nat, natlist_dep (n+1) -> natlist_dep (S n).
Proof.
intro n.
rewrite plus_one.
auto.
Defined.
Fixpoint reverse (n : nat) (k : natlist_dep n) {struct k} :
natlist_dep n :=
match k with
nil => nil
| cons m h t => help _ (append m 1 (reverse m t) (cons 0 h nil))
end.
One could try to define reverse directly, without first defining help,
as it is done on the slides. But that doesn't get very nice:
Print help.
Fixpoint reverse' (n : nat) (k : natlist_dep n) {struct k} :
natlist_dep n :=
match k with
nil => nil
| cons m h t => eq_rec (plus m 1) (fun n => natlist_dep n)
(append m 1 (reverse' m t) (cons 0 h nil)) (S m)(plus_one m)
end.
Executing reverse works as expected.
Because we have saved the Lemmas help and plus_one transparently
using Defined, these terms can be excecuted.
Note what happens when you change Defined into Qed
Print example_list_1.
example_list_1 = 3 :: 1 :: 4 :: 1 :: 5 :: 9 :: ☐ ]
which is equal to
cons 5 3 (cons 4 1 (cons 3 4 (cons 2 1 (cons 1 5 (cons 0 9 nil)))))
: natlist_dep 6