1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/connectives.ma".
16 include "properties/relations.ma".
18 ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
21 nlemma eq_rect_Type0_r':
22 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
23 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
26 nlemma eq_rect_Type0_r:
27 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
28 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
31 nlemma eq_rect_CProp0_r':
32 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
33 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
36 nlemma eq_rect_CProp0_r:
37 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
38 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
42 ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
43 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
46 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
48 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
50 ndefinition R0 ≝ λT:Type[0].λt:T.t.
52 ndefinition R1 ≝ eq_rect_Type0.
57 ∀T1:∀x0:T0. a0=x0 → Type[0].
58 ∀a1:T1 a0 (refl ? a0).
59 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
60 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
64 ∀e1:R1 ?? T1 a1 ? e0 = b1.
66 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
67 napply (eq_rect_Type0 ????? e1);
68 napply (R1 ?? ? ?? e0);
75 ∀T1:∀x0:T0. a0=x0 → Type[0].
76 ∀a1:T1 a0 (refl ? a0).
77 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
78 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
79 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
80 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
81 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
85 ∀e1:R1 ?? T1 a1 ? e0 = b1.
87 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
89 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
90 napply (eq_rect_Type0 ????? e2);
91 napply (R2 ?? ? ???? e0 ? e1);
98 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
99 ∀a1:T1 a0 (refl T0 a0).
100 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
101 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
102 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
103 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
104 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
105 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
106 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
107 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
108 ∀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.
110 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
111 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
112 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
113 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
118 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
120 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
121 ∀b3: T3 b0 e0 b1 e1 b2 e2.
122 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
123 T4 b0 e0 b1 e1 b2 e2 b3 e3.
124 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
125 napply (eq_rect_Type0 ????? e3);
126 napply (R3 ????????? e0 ? e1 ? e2);
130 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
132 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
133 #A; napply mk_equivalence_relation
136 | #x; #y; #H; nrewrite < H; napply refl
137 | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
141 naxiom T2 : T1 → Type[0].
143 naxiom t2 : ∀x:T1. T2 x.
145 ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝
146 | i2c1 : ∀x1:T1.∀x2:T2 x1. I2 x1 x2
147 | i2c2 : I2 t1 (t2 t1).
149 (* nlemma i2d : ∀a,b.∀x,y:I2 a b.
150 ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
151 ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.
155 match x return (λr1,r2,r.
156 ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
157 ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with
161 [napply (match y return (λr1,r2,r.
162 ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
163 ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
168 (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
169 ∀f: R2 T1 x1 (λz,p.T2 z) x2
171 (i2c1 (R1 ??? z1 ? (R1 ?? (λm,n.m = y1) f1 ? p1)) ?)
172 (* (R2 ???? (λm1,n1,m2,n2.R1 ?? (λm,n.T2 m) ? ? f1 = y2) f2 ?
174 (* (R2 ???? (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
175 ? (R1 ?? (λw,q.w = y1) e1 z1 p1)
177 (λw1,q1,w2,q2.R1 ?? (λm,n.T2 m) w2 ? q1 = y2)
178 e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
180 ? y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
183 (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
184 ∀f: R2 T1 x1 (λz,p.T2 z) x2
185 (λz1,p1,z2,p2.eq (I2 y1 y2)
186 (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
187 y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1)
188 y2 (R2 T1 x1 (λw,q.w = y1) e1
189 (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
191 e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
196 ndefinition i2d : ∀a,b.∀x,y:I2 a b.
197 ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
198 ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝
200 match x return (λr1,r2,r.
201 ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
202 ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with
204 match y return (λr1,r2,r.
205 ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
206 ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
207 [ i2c1 y1 y2 ⇒ λe1,e2,e.∀P:Type[1].
208 (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
209 ∀f: R2 T1 x1 (λz,p.T2 z) x2
210 (λz1,p1,z2,p2.eq (I2 y1 y2)
211 (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
212 y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1)
213 y2 (R2 T1 x1 (λw,q.w = y1) e1
214 (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
216 e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
218 | i2c2 ⇒ λe1,e2,e.∀P:Type[1].P ]
220 match y return (λr1,r2,r.
221 ∀e1: x1 = r1. ∀e2: R1 ?? (λz,p. T2 z) x2 ? e1 = r2.
222 ∀e : R2 ???? (λz1,p1,z2,p2. I2 z1 z2) i2c2 ? e1 ? e2 = r. Type[2]) with
223 [ i2c1 _ _ ⇒ λe1,e2,e.∀P:Type[1].P
224 | i2c2 ⇒ λe1,e2,e.∀P:Type[1].
226 (λz1,p1,z2,p2.eq ? i2c2 i2c2)
227 e ? e1 ? e2 = refl ? i2c2.P) → P ] ].