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 ninductive 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. P a (refl A a) → P x p.
24 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
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; napply (eq_rect_r ? ? ? p0); nassumption.
32 nlemma eq_rect_Type2_r :
33 ∀A:Type.∀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;ngeneralize in match H;ngeneralize 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 ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
47 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
50 ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
51 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
52 ##[ @; ##| nassumption; ##]
55 ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
56 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
59 ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
60 #A; #B; #Ha; #Heq;nelim Heq; nassumption.
63 ndefinition R0 ≝ λT:Type[0].λt:T.t.
65 ndefinition 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 napply (eq_rect_Type0 ????? e1);
81 napply (R1 ?? ? ?? e0);
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 napply (eq_rect_Type0 ????? e2);
104 napply (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 napply (eq_rect_Type0 ????? e3);
139 napply (R3 ????????? e0 ? e1 ? e2);
143 naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.