X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fdestruct_bb.ma;h=382620e34f23fa458a31029354c79039fca61833;hb=a6501e81dc2cae2025841cefd502c220e01cd5d8;hp=a494909f71d24084c52aa457c014b1960c5d00a2;hpb=6044e9411b4f174f382e9594fadacb40bb23c175;p=helm.git

diff --git a/helm/software/matita/tests/destruct_bb.ma b/helm/software/matita/tests/destruct_bb.ma
index a494909f7..382620e34 100644
--- a/helm/software/matita/tests/destruct_bb.ma
+++ b/helm/software/matita/tests/destruct_bb.ma
@@ -11,10 +11,45 @@
 (*        v         GNU General Public License Version 2                  *)
 (*                                                                        *)
 (**************************************************************************)
-(*
+
+include "logic/equality.ma".
+
 include "nat/nat.ma".
 include "list/list.ma".
 
+inductive list_x : Type ≝
+| nil_x  : list_x
+| cons_x : ∀T:Type.∀x:T.list_x → list_x.
+
+let rec mk_prod (l:list_x) ≝
+  match l with
+  [ nil_x ⇒ Type
+  | cons_x T x tl ⇒ ∀y0:T.∀p0:x = y0. mk_prod tl ].
+  
+let rec appl (l:list_x) : mk_prod l →  Type ≝ 
+ match l return λl:list_x.mk_prod l →Type
+ with
+ [ nil_x ⇒ λT:mk_prod nil_x.T
+ | cons_x Ty hd tl ⇒ λT:mk_prod (cons_x Ty hd tl).appl tl (T hd (refl_eq Ty hd)) ].
+  
+inductive list_xyp : list_x → Type ≝
+| nil_xyp  : ∀l.list_xyp l
+| cons_xyp : ∀l.∀T:mk_prod l.∀x:appl l T.list_xyp (cons_x ? x l) → list_xyp l.
+
+(* let rec tau (l:list_x) (w:list_xyp l) on w: Type ≝ 
+ match w with
+ [ nil_xyp _ ⇒ Type
+ | cons_xyp l' T' x' w' ⇒ 
+     ∀y:appl l' T'.∀p:x' = y.
+     tau (cons_x ? y l') w' ].
+
+eval normalize on (
+  ∀T0:Type.
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type.
+  ∀a1:T1 a0 (refl_eq ? a0).
+tau ? (cons_xyp nil_x T0 a0 (cons_xyp (cons_x T0 a0 nil_x) T1 a1 (nil_xyp ?))) Type).
+
 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.
@@ -28,31 +63,23 @@ intros 5;elim i
  |apply f1
   [rewrite > H;reflexivity
   |assumption]]]
-qed.
+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.
-  *)
-  
 definition R1 ≝ eq_rect'.
 
-
 definition R2 :
   ∀T0:Type.
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type.
   ∀a1:T1 a0 (refl_eq ? a0).
   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).  
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
   ∀e1:R1 ??? a1 ? e0 = b1.
-  ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
-intros 8;intros 2 (e1 H);
+  T2 b0 e0 b1 e1.
+intros (T0 a0 T1 a1 T2 a2);
 apply (eq_rect' ????? e1);
 apply (R1 ?? ? ?? e0);
 simplify;assumption;
@@ -66,63 +93,22 @@ definition R3 :
   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
-      ∀x2:T2 x0 p0 x1 p1.R2 ?????? p0 ? p1 a2 = x2→ Type.
+      ∀x2:T2 x0 p0 x1 p1.R2 T0 a0 T1 a1 T2 a2 ? p0 ? p1 = x2→ Type.
+  ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
   ∀e1:R1 ??? a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:R2 ?????? e0 ? e1 a2 = b2.
-  ∀so:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.
-intros 12;intros 2 (e2 H);
-apply (eq_rect' ????? e2);
-apply (R2 ?? ? ??? e0 ? e1);
-simplify;assumption;
-qed.
-
-
-
-definition r3 : ∀T0:Type.∀T1:T0 → Type.∀T2:∀t0:T0.∀t1:T1 t0.Type.
-                ∀T3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
-                ∀a0,b0:T0.∀e0:a0 = b0.
-                ∀a1:T1 a0.∀b1:T1 b0.∀e1:r1 ?? ?? e0 a1 = b1.
-                ∀a2:T2 a0 a1.∀b2:T2 b0 b1.
-                ∀e2: r2 ????? e0 ?? e1 a2 = b2.
-                T3 a0 a1 a2 → T3 b0 b1 b2.
-intros 12;intro e2;intro H;
+  ∀e2:R2 T0 a0 T1 a1 T2 a2 ? e0 ? e1 = b2.
+  T3 b0 e0 b1 e1 b2 e2.       
+intros (T0 a0 T1 a1 T2 a2 T3 a3);
 apply (eq_rect' ????? e2);
-apply (R2 ?? ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ? e0 ? e1);
+apply (R2 ?? ? ???? e0 ? e1);
 simplify;assumption;
 qed.
 
-
-apply (R2 ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ??? e0 e1);
-simplify;
-                
-                
-                
-                
-                
-  λT0:Type.λT1:T0 → Type.λT2:∀t0:T0.∀t1:T1 t0.Type.
-  λT3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
-
-  λa0,b0:T0.
-  λe0:a0 = b0.
-
-  λa1:T1 a0.λb1: T1 b0.
-  λe1:r1 ???? e0 a1 = b1.
-
-  λa2:T2 a0 a1.λb2: T2 b0 b1.
-  λe2:r2 ????? e0 ?? e1 a2 = b2.
- 
-  λso:T3 a0 a1 a2.
-  eq_rect' ?? (λy,p.T3 b0 b1 y) 
-    (eq_rect' ?? (λy,p.T3 b0 y (r2 ??? ??e0 ??p a2)) 
-       (eq_rect' T0 a0 (λy.λp:a0 = y.T3 y (r1 ?? a0 y p a1) (r2 ??? ??p  a2)) so b0 e0) 
-    ? e1)
-  ? e2.
-
-let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
+(*let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
   match n with
   [ O ⇒ Type
   | S p ⇒ match l2 with
@@ -144,7 +130,7 @@ let rec build_dep_type n T acc ≝
   [ O ⇒ acc
   | S p ⇒ 
 Type → list Type → Type.
-  λta,l.match l
+  λta,l.match l *)
 
 inductive II : nat → Type ≝
 | k1 : ∀n.II n
@@ -192,6 +178,14 @@ intros;rewrite > H;elim y;simplify;intros;
 |apply f;reflexivity]
 qed.
 
+axiom daemon:False.
+
+lemma IIconflict: ∀c,d.
+  k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
+intros;apply (IInc ??? H);clear H;intro;
+apply (eq_rect' ?? (λx.λp.∀e2:x=c.eq_rect ℕ c II (k1 c) x p=k2 x→eq_rect nat x II (k2 x) c e2 = k1 c → False) ?? e1);
+simplify;intros;apply (IInc ??? H);
+
 inductive I1 : nat → Type ≝
 | kI1 : ∀n.I1 n.
 
@@ -201,20 +195,140 @@ inductive I2 : ∀n:nat.I1 n → Type ≝
 inductive I3 : Type ≝
 | kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
 
-definition I3d: I3 → I3 → Type ≝ 
-λx,y.match x with
+(* lemma idfof : (∀t1,t2,t3,u1,u2,u3.((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.
+       λy3:I2 y1 y2.λp3:R2 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 (λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1 =y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t3 y1 p1 y2 p2 =y3.
+                    kI3 y1 y2 y3 =kI3 u1 u2 u3)
+t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)
+   t3 (refl_eq ((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)) t3)
+   )
+    → True).
+simplify; *)
+
+definition I3d : ∀x,y:I3.x = y → Type ≝
+λx,y.match x return (λx:I3.x = y → Type) with
+[ kI3 x1 x2 x3 ⇒ match y return (λy:I3.kI3 x1 x2 x3 = y → Type) with
+  [ kI3 y1 y2 y3 ⇒ 
+    λe:kI3 x1 x2 x3 = kI3 y1 y2 y3.
+       ∀P:Prop.(∀e1: x1 = y1.
+                ∀e2: R1 ?? (λz1,p1.I1 z1) ?? e1 = y2.
+                ∀e3: R2 ???? (λz1,p1,z2,p2.I2 z1 z2) x3 ? e1 ? e2 = y3. 
+                R3 ?????? 
+                (λz1,p1,z2,p2,z3,p3.
+                  eq ? (kI3 z1 z2 z3) (kI3 y1 y2 y3)) e y1 e1 y2 e2 y3 e3
+                = refl_eq ? (kI3 y1 y2 y3)
+                → P) → P]].
+
+definition I3d : ∀x,y:I3.x=y → Type.
+intros 2;cases x;cases y;intro;
+apply (∀P:Prop.(∀e1: x1 = x3.
+                ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = x4.
+                ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) i ? e1 ? e2 = i1. 
+                R3 ?????? 
+                (λy1,p1,y2,p2,y3,p3.
+                  eq ? (kI3 y1 y2 y3) (kI3 x3 x4 i1)) H x3 e1 x4 e2 i1 e3
+                = refl_eq ? (kI3 x3 x4 i1)
+                → P) → P);
+qed.
+
+(* definition I3d : ∀x,y:nat. x = y → Type ≝
+λx,y.
+match x 
+ return (λx.x = y → Type)
+ with
+[ O ⇒ match y return (λy.O = y → Type) with
+  [ O ⇒ λe:O = O.∀P.P → P
+  | S q ⇒ λe: O = S q. ∀P.P]
+| S p ⇒ match y return (λy.S p = y → Type) with
+  [ O ⇒ λe:S p = O.∀P.P
+  | S q ⇒ λe: S p = S q. ∀P.(p = q → P) → P]]. 
+
+definition I3d: 
+  ∀x,y:I3. x = y → Type 
+  ≝ 
+λx,y. 
+match x with
+[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
+  [ kI3 u1 u2 u3 ⇒ λe:kI3 t1 t2 t3 = kI3 u1 u2 u3.∀P:Type.
+    (∀e1: t1 = u1.
+     ∀e2: R1 nat t1 (λy1:nat.λp1:y1 = u1.I1 y1) t2 ? e1 = u2.
+     ∀e3: R2 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3. 
+     (* ∀e:  kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+     R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 
+        (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) e u1 e1 u2 e2 u3 e3 = refl_eq I3 (kI3 u1 u2 u3)
+     → P)
+    → P]].
+
+definition I3d: 
+  ∀x,y:I3.
+    (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+      match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]) → Type 
+  ≝ 
+λx,y.λe:
+   (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+      match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]). 
+match x with
 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
   [ kI3 u1 u2 u3 ⇒ ∀P:Type.
     (∀e1: t1 = u1.
-     ∀e2: (eq_rect ?? (λx.I1 x) t2 ? e1) = u2.
-     ∀e3: (eq_rect' ?? (λy,p.I2 u1 y)
-            (eq_rect' ?? (λy,p.I2 y (eq_rect ?? (λx.I1 x) t2 ? p)) t3 ? e1) 
-            ? e2) = u3.P) → P]].
+     ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = u2.
+     ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3. 
+     (* ∀e:  kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+     R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 
+        (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) (e (kI3 t1 t2 t3) (kI3 u1 u2 u3)) u1 e1 u2 e2 u3 e3 = refl_eq ? (kI3 u1 u2 u3)
+     → P)
+    → P]].*)
+     
+lemma I3nc : ∀a,b.∀e:a = b. I3d a b e.
+intros;apply (R1 ????? e);elim a;whd;intros;apply H;reflexivity;
+qed.
 
-lemma I3nc : ∀a,b.a = b → I3d a b.
-intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
+(*lemma R1_r : ΠA:Type.Πx:A.ΠP:Πy:A.y=x→Type.P x (refl_eq A x)→Πy:A.Πp:y=x.P y p.
+intros;lapply (eq_rect' A x P p y (sym_eq A y x p1));
+generalize in match Hletin;
+cut (∀p1:y = x.sym_eq ??? (sym_eq ??? p1) = p1)
+[rewrite > Hcut;intro;assumption
+|intro;apply (eq_rect' ????? p2);simplify;reflexivity]
 qed.
 
+definition R2_r :
+  ∀T0:Type.
+  ∀a0:T0.
+  ∀T1:∀x0:T0. x0=a0 → Type.
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:x0=a0. ∀x1:T1 x0 p0. x1 = R1_r ??? a1 ? p0 → Type.
+  ∀b0:T0.
+  ∀e0:b0 = a0.
+  ∀b1: T1 b0 e0.
+  ∀e1:b1 = R1_r ??? a1 ? e0.
+  ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
+intros 8;intros 2 (e1 H);
+apply (R1_r ????? e1);
+apply (R1_r ?? ? ?? e0);
+simplify;assumption;
+qed.*)
+
+definition I3prova : ∀a,b,c,d,e,f.∀Heq:kI3 a b c = kI3 d e f.
+  ∀P:? → ? → ? → ? → Prop.
+  P d e f Heq → 
+  P a b c (refl_eq ??).
+intros;apply (I3nc ?? Heq);
+simplify;intro;
+generalize in match H as H;generalize in match Heq as Heq;
+generalize in match f as f;generalize in match e as e;
+clear H Heq f e;
+apply (R1 ????? e1);intros 5;simplify in e2;
+generalize in match H as H;generalize in match Heq as Heq;
+generalize in match f as f;
+clear H Heq f;
+apply (R1 ????? e2);intros 4;simplify in e3;
+generalize in match H as H;generalize in match Heq as Heq;
+clear H Heq;
+apply (R1 ????? e3);intros;simplify in H1;
+apply (R1 ????? H1);
+assumption;
+qed.
+
+
 definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝
  λa,b,c,d,x,y.match x with
  [ c1 n ⇒ match y with
@@ -237,20 +351,3 @@ lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f.
 intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity;
 qed.
 
-lemma IIconflict: ∀c,d.
-  k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
-intros;apply (IInc ??? H);clear H;intro;
-apply (eq_rec ????? e1);
-intro;generalize in match e1;elim
-apply (eq_rect' ?? (λx.λp.∀e2:x=c.eq_rect ℕ c II (k1 c) x p=k2 x→eq_rect nat x II (k2 x) c e2 = k1 c → False) ?? e1);
-simplify;intro;
-apply (eq_rect' nat ? (λx.λp:c=x.k1 x = k2 x → eq_rect nat c II (k2 c) x p = k1 x → False) ?? e2);
-simplify;intro;
-
-generalize in match H1;
-apply (eq_rect' ?? (λx.λp.eq_rect ℕ c II (k1 c) x p=k2 x→False) ?? e1);
-simplify;intro;destruct;
-qed.
-
-elim e1 in H1;
-