(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-(*
-include "nat/nat.ma".
-include "list/list.ma".
-
-inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
-| il_s : ∀n.T n → index_list T n n
-| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
-
-lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
- ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
-intros 5;elim i
-[destruct;apply il_s;apply f;assumption
-|apply il_c
- [apply f;rewrite > H;assumption
- |apply f1
- [rewrite > H;reflexivity
- |assumption]]]
-qed.
-
-definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
- λT0:Type.λT1:T0 → Type.
- λa0,b0:T0.
- λe0:a0 = b0.
- λso:T1 a0.
- eq_rect' ?? (λy,p.T1 y) so ? e0.
- *)
include "logic/equality.ma".
+
+(* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
+ ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
+#T;#a;#b;#e;#P;#H;
+nrewrite < e;*)
+
+ndefinition R0 ≝ λT:Type[0].λt:T.t.
ndefinition R1 ≝ eq_rect_Type0.
+
ndefinition R2 :
∀T0:Type[0].
∀a0:T0.
∀T1:∀x0:T0. a0=x0 → Type[0].
∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+ ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
∀b0:T0.
∀e0:a0 = b0.
∀b1: T1 b0 e0.
- ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
- ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
-#T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ T2 b0 e0 b1 e1.
+#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
napply (eq_rect_Type0 ????? e1);
napply (R1 ?? ? ?? e0);
-napply H;
+napply a2;
nqed.
ndefinition R3 :
∀a0:T0.
∀T1:∀x0:T0. a0=x0 → Type[0].
∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
- ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
- ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
+ ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+ ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+ ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
∀b0:T0.
∀e0:a0 = b0.
∀b1: T1 b0 e0.
- ∀e1:R1 ? a0 ? a1 ? e0 = b1.
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
∀b2: T2 b0 e0 b1 e1.
- ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
- ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
+ ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+ T3 b0 e0 b1 e1 b2 e2.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ??? e0 ? e1);
-napply H;
-nqed.
\ No newline at end of file
+napply (R2 ?? ? ???? e0 ? e1);
+napply a3;
+nqed.
+
+(* include "nat/nat.ma".
+
+ninductive nlist : nat → Type[0] ≝
+| nnil : nlist O
+| ncons : ∀n:nat.nat → nlist n → nlist (S n).
+
+ninductive wrapper : Type[0] ≝
+| kw1 : ∀x.∀y:nlist x.wrapper
+| kw2 : ∀x.∀y:nlist x.wrapper.
+
+nlemma fie : ∀a,b,c,d.∀e:eq ? (kw1 a b) (kw1 c d).
+ ∀P:(∀x1.∀x2:nlist x1. ∀y1.∀y2:nlist y1.eq ? (kw1 x1 x2) (kw1 y1 y2) → Prop).
+ P a b a b (refl ??) → P a b c d e.
+#a;#b;#c;#d;#e;#P;#HP;
+ndiscriminate e;#e0;
+nsubst e0;#e1;
+nsubst e1;#E;
+(* nsubst E; purtroppo al momento funziona solo nel verso sbagliato *)
+nrewrite > E;
+napply HP;
+nqed.*)
+
+(***************)
+
+ninductive I1 : Type[0] ≝
+| k1 : I1.
+
+ninductive I2 : I1 → Type[0] ≝
+| k2 : ∀x.I2 x.
+
+ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
+| k3 : ∀x,y.I3 x y.
+
+ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
+| k4 : ∀x,y.∀z:I3 x y.I4 x y z.
+
+(*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
+alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
+
+ndefinition R4 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+ ∀a1:T1 a0 (refl T0 a0).
+ ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+ ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+ ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+ ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
+ ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ ∀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.
+ Type[0].
+ ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
+ a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+ a3).
+ ∀b0:T0.
+ ∀e0:eq (T0 …) a0 b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+ ∀b2: T2 b0 e0 b1 e1.
+ ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+ ∀b3: T3 b0 e0 b1 e1 b2 e2.
+ ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+ T4 b0 e0 b1 e1 b2 e2 b3 e3.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+napply (eq_rect_Type0 ????? e3);
+napply (R3 ????????? e0 ? e1 ? e2);
+napply a4;
+nqed.
+
+
+ninductive II : Type[0] ≝
+| kII1 : ∀x,y,z.∀w:I4 x y z.II
+| kII2 : ∀x,y,z.∀w:I4 x y z.II.
+
+(* nlemma foo : ∀a,b,c,d,e,f,g,h. kII1 a b c d = kII2 e f g h → True.
+#a;#b;#c;#d;#e;#f;#g;#h;#H;
+ndiscriminate H;
+nqed. *)
+
+nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
+ ∀P:(∀a,b,c,d.kII1 a b c d = kII1 e f g h → Prop).
+ P e f g h (refl ??) → P a b c d Heq.
+#a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;
+ndestruct;
+napply HP;
+nqed.
projects / helm.git / blobdiff