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).
21 interpretation "leibniz reflexivity" 'refl = refl.
24 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
25 #A #a #x #p (cases p) // qed.
28 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
29 #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
31 lemma eq_rect_Type0_r:
32 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
33 #A #a #P #H #x #p (generalize in match H) (generalize in match P)
36 lemma eq_rect_Type2_r:
37 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
38 #A #a #P #H #x #p (generalize in match H) (generalize in match P)
41 theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y.
42 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
44 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
45 #A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
47 theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y.
48 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
50 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
51 #A #B #Ha #Heq (elim Heq); //; qed.
53 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
54 #A #x #y #z #H1 #H2 >H1; //; qed.
56 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
57 #A #B #f #x #y #H >H; //; qed.
59 (* deleterio per auto? *)
60 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
61 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
62 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
64 lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
65 ∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
66 #A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
68 (* hint to genereric equality
69 definition eq_equality: equality ≝
70 mk_equality eq refl rewrite_l rewrite_r.
73 unification hint 0 ≔ T,a,b;
75 (*------------------------------------*) ⊢
76 equal X T a b ≡ eq T a b.
79 (********** connectives ********)
81 inductive True: Prop ≝
84 inductive False: Prop ≝ .
86 (* ndefinition Not: Prop → Prop ≝
89 inductive Not (A:Prop): Prop ≝
90 nmk: (A → False) → Not A.
92 interpretation "logical not" 'not x = (Not x).
94 theorem absurd : ∀A:Prop. A → ¬A → False.
95 #A #H #Hn (elim Hn); /2/; qed.
98 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
99 #A; #C; #H; #Hn; nelim (Hn H).
102 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
106 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
108 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
112 inductive And (A,B:Prop) : Prop ≝
113 conj : A → B → And A B.
115 interpretation "logical and" 'and x y = (And x y).
117 theorem proj1: ∀A,B:Prop. A ∧ B → A.
118 #A #B #AB (elim AB) //; qed.
120 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
121 #A #B #AB (elim AB) //; qed.
124 inductive Or (A,B:Prop) : Prop ≝
125 or_introl : A → (Or A B)
126 | or_intror : B → (Or A B).
128 interpretation "logical or" 'or x y = (Or x y).
130 definition decidable : Prop → Prop ≝
134 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
135 ex_intro: ∀ x:A. P x → ex A P.
137 interpretation "exists" 'exists x = (ex ? x).
139 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
140 ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
144 λ A,B. (A → B) ∧ (B → A).
146 interpretation "iff" 'iff a b = (iff a b).
148 (* cose per destruct: da rivedere *)
150 definition R0 ≝ λT:Type[0].λt:T.t.
152 definition R1 ≝ eq_rect_Type0.
154 (* used for lambda-delta *)
158 ∀T1:∀x0:T0. a0=x0 → Type[0].
159 ∀a1:T1 a0 (refl ? a0).
160 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
161 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
165 ∀e1:R1 ?? T1 a1 ? e0 = b1.
167 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
168 @(eq_rect_Type0 ????? e1)
176 ∀T1:∀x0:T0. a0=x0 → Type[0].
177 ∀a1:T1 a0 (refl ? a0).
178 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
179 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
180 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
181 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
182 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
186 ∀e1:R1 ?? T1 a1 ? e0 = b1.
188 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
189 T3 b0 e0 b1 e1 b2 e2.
190 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
191 @(eq_rect_Type0 ????? e2)
192 @(R2 ?? ? ???? e0 ? e1)
199 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
200 ∀a1:T1 a0 (refl T0 a0).
201 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
202 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
203 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
204 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
205 ∀a3:T3 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 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
208 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
209 ∀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.
211 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
212 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
213 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
214 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
219 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
221 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
222 ∀b3: T3 b0 e0 b1 e1 b2 e2.
223 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
224 T4 b0 e0 b1 e1 b2 e2 b3 e3.
225 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
226 @(eq_rect_Type0 ????? e3)
227 @(R3 ????????? e0 ? e1 ? e2)
231 definition eqProp ≝ λA:Prop.eq A.
233 (* Example to avoid indexing and the consequential creation of ill typed
234 terms during paramodulation *)
235 example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
236 #A #x #h @(refl ? h: eqProp ? ? ?).
239 theorem streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
240 #T #t #P #H #p >(lemmaK ?? p) @H