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.
34 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
35 #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
36 ncases p0; #Heq; nassumption.
40 ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
41 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
44 ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
45 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
46 ##[ @; ##| nassumption; ##]
49 ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
50 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
53 ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
54 #A; #B; #Ha; #Heq;nelim Heq; nassumption.
57 ndefinition R0 ≝ λT:Type[0].λt:T.t.
59 ndefinition R1 ≝ eq_rect_Type0.
64 ∀T1:∀x0:T0. a0=x0 → Type[0].
65 ∀a1:T1 a0 (refl ? a0).
66 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
67 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
71 ∀e1:R1 ?? T1 a1 ? e0 = b1.
73 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
74 napply (eq_rect_Type0 ????? e1);
75 napply (R1 ?? ? ?? e0);
82 ∀T1:∀x0:T0. a0=x0 → Type[0].
83 ∀a1:T1 a0 (refl ? a0).
84 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
85 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
86 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
87 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
88 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
92 ∀e1:R1 ?? T1 a1 ? e0 = b1.
94 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
96 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
97 napply (eq_rect_Type0 ????? e2);
98 napply (R2 ?? ? ???? e0 ? e1);
105 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
106 ∀a1:T1 a0 (refl T0 a0).
107 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
108 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
109 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
110 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
111 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
112 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
113 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
114 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
115 ∀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.
117 ∀a4:T4 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 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
120 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
125 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
127 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
128 ∀b3: T3 b0 e0 b1 e1 b2 e2.
129 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
130 T4 b0 e0 b1 e1 b2 e2 b3 e3.
131 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
132 napply (eq_rect_Type0 ????? e3);
133 napply (R3 ????????? e0 ? e1 ? e2);
137 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.