(* TP6 exercice 1*)

Fixpoint rec (T : Set) (a:T) (g:nat->T->T) (n:nat) {struct n} : T :=
 match n with
      O => a
  | S m => g m (rec T a g m)
  end.


Lemma rec_0 : forall T a g, rec T a g 0 = a.
intros; reflexivity.
Qed.

Lemma rec_S: forall T a g n,
   rec T a g (S n) = g n (rec T a g n).
intros; reflexivity.
Qed.

Definition pred (n:nat) := rec nat O (fun x _ => x) n.

Lemma pred_0 : pred 0 = 0.
unfold pred.
rewrite rec_0.
reflexivity.
Qed.

Lemma pred_S: forall x, pred (S x) = x.
intros; unfold pred.
rewrite rec_S.
reflexivity.
Qed.

Definition plus (x y:nat):= rec nat y (fun n m => S m) x.

Lemma plus_0: forall y, plus O y = y.
intros; reflexivity.
Qed.

Lemma plus_S: forall x y, plus (S x) y = S (plus x y).
intros; reflexivity.
Qed.

Definition mult (x y:nat):= rec nat O (fun n m => plus m y) x.

Lemma mult_0: forall y, mult O y = O.
intros; reflexivity.
Qed.

Lemma mult_S: forall x y, mult (S x) y = plus (mult x y) y.
intros; reflexivity.
Qed.

Definition ack (x : nat) := 
  rec (nat -> nat) (fun y => S y) (fun (x : nat)(fx : nat -> nat)(y : nat)=>
    (rec nat (fx 1) (fun (y : nat) (ay : nat) => fx ay) y)) x.

Lemma ack_0: forall y, ack 0 y = S y.
intros; reflexivity.
Qed.

Lemma ack_1: forall x, ack (S x) O = ack x 1.
intros; reflexivity.
Qed.

Lemma ack_2: forall x y, ack (S x) (S y) = ack x (ack (S x) y).
intros; reflexivity.
Qed.

(* TP6 exercice 2 *)

Check nat_rec.

Lemma nat_rec_0: forall P x f, nat_rec P x f O = x.
intros; reflexivity.
Qed.

Lemma nat_rec_S: forall P x f n, nat_rec P x f (S n) = f n (nat_rec P x f n).
intros; reflexivity.
Qed.


Definition rec' (T : Set) (a:T) (g:nat->T->T) (n:nat) := 
 nat_rec (fun _ : nat => T) a g n.

Lemma rec_rec': forall T a g n, rec' T a g n = rec T a g n.
intros.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.

Check nat_rec.
Check nat_ind.
Check nat_rect.

(* TP6 exercice 3 *)
Inductive list : Set :=
| nil : list
| cons : nat -> list -> list.

Check list_ind.
Check list_rec.
Check list_rect.

Definition append (l1 l2:list) :=
   list_rec (fun _ : list => list) 
   l2
   (fun h1 t1 l => cons h1 l) l1.


Lemma append_nil : forall  l2, append nil l2 = l2.
intros; reflexivity.
Qed.

Lemma append_cons : forall a l1 l2, 
  append (cons a l1) l2 = cons a (append l1 l2).
intros; reflexivity.
Qed.

Lemma nil_app : forall l, append nil l = l.
intros; reflexivity.
Qed.

Lemma app_nil : forall l, append l nil = l.
intros.
induction l.
reflexivity.
simpl.
rewrite IHl.
reflexivity.
Qed.


Lemma app_assoc : forall l1 l2 l3, 
  append (append l1 l2) l3 = append l1 (append l2 l3).
intros.
induction l1.
repeat rewrite nil_app.
reflexivity.
simpl.
rewrite IHl1.
reflexivity.
Qed.

(* TP6 exercice 4 *)

Inductive vect : nat -> Set :=
| vnil : vect 0
| vcons : forall n : nat, nat -> vect n -> vect (S n).

Check (vcons 2 5 (vcons 1 6 (vcons 0 7 vnil))).

Check vect_rec.
Check vect_ind.
Check vect_rect.


Definition vappend (n p:nat) (vn:vect n) (vp: vect p) :=
  vect_rec (fun k vk => vect (k+p))
  vp
  (fun k m (vk:vect k) (v:vect (k+p)) =>
     vcons (k+p) m v) n vn. 


(* On voudrait écrire:
Lemma vappend_assoc : forall n m p vn vm vp,
vappend (n + m) p (vappend n m vn vm) vp  
=
vappend n (m + p) vn (vappend m p vm vp).

mais les types dépendants en Coq, ce n'est pas si simple ...
en effet les deux membres de l'égalités ont respectivement pour type
vect ((n + m) + p) et vect (n + (m + p)) qui sont prouvablement égaux,
mais pas convertibles. Dit autrement, les règles de réduction de l'addition
ne permettent pas à elles seules d'identifier ((n + m) + p) et 
(n + (m + p)), il faut une réécriture d'un lemme prouvé par induction

Un solution possible est d'utiliser une égalité plus "libérale"
que celle définie par eq.*)

Require Import JMeq.
Require Import Arith.
Print JMeq.

(*On va voir qu'il sera utile d'avoir:*)
Lemma vcons_eq : forall (a n m : nat), 
  n = m -> 
  forall (v : vect n)(w : vect m), JMeq v w -> JMeq (vcons n a v) (vcons m a w).
Proof.
intros a n m enm.
rewrite enm.
intros v w evw.
rewrite evw.
reflexivity.
Qed.


(* Grâce à cette égalité "hétérogène", on peut énoncer le lemme: *)
Lemma vappend_assoc : forall n m p vn vm vp,
JMeq 
(vappend (n + m) p (vappend n m vn vm) vp)
(vappend n (m + p) vn (vappend m p vm vp)).
Proof.
intros n m p vn; induction vn.
  intros vm vp; simpl.
  reflexivity.
intros vm vp; simpl.
(* là on voudrait réécrire IHvn, mais l'égalité est encore hétérogène...
du coup on a besoin du lemme vcons_eq 
*)
apply vcons_eq.
  rewrite plus_assoc; trivial.
apply IHvn.
Qed.


(* TP6 exercice 5 *)
Definition arity := 
  nat_rect (fun k : nat=> Type) 
  nat
  (fun (k : nat)(ak : Type)=> nat -> ak).

Eval compute in (arity 5).

Definition varsum_aux  :=
  nat_rect (fun (k : nat) => nat -> arity k)
  (fun a : nat => a)
  (fun (k : nat)(vk : nat -> arity k) => (fun x y : nat => vk (x + y))).

(* et par exemple *)
Lemma varsum_aux4 : forall a x1 x2 x3 x4, 
  varsum_aux 4 a x1 x2 x3 x4 = a + x1 + x2 + x3 + x4.
Proof.
intros a x1 x2 x3 x4; trivial. 
Qed.

Definition varsum n := varsum_aux n 0.

(* encore un exemple *)
Lemma varsum4 : forall x1 x2 x3 x4, 
  varsum 4 x1 x2 x3 x4 = x1 + x2 + x3 + x4.
Proof.
intros x1 x2 x3 x4; trivial. 
Qed.


(* On construit d'abord le type de la fontion : 
nat -> ... -> Type -> Type.
*)
Definition vect_buil_type_auc :=
  nat_rect (fun (k : nat)=> Type -> Type)
    (fun t : Type => t)
    (fun (k : nat)(tk : Type -> Type)=> 
      (fun t : Type => nat -> (tk t))).


(*On procède comme pour varsum. Mais le joker à insérer dans la 
fonction auxiliaire doit avoir un type variable, du coup c'est un 
peu plus technique. La dépendance est difficile a gérer "à la main":
on définit la fonction auxiliare en "mode preuve". *)

(*La fonction auxiliaire aux n m (v : vect m) x1 ... xn := [xn ; ... ; x1]++m *)
Definition aux : forall (n m : nat), vect m -> vect_buil_type_auc n (vect (n + m)).
intro n; unfold vect_buil_type_auc;  induction n;simpl; intros m vm. 
exact vm.
intro k; simpl.
rewrite plus_n_Sm.
apply IHn.
exact (vcons m k vm).
Defined.

Definition vect_build (n : nat) := aux n 0 vnil.

(* Par contre à la réduction c'est la catastrophe, du fait qu'on aie dû
réécrire avec plus_n_Sm au cours de la définition... *)
Eval compute in (vect_build 2 1 2).