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_CProp0_r':
22 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
23 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
26 nlemma eq_rect_CProp0_r:
27 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
28 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
32 ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
36 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
38 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
40 ndefinition R0 ≝ λT:Type[0].λt:T.t.
42 ndefinition R1 ≝ eq_rect_Type0.
47 ∀T1:∀x0:T0. a0=x0 → Type[0].
48 ∀a1:T1 a0 (refl ? a0).
49 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
50 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
54 ∀e1:R1 ?? T1 a1 ? e0 = b1.
56 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
57 napply (eq_rect_Type0 ????? e1);
58 napply (R1 ?? ? ?? e0);
65 ∀T1:∀x0:T0. a0=x0 → Type[0].
66 ∀a1:T1 a0 (refl ? a0).
67 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
68 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
69 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
70 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
71 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
75 ∀e1:R1 ?? T1 a1 ? e0 = b1.
77 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
79 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
80 napply (eq_rect_Type0 ????? e2);
81 napply (R2 ?? ? ???? e0 ? e1);
88 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
89 ∀a1:T1 a0 (refl T0 a0).
90 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
91 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
92 ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
93 ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
94 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
95 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
96 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
97 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
98 ∀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.
100 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
101 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
102 a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
103 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
108 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
110 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
111 ∀b3: T3 b0 e0 b1 e1 b2 e2.
112 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
113 T4 b0 e0 b1 e1 b2 e2 b3 e3.
114 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
115 napply (eq_rect_Type0 ????? e3);
116 napply (R3 ????????? e0 ? e1 ? e2);
120 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
121 #A; napply mk_equivalence_relation
124 | #x; #y; #H; nrewrite < H; napply refl
125 | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]