(*****************************)
(* 1 Basic inductive types          *)

(* 1.1 Booleans *)

Inductive bool : Type := true : bool | false : bool.

Definition negb (b:bool) := match b with true => false | false => true end.

Definition andb (b b':bool) := match b with true => b' | false => false end.

(* 1.2 Disjunction *)

(* 1- *)

Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.

(* 2- *)

Definition sum' (A B:Prop) := forall P:Prop, (A -> P) -> (B -> P) -> P.
Definition inl' (A B:Prop) (H:A) : sum' A B := fun (P:Prop) (H1:A -> P) (H2:B -> P) => H1 H.
Definition inr' (A B:Prop) (H:B) : sum' A B := fun (P:Prop) (H1:A -> P) (H2:B -> P) => H2 H.
Definition case_sum' (A B P:Prop) (H1:A -> P) (H2:B -> P) (H:sum' A B) :=
  H P H1 H2.

(* 3- *)

Definition select (A B:Type) :=
  fun (b:sum A B) => match b with inl _ => true | inr _ => false end.

(* 1.3 Conjunction *)

Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B.

Theorem and_comm : forall A B : Prop, and A B -> and B A.
Proof.
exact (fun A B H => match H with conj a b => conj _ _ b a end).
Qed.

(*****************************************)
(* 2 Natural numbers at the Prop level in CC *)

Definition eq := fun (A : Prop) (a b:A) => forall P:A->Prop, P a -> P b.
Definition neg := fun (A : Prop) => A -> forall C : Prop, C.

Definition N := forall C:Prop, C -> (C -> C) -> C.
Definition O : N := fun C x f => x.
Definition S : N -> N := fun n => fun C x f => f (n C x f).
Definition plus : N -> N -> N := fun n m => fun C x f => n C (m C x f) f.
Definition mult : N -> N -> N := fun n m => fun C x f => n C x (fun x => m C x f).

Definition prod := fun A B : Prop => forall C:Prop, (A -> B -> C) -> C.
Definition pair := fun A B : Prop => fun a b => fun C (f:A->B->C) => f a b.
Definition fst := fun A B : Prop => fun p : prod A B => p A (fun x _ => x).
Definition snd := fun A B : Prop => fun p : prod A B => p B (fun _ y => y).

Definition pred : N -> N := fun n => 
  fst _ _ (n (prod N N) (pair _ _ O O) 
    (fun p => pair _ _ (snd _ _ p) (S (snd _ _ p)))).

Definition IND := fun n:N => 
  forall P:N->Prop, P O -> (forall n, P n -> P (S n)) -> P n.

(* Non provable : consider the boolean model (not proof-irrelevent) which 
   interprets Prop as a set which contains two types : the empty type and the type of all
   pure lambda terms.  The interprétation of N (which is inhabited) is the set of all 
   lambda-terms, while the interprétation of "IND n" is a proposition which is inhabited only 
   when n is a lambda-term buit by iterating S from the lambda-term 0. "IND
   n" is not true for all lambda-terms (only true for the subset of Church's numbers and "forall
   n:N, IND n" is false (i.e  empty) in the model. [référence: Herman
   Geuvers, Induction Is Not Derivable in Second Order Dependent Type
   Theory, TLCA 2001, by extending the construction to CC as in Stefanova-Geuvers, 
   A Simple Model Construction for the Calculus of Constructions, TYPES 1995]

Theorem ind : forall n:N, IND n.
*)

(* A priori non provable : can we build a term model which contradicts this property ?
   (the keypoint which requires induction is the lemma
   "pred (S n) = n"; which requires induction because the predecessor
   is built by iteration from zéro)

Theorem inj_S : forall n m : N, eq N (S n) (S m) -> eq N n m.
*)

Theorem inj_S : forall n m : N, IND n -> IND m -> eq N (S n) (S m) -> eq N n m.
Proof.
intros n m Hn Hm H.
assert (H':forall n : N, IND n -> eq _ (pred (S n)) n).
 intros p Hp. apply Hp.
  exact (fun _ x => x).
  intros n0 Heqn0. pattern n0 at 2. apply Heqn0. exact (fun _ x => x).
apply (H' m Hm).
apply H.
pattern n at 1.
apply (H' n Hn).
exact (fun _ x => x).
Qed.

(* Non provable because CC has a "proof-irrelevant" interprétation which
   makes equal every terms in a type with type Prop (cf below).
   forgetting dependencies will also change this proof into a proof of 
   forall n : N, (forall P:Prop,P->P) -> forall C,C that will lead to a contradiction

Theorem O_S : forall n : N, neg (eq _ O (S n)).
*)

Reset Initial.
(*****************************************)
(* Entiers au niveau Type dans CC et F_w *)

Definition eq := fun (A : Type) (a b:A) => forall P:A->Prop, P a -> P b.
Definition neg := fun (A : Prop) => A -> forall C : Prop, C.

Definition N := Prop -> (Prop -> Prop) -> Prop.
Definition O : N := fun x f => x.
Definition S : N -> N := fun n => fun x f => f (n x f).
Definition plus : N -> N -> N := fun n m => fun x f => n (m x f) f.
Definition mult : N -> N -> N := fun n m => fun x f => n x (fun x => m x f).

(* no predecessor (no power function) *)
(* cf Schwichtenberg 1976 and Statman 1979 *)

Definition IND := fun n:N => 
  forall P:N->Prop, P O -> (forall n, P n -> P (S n)) -> P n.

(* not provable : the opposite can be proven, there is in N, non standard natural numbers
(for instance of the form fun _ _ => A with A an arbitrary proposition)

Theorem ind : forall n : N, IND n.
*)

Theorem not_ind : (forall n : N, IND n) -> forall C:Prop, C.
Proof.
intros H C.
pose (n_non_standard := (fun _ _ => forall C:Prop, C) : N).
pose (True:=C->C).
pose (P_identity := (fun n:N => n True (fun X => X))).
apply (H n_non_standard P_identity).
exact (fun x => x).
intros. assumption. 
Qed.

(* not provable ??
Theorem inj_S : forall n m : N, eq N (S n) (S m) -> eq N n m.
Theorem inj_S : forall n m : N, IND n -> IND m -> eq N (S n) (S m) -> eq N n m.
*)

Theorem O_S : forall n : N, neg (eq _ O (S n)).
Proof.
intros n H C.
change C with (S n (C -> C) (fun _ => C)) in |- *.
apply H. exact (fun x => x).
Qed.

Reset Initial.

(*************************************************)
(* Natural numbers at level Type_2 in CC_w and F_w.2 *)

Definition eq := fun (A : Type) (a b:A) => forall P:A->Prop, P a -> P b.
Definition neg := fun (A : Prop) => A -> forall C : Prop, C.

Definition Type2 := Type.
Definition Type1 := Type : Type2.

Definition N : Type2 := forall C:Type1, C -> (C -> C) -> C.
Definition O : N := fun C x f => x.
Definition S : N -> N := fun n => fun C x f => f (n C x f).
Definition plus : N -> N -> N := fun n m => fun C x f => n C (m C x f) f.
Definition mult : N -> N -> N := fun n m => fun C x f => n C x (fun x => m C x f).

Definition prod := fun A : Type1 => (A -> A -> A) -> A.
Definition pair := fun A : Type1 => fun a b => fun (f:A->A->A) => f a b.
Definition fst := fun A : Type1 => fun p : prod A => p (fun x _ => x).
Definition snd := fun A : Type1 => fun p : prod A => p (fun _ y => y).

Definition pred : N -> N := fun n => fun C x f =>
  fst _ (n _ (pair _ x x)
    (fun p => pair _ (snd _ p) (f (snd _ p)))).

Definition IND := fun n:N => 
  forall P:N->Prop, P O -> (forall n, P n -> P (S n)) -> P n.

(* not provable ?? 
Theorem ind : forall n : N, IND n.
*)

Theorem inj_S : forall n m : N, IND n -> IND m -> eq N (S n) (S m) -> eq N n m.
Proof.
intros n m Hn Hm H.
assert (H':forall n : N, IND n -> eq _ (pred (S n)) n).
 intros p Hp. apply Hp.
  exact (fun _ x => x).
  intros n0 Heqn0. pattern n0 at 2. apply Heqn0. exact (fun _ x => x).
apply (H' m Hm).
apply H.
pattern n at 1.
apply (H' n Hn).
exact (fun _ x => x).
Qed.

Theorem O_S : forall n : N, neg (eq _ O (S n)).
Proof.
intros n H.
apply (H (fun n => n _ (forall C:Prop, C -> C) (fun _ => forall C:Prop, C))).
exact (fun _ x => x).
Qed.