(** * Examples of Programming and Proving in Rocq *)

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

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.

(** We 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.

(** A first attempt at defining [reverse] could be
<<
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. 
>>
which produces a fault message by Rocq:
<<
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)".
>>
*)

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

Eval compute in (reverse _ example_list_1).

End Natlist_dep.