2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/pts.ma".
13 include "hints_declaration.ma".
15 (* propositional equality *)
17 inductive eq (A:Type[1]) (x:A) : A → Prop ≝
20 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
23 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
24 #A #a #x #p (cases p) // qed.
27 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
28 #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
30 lemma eq_rect_Type2_r:
31 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
32 #A #a #P #H #x #p (generalize in match H) (generalize in match P)
35 theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y.
36 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
38 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
39 #A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
41 theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y.
42 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
44 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
45 #A #B #Ha #Heq (elim Heq); //; qed.
47 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
48 #A #x #y #z #H1 #H2 >H1; //; qed.
50 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
51 #A #B #f #x #y #H >H; //; qed.
53 (* deleterio per auto? *)
54 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
55 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
56 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
58 lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
59 ∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
60 #A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
62 (* hint to genereric equality
63 definition eq_equality: equality ≝
64 mk_equality eq refl rewrite_l rewrite_r.
67 unification hint 0 ≔ T,a,b;
69 (*------------------------------------*) ⊢
70 equal X T a b ≡ eq T a b.
73 (********** connectives ********)
75 inductive True: Prop ≝
78 inductive False: Prop ≝ .
80 (* ndefinition Not: Prop → Prop ≝
83 inductive Not (A:Prop): Prop ≝
84 nmk: (A → False) → Not A.
86 interpretation "logical not" 'not x = (Not x).
88 theorem absurd : ∀A:Prop. A → ¬A → False.
89 #A #H #Hn (elim Hn); /2/; qed.
92 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
93 #A; #C; #H; #Hn; nelim (Hn H).
96 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
100 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
102 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
106 inductive And (A,B:Prop) : Prop ≝
107 conj : A → B → And A B.
109 interpretation "logical and" 'and x y = (And x y).
111 theorem proj1: ∀A,B:Prop. A ∧ B → A.
112 #A #B #AB (elim AB) //; qed.
114 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
115 #A #B #AB (elim AB) //; qed.
118 inductive Or (A,B:Prop) : Prop ≝
119 or_introl : A → (Or A B)
120 | or_intror : B → (Or A B).
122 interpretation "logical or" 'or x y = (Or x y).
124 definition decidable : Prop → Prop ≝
128 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
129 ex_intro: ∀ x:A. P x → ex A P.
131 interpretation "exists" 'exists x = (ex ? x).
133 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
134 ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
138 λ A,B. (A → B) ∧ (B → A).
140 interpretation "iff" 'iff a b = (iff a b).
142 (* cose per destruct: da rivedere *)
144 definition R0 ≝ λT:Type[0].λt:T.t.
146 definition R1 ≝ eq_rect_Type0.
148 (* used for lambda-delta *)
152 ∀T1:∀x0:T0. a0=x0 → Type[0].
153 ∀a1:T1 a0 (refl ? a0).
154 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
155 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
159 ∀e1:R1 ?? T1 a1 ? e0 = b1.
161 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
162 @(eq_rect_Type0 ????? e1)
170 ∀T1:∀x0:T0. a0=x0 → Type[0].
171 ∀a1:T1 a0 (refl ? a0).
172 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
173 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
174 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
175 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
176 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
180 ∀e1:R1 ?? T1 a1 ? e0 = b1.
182 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
183 T3 b0 e0 b1 e1 b2 e2.
184 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
185 @(eq_rect_Type0 ????? e2)
186 @(R2 ?? ? ???? e0 ? e1)
193 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
194 ∀a1:T1 a0 (refl T0 a0).
195 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
196 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
197 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
198 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
199 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
200 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
201 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
202 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
203 ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
205 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
206 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
207 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
208 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
213 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
215 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
216 ∀b3: T3 b0 e0 b1 e1 b2 e2.
217 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
218 T4 b0 e0 b1 e1 b2 e2 b3 e3.
219 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
220 @(eq_rect_Type0 ????? e3)
221 @(R3 ????????? e0 ? e1 ? e2)
225 (* TODO concrete definition by means of proof irrelevance *)
226 axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.