(* Récurseur T *)
Fixpoint rec (T : Set)(x_base : T)(f : nat -> T -> T)(n : nat){struct n} : T :=
  match n with
    |0 => x_base
    |S m => f m (rec T x_base f m)
  end.


(* Égalités définitionnelles *)
Lemma rec0 : forall (T : Set)(x : T)(f : nat -> T -> T), 
  rec T x f 0 = x.
Proof.
intros T x f.
simpl.
reflexivity.
Qed.

Lemma recS : forall (T : Set)(x : T)(f : nat -> T -> T)(n : nat), 
  rec T x f (S n) = f n (rec T x f n).
Proof.
intros T x f n.
simpl.
reflexivity.
Qed.


Definition pred n := rec nat 0 (fun (x : nat)(px : nat) => x) n.

(* Pour vérifier les égalités définitionnelles pred, 
on utilise les lemmes rec0 et recS *)

Lemma pred0 : pred 0 = 0.
Proof.
unfold pred.
rewrite rec0.
reflexivity.
Qed.

Lemma predS : forall n, pred (S n) = n.
Proof.
intros n; unfold pred.
rewrite recS.
reflexivity.
Qed.

(* On définit l'addition *)
Definition plus n m := rec nat n (fun (x : nat)(px : nat) => S px) m.

(* Véfifications *)
Lemma plus0 : forall n, plus n 0 = n.
Proof.
intros n; unfold plus.
rewrite rec0.
reflexivity.
Qed.

Lemma plusS : forall n m, plus n (S m) = S (plus n m).
Proof.
intros n m; unfold plus.
rewrite recS.
reflexivity.
Qed.



(* On définit la multiplication *)
Definition mult n m := rec nat 0 (fun (x : nat)(px : nat) => plus px n) m.

(* Véfifications *)
Lemma mult0 : forall n, mult n 0 = 0.
Proof.
intros n; unfold mult.
rewrite rec0.
reflexivity.
Qed.

Lemma multS : forall n m, mult n (S m) = plus (mult n m) n.
Proof.
intros n m; unfold mult.
rewrite recS.
reflexivity.
Qed.

(* La fonction d'Ackermann *)
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 ack0y : forall y, ack 0 y = S y.
Proof.
intro y; unfold ack.
rewrite rec0.
reflexivity.
Qed.

Lemma ackS0 : forall x, ack (S x) 0 = ack x 1.
Proof.
intros x; unfold ack.
rewrite recS.
rewrite rec0.
reflexivity.
Qed.

Lemma ackSS : forall x y, ack (S x) (S y) = ack x (ack (S x) y).
Proof.
intros x y; unfold ack.
rewrite recS.
reflexivity.
Qed.

(* Exercice 2 *)
Check nat_rec.

Lemma nat_rec0 : forall P x f, nat_rec P x f 0 = x.
Proof.
intros P x f.
reflexivity.
Qed.


Lemma nar_recS : forall P x f n, nat_rec P x f (S n) = f n (nat_rect P x f n).
Proof.
intros P x f n.
reflexivity.
Qed.

Definition rec' := 
fun (T : Set) (x : T) (f : nat -> T -> T) => nat_rec (fun _ : nat => T) x f.

Lemma rec_rec': forall T x f n, rec' T x f n = rec T x f n.
Proof.
intros T x f n.
induction n; simpl; trivial.
rewrite IHn; trivial.
Qed.


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

Definition append (l1 l2 : list) :=
  list_rec (fun _ : list => list) 
  l2
  (fun (a : nat)(l : list)(l1_l2 : list) => cons a l1_l2) l1.

Definition v1 := cons 2 (cons 1 nil).
Definition v2 := cons 4 (cons 3 nil).
Eval compute in (append v2 v1).

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

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

Lemma nil_app : forall l, append nil l = l.
Proof.
intros l.
trivial.
Qed.

Lemma app_nil : forall l, append l nil = l.
Proof.
induction l as [| a l IHl]; trivial.
simpl; rewrite IHl.
trivial.
Qed.

Lemma app_assoc : forall l1 l2 l3, 
  append (append l1 l2) l3 = append l1 (append l2 l3).
Proof.
intros l1; induction l1 as [|a l1 Hl1]; intros l2 l3.
  trivial.
simpl; rewrite Hl1.
trivial.
Qed.

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

Check vect_rec.

Definition vappend (n p : nat)(vn : vect n)(vp : vect p) :=
  vect_rec (fun (k : nat)(vk : vect k)=> vect (k + p))
  vp
  (fun (k m : nat)(vk : vect k)(vkp : vect (k + p)) =>
    vcons (k + p) m vkp) 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 pou 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éorgè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.

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


(* Programmer avec les types dépendants est un problème délicat et 
les solutions adoptées par Coq sont parfois plus adaptées à un usage
de spécification qu'à une véritable utilisation en programmation et
définition de  types de données...

Il existe cependant des solutions plus élégantes que la méthode "à la main" et 
à cloche pied utilisée ci-dessus. Voire par exemple le chapitre 19 du
manuel de référence de Coq.
*)