(* 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- *)
(* Defined in standard library *)
(*
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 *)

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.

(* 6 *)

Inductive W (A:Type) (B:A -> Type) : Type := 
     node : forall (a:A), (B a -> W A B) -> W A B.

Check W_rect.

Section Exo6.

(* 6-2 *)
Inductive empty : Type :=.
Definition Bnat : bool -> Type := fun b:bool => if b then empty else unit.
Definition nat := W bool Bnat.
Definition O : nat := node bool  Bnat true (fun abs => match abs return nat with end).
Definition S (n:nat) : nat := node bool  Bnat false (fun x => n).

(* 6-3 *)
Parameter V:Type.
Inductive nt : Type := Left | Val : V -> nt | Right.

Definition Btree : option V ->  Type := fun x => match x with None => empty | Some _ => bool end.
Definition tree := W _ Btree.
Definition leaf : tree := node _  Btree None (fun abs => match abs return tree with end).
Definition bin (l:tree) (v:V) (r:tree) : tree := node _  Btree (Some v) (fun b => if b then l else r).

(* 6-4 *)
Definition f1 (n:nat) (x : unit) := n.
Definition f2 (n:nat) (x : unit) := match x with _ => n end.

(* 6-5 *)
Fixpoint eqW A B (t u : W A B) {struct t}: Prop := match (t,u) with
     (node a st, node b su) 
     => exists h : a = b, forall x : B a, eqW A B (st x) (su (match h with refl_equal => x end))
end.

Inductive eqW2 A B : W A B -> W A B -> Prop :=
    eqW2_intro : forall a (st su : B a -> W A B), (forall x : B a, eqW2 _ _ (st x) (su x)) 
                        -> eqW2 _ _ (node _ _ a st) (node _ _ a su).

End Exo6.