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/equality.ma".
17 (* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
18 ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
22 ndefinition R0 ≝ λT:Type[0].λt:T.t.
24 ndefinition R1 ≝ eq_rect_Type0.
29 ∀T1:∀x0:T0. a0=x0 → Type[0].
30 ∀a1:T1 a0 (refl ? a0).
31 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
32 ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
36 ∀e1:R1 ?? T1 a1 ? e0 = b1.
38 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
39 napply (eq_rect_Type0 ????? e1);
40 napply (R1 ?? ? ?? e0);
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).
51 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
52 ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
53 ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
57 ∀e1:R1 ?? T1 a1 ? e0 = b1.
59 ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
61 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
62 napply (eq_rect_Type0 ????? e2);
63 napply (R2 ?? ? ???? e0 ? e1);
67 (* include "nat/nat.ma".
69 ninductive nlist : nat → Type[0] ≝
71 | ncons : ∀n:nat.nat → nlist n → nlist (S n).
73 ninductive wrapper : Type[0] ≝
74 | kw1 : ∀x.∀y:nlist x.wrapper
75 | kw2 : ∀x.∀y:nlist x.wrapper.
77 nlemma fie : ∀a,b,c,d.∀e:eq ? (kw1 a b) (kw1 c d).
78 ∀P:(∀x1.∀x2:nlist x1. ∀y1.∀y2:nlist y1.eq ? (kw1 x1 x2) (kw1 y1 y2) → Prop).
79 P a b a b (refl ??) → P a b c d e.
80 #a;#b;#c;#d;#e;#P;#HP;
84 (* nsubst E; purtroppo al momento funziona solo nel verso sbagliato *)
91 ninductive I1 : Type[0] ≝
94 ninductive I2 : I1 → Type[0] ≝
97 ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
100 ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
101 | k4 : ∀x,y.∀z:I3 x y.I4 x y z.
103 (*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
104 alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
109 ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
110 ∀a1:T1 a0 (refl T0 a0).
111 ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
112 ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
113 ∀T3:∀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.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
115 ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
116 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
117 ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
118 ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
119 ∀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.
121 ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
122 a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
123 a3 (refl (T3 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))
129 ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
131 ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
132 ∀b3: T3 b0 e0 b1 e1 b2 e2.
133 ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
134 T4 b0 e0 b1 e1 b2 e2 b3 e3.
135 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
136 napply (eq_rect_Type0 ????? e3);
137 napply (R3 ????????? e0 ? e1 ? e2);
142 ninductive II : Type[0] ≝
143 | kII1 : ∀x,y,z.∀w:I4 x y z.II
144 | kII2 : ∀x,y,z.∀w:I4 x y z.II.
146 (* nlemma foo : ∀a,b,c,d,e,f,g,h. kII1 a b c d = kII2 e f g h → True.
147 #a;#b;#c;#d;#e;#f;#g;#h;#H;
151 nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
152 ∀P:(∀a,b,c,d.kII1 a b c d = kII1 e f g h → Prop).
153 P e f g h (refl ??) → P a b c d Heq.
154 #a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;