very bad bug found, asert false in cicReduction when a clear is performed

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 79bc27ee194ab8091b26acc3a805094b005e0261..96252c6ee9c6bb75bb6161c7951b2f35c1669dca 100644 (file)
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -216,76 +216,39 @@ lemma subst_excess_base_in_semi_lattice:
   ∀sl:semi_lattice.
   ∀eb:excess_base.
   ∀p:exc_carr sl = exc_carr eb.
-  
-  mancano le 4 proprietà riscritte con p
-    
+  (∀y1,x1:eb. (?(ap_apart sl)) y1  x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
+  (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 →  (?(ap_apart sl)) y2 x2) →
+  (∀x3,y3:eb.(le eb) x3 y3 → (?(ap_apart sl)) x3 ((?(sl_meet sl)) x3 y3)) →
+  (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) → 
   semi_lattice.
-intros (l eb H); apply (subst_excess l);
-  [apply (subst_excess_ l);
-    [apply (subst_dual_excess l);
-      [apply (subst_excess_base l eb);
+[2,3,7,9,10: apply Type|4:apply (exc_carr eb);
+|1,5,6,8,11: intro f; cases p; apply f;]
+intros (sl eb H H1 H2 H3 H4); apply (subst_excess sl);
+  [apply (subst_excess_ sl);
+    [apply (subst_dual_excess sl);
+      [apply (subst_excess_base sl eb);
       |apply H;]
-    | change in \vdash (% -> % -> ?) with (exc_carr eb);
-    letin xxx \def (ap2exc l); clearbody xxx;
-    change in xxx:(%→%→?) with (Type_OF_semi_lattice l);
-    whd in ⊢ (?→?→? (? %) ? ?→?); 
-    unfold exc_ap;
-    simplify in ⊢ (?→?→%→?);
-
-intros 2;
-generalize in ⊢ (% -> ?); intro P;
-generalize in match x in ⊢ % as x;
-generalize in match y in ⊢ % as y; clear x y;
-
+    | (*clear H2 H3 H4;*) 
+      change in ⊢ (% -> % -> ?) with (exc_carr eb);
+      unfold subst_excess_base; unfold mk_excess_dual_smart;
+      unfold subst_dual_excess; simplify in ⊢ (?→?→?→%);
+      (unfold exc_ap; simplify in ⊢ (?→?→? % ? ?→?));
+      simplify; intros (x y H2); apply H1;
+      generalize in match H2;
+      generalize in match x as x;
+      generalize in match y as y; (*clear H1 H2 x y;*)
+      change in ⊢ (?→?→match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?→?)
+      with (Type_OF_semi_lattice sl); 
+      change in ⊢ (?→?→match match ? return λ_:?.(λ_:? ? % ?.? ? % ?) with [_⇒? ? %] return ? with [_⇒?] ??→?) with (Type_OF_semi_lattice sl);
+      cases H; intros; assumption; (* se faccio le clear... BuM! *)
+    | clear H1 H3 H4;
     
-cases H; simplify;
-
-
-cut (Πy:exc_carr eb
-.Πx:exc_carr eb
- .match 
-  (match H
-   in eq
-   return 
-  λright_1:Type
-  .(λmatched:eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1
-    .eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1)
-   with 
-  [refl_eq⇒refl_eq Type (Type_OF_excess_ (excess__OF_semi_lattice l))])
-   in eq
-   return 
-  λright_1:Type
-  .(λmatched:eq Type (ap_carr (exc_ap (excess__OF_semi_lattice l))) right_1
-    .right_1→right_1→Type)
-   with 
-  [refl_eq⇒ap_apart (exc_ap (excess__OF_semi_lattice l))] y x);[2:
-  
-
-    change in ⊢ (?→?→? % ? ?→?) with (exc_ap_ (excess__OF_semi_lattice l));
-    generalize in match H in \vdash (? -> %); cases H;  
-    cases H;
-    
-    
-normalize in ⊢ (?→?→?→? (? (? (? ? (% ? ?) ?)) ? ?) ?);
-whd in ⊢ (?→?→? % ? ?→?); change in ⊢ (?→?→? (? % ? ? ? ?) ? ?→?) with (exc_carr eb);
-cases H;
-      change in ⊢ (?→?→? % ? ?→?) with (exc_ap l);
-(subst_dual_excess (excess__OF_semi_lattice l)
- (subst_excess_base (excess_dual_OF_semi_lattice l) eb) H)
-      
-      
-       unfold subst_excess_base;
-        unfold mk_excess_dual_smart;
-        unfold excess__OF_semi_lattice;
-        unfold excess_dual_OF_semi_lattice;
-        unfold excess_dual_OF_semi_lattice;
-        
-      reflexivity]
-*)
+    ]
 
 record lattice_ : Type ≝ {
   latt_mcarr:> semi_lattice;
   latt_jcarr_: semi_lattice;
+  (*latt_with1: latt_jcarr_ = subst latt_jcarr (exc_dual_dual latt_mcarr)*) 
 (*  latt_with1:   (subst_excess_
                   (subst_dual_excess
                     (subst_excess_base