(* Various Examples of Programming and Proving in Coq II *)

(* Dependent (Parametrized) Inductive Types: the case for 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).

(* Definition example_list_1 := 
cons 3 (cons 1 (cons 4 (cons 1 (cons 5 (cons 9 nil))))).

Check example_list_1. *)

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. 
(* Coq 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 (* return natlist_dep n *) with
| O    => nil
| S n' => cons n' O (zeroes n')
end.

(* Now let us define the basic operations of head and tail *)
Definition Tail (n:nat)(l : natlist_dep (S n)):  natlist_dep n:=
match l with
 cons n k l => l
end.
(* NB! The match case for "nil" can be left out; 
   the type checker knows it doesn't occur *)

Definition Head (n:nat)(l : natlist_dep (S n)):  nat :=
match l with
 cons n k l => k
end.
(* 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 (* in natlist_dep n return natlist_dep (plus n m) *) with
| nil => l
| cons n' h t => cons (plus n' m) h (append n' m t l)
end.

(*
Fixpoint reverse (n : nat) (k : natlist_dep n) {struct k} :
natlist_dep n :=
match k with
nil => nil
| cons m h t => append m 1 (reverse m t) (cons 0 h nil) 
end. 

In environment
reverse : forall n : nat, natlist_dep n -> natlist_dep n
n : nat
k : natlist_dep n
m : nat
h : nat
t : natlist_dep m
The term "append m 1 (reverse m t) (cons 0 h nil)" has type
 "natlist_dep (m + 1)" while it is expected to have type "natlist_dep (S m)".


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
*)

Eval compute in (reverse _ example_list_1).

End NATLIST_DEP.