1 include "basics/pts.ma".
2 include "basics/hints_declaration.ma".
4 (* propositional equality *)
6 inductive eq (A:Type[2]) (x:A) : A → Prop ≝
9 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
10 interpretation "leibniz reflexivity" 'refl = refl.
13 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → P x p.
14 #A #a #x #p (cases p) // qed.
17 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
18 #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
20 lemma eq_rect_Type0_r:
21 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
22 #A #a #P #H #x #p lapply H lapply P
25 lemma eq_rect_Type1_r:
26 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
27 #A #a #P #H #x #p lapply H lapply P
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 lapply H lapply P
35 lemma eq_rect_Type3_r:
36 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
37 #A #a #P #H #x #p lapply H lapply P
40 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
41 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
43 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
44 #A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
46 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
47 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
49 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
50 #A #B #Ha #Heq (elim Heq); //; qed.
52 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
53 #A #x #y #z #H1 #H2 >H1; //; qed.
55 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
56 #A #B #f #x #y #H >H; //; qed.
58 (* deleterio per auto? *)
59 theorem eq_f2: ∀A,B,C.∀f:A→B→C.
60 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
61 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
63 lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
64 ∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
65 #A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
67 (* hint to genereric equality
68 definition eq_equality: equality ≝
69 mk_equality eq refl rewrite_l rewrite_r.
72 unification hint 0 ≔ T,a,b;
74 (*------------------------------------*) ⊢
75 equal X T a b ≡ eq T a b.
78 (********** connectives ********)
80 inductive True: Prop ≝
83 inductive False: Prop ≝ .
85 (* ndefinition Not: Prop → Prop ≝
88 inductive Not (A:Prop): Prop ≝
89 nmk: (A → False) → Not A.
91 interpretation "logical not" 'not x = (Not x).
93 theorem absurd : ∀A:Prop. A → ¬A → False.
94 #A #H #Hn (elim Hn); /2/; qed.
97 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
98 #A; #C; #H; #Hn; nelim (Hn H).
101 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
105 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
107 theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
111 inductive And (A,B:Prop) : Prop ≝
112 conj : A → B → And A B.
114 interpretation "logical and" 'and x y = (And x y).
116 theorem proj1: ∀A,B:Prop. A ∧ B → A.
117 #A #B #AB (elim AB) //; qed.
119 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
120 #A #B #AB (elim AB) //; qed.
123 inductive Or (A,B:Prop) : Prop ≝
124 or_introl : A → (Or A B)
125 | or_intror : B → (Or A B).
127 interpretation "logical or" 'or x y = (Or x y).
129 definition decidable : Prop → Prop ≝
133 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
134 ex_intro: ∀ x:A. P x → ex A P.
136 interpretation "exists" 'exists x = (ex ? x).
138 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
139 ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
143 λ A,B. (A → B) ∧ (B → A).
145 interpretation "iff" 'iff a b = (iff a b).
147 lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
150 lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
151 #A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
153 lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
154 #A #B * #H1 #H2 % /3/ qed.
156 lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
157 #A #B #C * #H1 #H2 % * /3/ qed.
159 lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
160 #A #B #C * #H1 #H2 % * /3/ qed.
162 lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
163 #A #B #C * #H1 #H2 % * /3/ qed.
165 lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
166 #A #B #C * #H1 #H2 % * /3/ qed.
168 (* cose per destruct: da rivedere *)
170 definition R0 ≝ λT:Type[0].λt:T.t.
172 definition R1 ≝ eq_rect_Type0.
174 (* used for lambda-delta *)
178 ∀T1:∀x0:T0. a0=x0 → Type[0].
179 ∀a1:T1 a0 (refl ? a0).
180 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
181 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
185 ∀e1:R1 ?? T1 a1 ? e0 = b1.
187 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
188 @(eq_rect_Type0 ????? e1)
196 ∀T1:∀x0:T0. a0=x0 → Type[0].
197 ∀a1:T1 a0 (refl ? a0).
198 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
199 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
200 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
201 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
202 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
206 ∀e1:R1 ?? T1 a1 ? e0 = b1.
208 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
209 T3 b0 e0 b1 e1 b2 e2.
210 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
211 @(eq_rect_Type0 ????? e2)
212 @(R2 ?? ? ???? e0 ? e1)
219 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
220 ∀a1:T1 a0 (refl T0 a0).
221 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
222 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
223 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
224 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
225 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
226 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
227 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
228 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
229 ∀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.
231 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
232 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
233 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
234 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
239 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
241 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
242 ∀b3: T3 b0 e0 b1 e1 b2 e2.
243 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
244 T4 b0 e0 b1 e1 b2 e2 b3 e3.
245 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
246 @(eq_rect_Type0 ????? e3)
247 @(R3 ????????? e0 ? e1 ? e2)
251 definition eqProp ≝ λA:Prop.eq A.
253 (* Example to avoid indexing and the consequential creation of ill typed
254 terms during paramodulation *)
255 example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
256 #A #x #h @(refl ? h: eqProp ? ? ?).
259 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
260 #T #t #P #H #p >(lemmaK T t p) @H