...

[helm.git] / helm / software / matita / nlibrary / logic / destruct_bb.ma

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index 49a03ff0f1b79bc3252f806c97ca86ed320f61e1..308f8bebeb91ed3b554cca708bb4e6fbd0eb1124 100644 (file)
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -14,79 +14,17 @@
 
 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.
+ninductive unit: Type[0] ≝ k: unit.
 
-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 ?? 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 ?? 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 a2;
-nqed.
+ninductive bool: unit → Type[0] ≝ true : bool k | false : bool k.
 
-ndefinition R3 :
-  ∀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 ?? 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 ?? 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 ?? T1 a1 ? e0 = b1.
-  ∀b2: T2 b0 e0 b1 e1.
-  ∀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 a3;
+nlemma foo: true = false → False. #H; ndestruct;
 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.*) 
-
-(***************)
+(* 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;*)
 
 ninductive I1 : Type[0] ≝
 | k1 : I1.
@@ -103,42 +41,6 @@ ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
 (*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.
@@ -154,4 +56,4 @@ nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
 #a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;
 ndestruct;
 napply HP;
-nqed.
+nqed.
\ No newline at end of file