(* TD 2- Les spécificités du Calcul des Constructions Inductives *)

(* 1 A- *)
Inductive est_pair : nat -> Prop :=
| pair_0 : est_pair O
| pair_S : forall n:nat, est_pair n -> est_pair (S (S n)).

(* 1 B- *)
Inductive exp (n:nat) : nat -> nat -> Prop :=
| exp_0 : exp n O (S O)
| exp_S : forall p q:nat, exp n p q -> exp n (S p) (n * q).

Hint Constructors exp sig.
Goal { x:nat | exp 2 3 x }.
eauto. (* trouve x = 8 comme en Prolog *)
Qed.

(* 2 A- *)
Inductive list (A:Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

(* 2 B- *)
Inductive prod (A B : Type) : Type := pair : A -> B -> prod A B.
Inductive unit : Type := tt : unit.
Inductive nat : Type := O : nat | S : nat -> nat.

Definition prodn : Type -> nat -> Type :=
  fun (A:Type) =>
    fix An (n:nat) : Type :=
    match n with
    | O => unit
    | S n => prod A (An n)
    end.

Definition length : forall A:Type, list A -> nat :=
  fun A => fix length (l:list A) : nat :=
  match l with
  | nil => O
  | cons _ l => S (length l)
  end.

Definition embed : forall (A:Type) (l:list A), prodn A (length A l):=
  fun A => fix embed (l:list A) : prodn A (length A l) :=
  match l as l return prodn A (length A l) with
  | nil => tt
  | cons a l => pair A (prodn A (length A l)) a (embed l)
  end.

(* 2 C- *)

(* "Fixpoint f" est une abbréviation pour "Definition f := fix f ..." *)

Definition list_rec_nodep
  :  forall (A:Type) (C:Type), C -> (A -> list A -> C -> C) -> list A -> C
  := fun (A:Type) (C:Type) (c : C) (f : A -> list A -> C -> C) => 
  fix rec (l:list A) : C :=
    match l return C with
    | nil => c
    | cons a l' => f a l' (rec l')
    end.

Definition list_rec_dep 
  :  forall (A:Type) (C:list A -> Type), 
     C (nil A) -> (forall (a:A) (l:list A), C l -> C (cons A a l)) -> 
     forall l:list A, C l
  := fun (A:Type) (C:list A -> Type)
         (c : C (nil A)) (f : forall (a:A) (l:list A), C l -> C (cons A a l)) => 
  fix rec (l:list A) : C l :=
    match l as l return C l with
    | nil => c
    | cons a l' => f a l' (rec l')
    end.

(* 3 *)
Reset nat.
Definition ackermann := fix f (n:nat) : nat -> nat := match n with
  | O => S
  | S n' => fix g (m:nat) : nat := match m with
                                   | O => f n' (S O)
                                   | S m' => f n' (g m')
                                   end
  end.

Eval compute in ackermann 2 3.
(* = 9 : nat *)
Eval compute in ackermann 3 2.
(* = 29 : nat *)

(* 4 *)
Parameters T1 T2:Type.
Parameter (t1:T1) (t2:T2).

Definition f := fun b:bool => 
  match b return (match b return Type with true => T1 | false => T2 end) with
  | true => t1
  | false => t2
  end.

(* Le même en notations abrégées *)
Definition f' (b:bool) :=  if b return (if b then T1 else T2) then t1 else t2.

(* 5 A- *)
Inductive True : Prop := I : True.

Definition phi := fun (x:unit) => match x with tt => I end.
Definition psi := fun (x:True) => match x with I => tt end.

Scheme True_indd := Induction for True Sort Prop.

Lemma l1 : forall x, phi (psi x) = x.
Proof.
destruct x using True_indd.
reflexivity.
Qed.

Lemma l2 : forall x, psi (phi x) = x.
Proof.
destruct x.
reflexivity.
Qed.

(* 5 B- *)
Inductive BOOL : Prop := TRUE : BOOL | FALSE : BOOL.

Definition bool_BOOL_retract :=
  exists phi:BOOL->bool, exists psi:bool->BOOL, forall x, phi (psi x) = x.

Definition proof_irrelevance := forall P:Prop, forall p q:P, p=q.

Lemma not_proof_irrelevance : bool_BOOL_retract -> ~ proof_irrelevance.
Proof.
intros Hr H.
assert (Hdiscr:true <> false) by discriminate.
apply Hdiscr.
destruct Hr as (phi',(psi',Hr)).
rewrite <- (Hr true).
rewrite <- (Hr false).
rewrite (H _ (psi' true) (psi' false)).
reflexivity.
Qed.