(* 2.1 Equality *) Definition sym (A:Type) (x y:A) (e:x=y) : y = x := @eq_ind A _ (fun z => z=x) eq_refl _ e. Definition trans (A:Type) (x y z:A) (e1:x=y) (e2:y=z) : x=z := @eq_ind A _ (fun a => x=a) e1 _ e2. Definition congr (A B:Type) (f:A->B) (x y:A) (e:x=y) : f x = f y := @eq_ind A _ (fun z => f x = f z) eq_refl _ e. (* with f:forall x:A, B x, f x : B x and f y : B y So f x and f y do not have the same type, so the conclusion of congr becomes ill-typed. eq_rect can be used to "coerce" f x : B x to type B y by the proof of x=y *) Lemma dcongr (A:Type) (B:A->Type) (f:forall x:A, B x) (x y:A) (e:x=y) : @eq_rect A _ B (f x) _ e = f y. Proof. case e. compute. reflexivity. Qed. (* The proof cannot be done using just eq_ind... *) (* 3 Only forall (P:Prop), P (given at type Prop) uses impredicativity *) Set Printing Universes. Definition t := Type. Fail Check (forall (x:t), x) : t. Definition u := Prop. Check (forall (x:u), x) : u. (* 4.1 *) Definition conj (A B:Prop) : Prop := forall Q:Prop, (A->B->Q) -> Q. Definition conj_i (A B:Prop) (h1:A) (h2:B) : conj A B := fun Q f => f h1 h2. Definition conj_e1 (A B:Prop) (h:conj A B) : A := h A (fun a b => a). Definition conj_e2 (A B:Prop) (h:conj A B) : B := h B (fun a b => b). Definition disj (A B:Prop) : Prop := forall Q:Prop, (A->Q)->(B->Q)->Q. Definition disj_i1 (A B:Prop) (h:A) : disj A B := fun Q f1 f2 => f1 h. Definition disj_i2 (A B:Prop) (h:B) : disj A B := fun Q f1 f2 => f2 h. Definition disj_e (A B Q:Prop) (h:disj A B) (f1:A->Q) (f2:B->Q) : Q := h Q f1 f2. Definition ex (A:Type) (B:A->Prop) : Prop := forall Q:Prop, (forall x:A, B x -> Q) -> Q. Definition ex_i A (B:A->Prop) (a:A) (h:B a) : ex A B := fun Q f => f a h. Definition ex_e A (B:A->Prop) (h:ex A B) (Q:Prop) (f:forall x:A, B x -> Q) : Q := h Q f. Definition equ (A:Type) (x y:A) : Prop := forall P:A->Prop, P x -> P y. Definition equ_refl A x : equ A x x := fun P h => h. Definition equ_ind A x y (e:equ A x y) (P:A->Prop) (h: P x) : P y := e P h. (* Since we have equ_refl and equ_ind, we could do the same proof as in 2.1. But direct proofs (especially transitivity) are easier *) Definition equ_sym A x y (e:equ A x y) : equ A y x := fun P (h:P y) => e (fun z => P z -> P x) (fun h1:P x => h1) h. Definition equ_trans A x y z (e1:equ A x y) (e2:equ A y z) : equ A x z := fun P h => e2 P (e1 P h). Definition equ_congr A B (f:A->B) x y (e:equ A x y) : equ B (f x) (f y) := fun P (h:P(f x)) => e (fun z => P (f z)) h. (* 4.2 *) Definition bool : Prop := forall Q:Prop, Q->Q->Q. Definition true : bool := fun Q f1 f2 => f1. Definition false : bool := fun Q f1 f2 => f2. Definition ifthenelse (b:bool) (Q:Prop) (th:Q) (el:Q) : Q := b Q th el. Definition band (b1 b2:bool) : bool := ifthenelse b1 _ b2 false. Lemma band_ff : band false false = false. reflexivity. Qed. Lemma band_ft : band false true = false. reflexivity. Qed. Lemma band_tf : band true false = false. reflexivity. Qed. Lemma band_tt : band true true = true. reflexivity. Qed. (* 4.3 *) Definition nat : Prop := forall Q:Prop, Q -> (Q->Q) -> Q. Definition zero : nat := fun Q z f => z. Definition succ (n:nat) : nat := fun Q z f => f (n Q z f). (* iterate n times successor on m (ok because nat : Prop) *) Definition plus (n m:nat) : nat := n nat m (fun k => succ k). (* Here we iterate first m times f, and then n more times f on z (works because Q:Prop, independently of the type of nat) *) Definition smart_plus (n m:nat) : nat := fun Q z f => n Q (m Q z f) f. Definition mult (n m:nat) : nat := n nat zero (fun k => plus k m). Definition smart_mult (n m:nat) : nat := fun Q z f => let g : Q->Q := fun x => m Q x f in n (Q->Q) (fun x=>x) (fun h:Q->Q => fun x => g (h x)) z. Eval compute in (smart_mult (succ (succ zero)) (succ (succ (succ zero)))). (* Cannot prove that a term of type nat is either zero or succ n for some n. *) (* 5. *) Definition pnat : Type := forall Q:Type, Q -> (Q->Q) -> Q. Definition pzero : pnat := fun Q z f => z. Definition psucc (n:pnat) : pnat := fun Q z f => f (n Q z f). (* cannot do the easy plus, because pnat lives in an universe higher than that of Q. *) Fail Definition pplus (n m:pnat) : pnat := n pnat m (fun k => psucc k). (* But the smart one works! *) Definition smart_pplus (n m:pnat) : pnat := fun Q z f => n Q (m Q z f) f. Fail Definition pmult (n m:pnat) : pnat := n pnat pzero (fun k => smart_pplus k m). Definition smart_pmult (n m:pnat) : pnat := fun Q z f => let g : Q->Q := fun x => m Q x f in n (Q->Q) (fun x=>x) (fun h:Q->Q => fun x => g (h x)) z. Lemma discr : ~ equ pnat pzero (psucc pzero). intro h. red in h. pose (D := fun n:pnat => n Prop True (fun _ => False)). apply (h D). compute. trivial. Qed. Definition is_inductive (n:pnat) : Prop := forall P:pnat->Prop, P pzero -> (forall k, P k -> P (psucc k)) -> P n. Definition is_ex (A:Type) (B:A->Prop) (h:ex A B) : Prop := forall P:ex A B->Prop, (forall a b, P (ex_i A B a b)) -> P h. Definition pex (A:Type) (B:A->Prop) : Prop := ex _ (is_ex A B). Definition pex_i A (B:A->Prop) (a:A) (b:B a) : pex A B. apply ex_i with (a:=ex_i _ _ a b). red; intros. apply H. Qed. Definition p_exe A (B:A->Prop) (h:pex A B) (Q:pex A B->Prop) (f:forall a b, Q (pex_i _ _ a b)) : Q h. apply (ex_e _ _ h). Definition Nat : Prop := ex pnat is_inductive. Lemma ind0 : is_inductive pzero. red; intros; trivial. Qed. Lemma indS n : is_inductive n -> is_inductive (psucc n). red; intros. apply H1. apply H; trivial. Qed. Definition Zero : Nat := ex_i _ is_inductive pzero ind0. Definition Succ (n:Nat) : Nat := ex_e _ is_inductive n _ (fun (n:pnat) nind => ex_i _ is_inductive (psucc n) (indS n nind)). (** The rest of the Peano axioms can be proved reusing ideas from Alexandre Miquel, "lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts", TYPES 2004. where an inductive type representing sets is constructed with predicative encodings *)