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[2]) (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[3]. 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_Type1_r:
37 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. 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 lemma eq_rect_Type2_r:
42 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
43 #A #a #P #H #x #p (generalize in match H) (generalize in match P)
46 lemma eq_rect_Type3_r:
47 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
48 #A #a #P #H #x #p (generalize in match H) (generalize in match P)
51 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
52 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
54 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
55 #A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
57 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
58 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
60 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
61 #A #B #Ha #Heq (elim Heq); //; qed.
63 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
64 #A #x #y #z #H1 #H2 >H1; //; qed.
66 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
67 #A #B #f #x #y #H >H; //; qed.
69 (* deleterio per auto? *)
70 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
71 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
72 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
74 lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
75 ∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
76 #A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
78 (* hint to genereric equality
79 definition eq_equality: equality ≝
80 mk_equality eq refl rewrite_l rewrite_r.
83 unification hint 0 ≔ T,a,b;
85 (*------------------------------------*) ⊢
86 equal X T a b ≡ eq T a b.
89 (********** connectives ********)
91 inductive True: Prop ≝
94 inductive False: Prop ≝ .
96 (* ndefinition Not: Prop → Prop ≝
99 inductive Not (A:Prop): Prop ≝
100 nmk: (A → False) → Not A.
102 interpretation "logical not" 'not x = (Not x).
104 theorem absurd : ∀A:Prop. A → ¬A → False.
105 #A #H #Hn (elim Hn); /2/; qed.
108 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
109 #A; #C; #H; #Hn; nelim (Hn H).
112 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
116 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
118 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
122 inductive And (A,B:Prop) : Prop ≝
123 conj : A → B → And A B.
125 interpretation "logical and" 'and x y = (And x y).
127 theorem proj1: ∀A,B:Prop. A ∧ B → A.
128 #A #B #AB (elim AB) //; qed.
130 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
131 #A #B #AB (elim AB) //; qed.
134 inductive Or (A,B:Prop) : Prop ≝
135 or_introl : A → (Or A B)
136 | or_intror : B → (Or A B).
138 interpretation "logical or" 'or x y = (Or x y).
140 definition decidable : Prop → Prop ≝
144 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
145 ex_intro: ∀ x:A. P x → ex A P.
147 interpretation "exists" 'exists x = (ex ? x).
149 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
150 ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
154 λ A,B. (A → B) ∧ (B → A).
156 interpretation "iff" 'iff a b = (iff a b).
158 (* cose per destruct: da rivedere *)
160 definition R0 ≝ λT:Type[0].λt:T.t.
162 definition R1 ≝ eq_rect_Type0.
164 (* used for lambda-delta *)
168 ∀T1:∀x0:T0. a0=x0 → Type[0].
169 ∀a1:T1 a0 (refl ? a0).
170 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
171 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
175 ∀e1:R1 ?? T1 a1 ? e0 = b1.
177 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
178 @(eq_rect_Type0 ????? e1)
186 ∀T1:∀x0:T0. a0=x0 → Type[0].
187 ∀a1:T1 a0 (refl ? a0).
188 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
189 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
190 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
191 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
192 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
196 ∀e1:R1 ?? T1 a1 ? e0 = b1.
198 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
199 T3 b0 e0 b1 e1 b2 e2.
200 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
201 @(eq_rect_Type0 ????? e2)
202 @(R2 ?? ? ???? e0 ? e1)
209 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
210 ∀a1:T1 a0 (refl T0 a0).
211 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
212 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
213 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
214 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
215 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
216 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
217 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
218 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
219 ∀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.
221 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
222 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
223 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
224 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
229 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
231 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
232 ∀b3: T3 b0 e0 b1 e1 b2 e2.
233 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
234 T4 b0 e0 b1 e1 b2 e2 b3 e3.
235 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
236 @(eq_rect_Type0 ????? e3)
237 @(R3 ????????? e0 ? e1 ? e2)
241 definition eqProp ≝ λA:Prop.eq A.
243 (* Example to avoid indexing and the consequential creation of ill typed
244 terms during paramodulation *)
245 example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
246 #A #x #h @(refl ? h: eqProp ? ? ?).
249 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
250 #T #t #P #H #p >(lemmaK T t p) @H