1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "logic/pts.ma".
17 inductive eq (A:Type[2]) (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[0]. P a (refl A a) → P x p.
24 #A #a #x #p cases p #P #H assumption.
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 apply (eq_rect_r ? ? ? p0) assumption.
32 lemma eq_rect_Type2_r :
33 ∀A:Type[0].∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
34 #A #a #P #H #x #p generalize in match H generalize in match P
40 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
41 #A #a #P #p #x0 #p0 ngeneralize in match p
42 ncases p0 #Heq nassumption.
46 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
47 #A #x #P #Hx #y #Heq cases Heq assumption.
50 theorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
51 #A #x #y #Heq apply (rewrite_l A x (λz.z=x))
55 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
56 #A #x #P #Hx #y #Heq cases (sym_eq ? ? ?Heq) assumption.
59 theorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
60 #A #B #Ha #Heq elim Heq assumption.
63 definition R0 ≝ λT:Type[0].λt:T.t.
65 definition R1 ≝ eq_rect_Type0.
70 ∀T1:∀x0:T0. a0=x0 → Type[0].
71 ∀a1:T1 a0 (refl ? a0).
72 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
73 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
77 ∀e1:R1 ?? T1 a1 ? e0 = b1.
79 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
80 apply (eq_rect_Type0 ????? e1)
88 ∀T1:∀x0:T0. a0=x0 → Type[0].
89 ∀a1:T1 a0 (refl ? a0).
90 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
91 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
92 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
93 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
94 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
98 ∀e1:R1 ?? T1 a1 ? e0 = b1.
100 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
101 T3 b0 e0 b1 e1 b2 e2.
102 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
103 apply (eq_rect_Type0 ????? e2)
104 apply (R2 ?? ? ???? e0 ? e1)
111 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
112 ∀a1:T1 a0 (refl T0 a0).
113 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
114 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
115 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
116 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
117 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
118 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
119 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
120 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
121 ∀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.
123 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
124 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
125 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
126 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
131 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
133 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
134 ∀b3: T3 b0 e0 b1 e1 b2 e2.
135 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
136 T4 b0 e0 b1 e1 b2 e2 b3 e3.
137 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
138 apply (eq_rect_Type0 ????? e3)
139 apply (R3 ????????? e0 ? e1 ? e2)
143 axiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.