the attempt of completing dama using duality frozen

[helm.git] / helm / software / matita / contribs / dama / dama / lattice.ma

diff --git a/helm/software/matita/contribs/dama/dama/lattice.ma b/helm/software/matita/contribs/dama/dama/lattice.ma
index 78046c688ead8c5561ad629785fce67f98ea52c1..adf751b8302c979bccb3d38e401546f40dd691b0 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lattice.ma
+++ b/helm/software/matita/contribs/dama/dama/lattice.ma
@@ -185,9 +185,6 @@ definition hole ≝ λT:Type.λx:T.x.
 notation < "\ldots" non associative with precedence 50 for @{'hole}.
 interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _).
 
-
-axiom FALSE : False.
-
 (* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
 lemma subst_excess: 
   ∀l:semi_lattice.
@@ -340,15 +337,56 @@ apply (subst_excess sl);
   [apply (subst_excess_base_in_excess sl eb H H1 H2);
   |apply subst_excess_base_in_excess_preserves_apartness;
   |change in ⊢ (%→%→?) with ((λx.ap_carr x) (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)); simplify;
-   intros 3 (x y LE);
-   generalize in match (H3 ?? LE);
-   generalize in match H1 as H1;generalize in match H2 as H2; 
+   intros 3 (x y LE); clear H3 LE;
    generalize in match x as x; generalize in match y as y;
-   cases FALSE;
-   (*
-   (reduce in H ⊢ %; cases H; simplify; intros; assumption); 
+   generalize in match H1 as H1;generalize in match H2 as H2;
+   clear x y H1 H2 H4; STOP
+ 
+   apply (match H return λr:Type.λm:Type_OF_semi_lattice sl=r.
+   ∀H2:(Πy2:exc_carr eb
+               .Πx2:exc_carr eb
+                .Or (exc_excess eb y2 x2) (exc_excess eb x2 y2)
+                 →match H
+                     in eq
+                     return 
+                    λright_1:Type
+                    .(λmatched:eq Type (Type_OF_semi_lattice sl) right_1
+                      .right_1→right_1→Type)
+                     with 
+                    [refl_eq⇒ap_apart (apartness_OF_semi_lattice sl)] y2 x2)
+.∀H1:Πy1:exc_carr eb
+               .Πx1:exc_carr eb
+                .match H
+                  in eq
+                  return 
+                 λright_1:Type
+                 .(λmatched:eq Type (Type_OF_semi_lattice sl) right_1
+                   .right_1→right_1→Type)
+                  with 
+                 [refl_eq⇒ap_apart (apartness_OF_semi_lattice sl)] y1 x1
+                 →Or (exc_excess eb y1 x1) (exc_excess eb x1 y1)
+ .∀y:ap_carr
+              (apartness_OF_excess (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2))
+  .∀x:ap_carr
+               (apartness_OF_excess
+                (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2))
+   .eq
+    (apartness_OF_excess (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)) x
+    (match 
+     subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2
+      in eq
+      return 
+     λright_1:apartness
+     .(λmatched:eq apartness (apartness_OF_semi_lattice sl) right_1
+       .ap_carr right_1→ap_carr right_1→ap_carr right_1)
+      with 
+     [refl_eq⇒sl_meet sl] x y)
+   
+   with [ refl_eq ⇒ ?]);
    
    
+   cases (subst_excess_base_in_excess_preserves_apartness sl eb H H1 H2);
+   cases H;
    cases (subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2); simplify;
    change in x:(%) with (exc_carr eb);
    change in y:(%) with (exc_carr eb);