snopshot before isabellization

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 55f531a9b53f7ff5016d16b42323cfa914555bb8..0f236dd06a3ea4b3463740b52be6f23d9620086d 100644 (file)
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -258,3 +258,10 @@ qed.
 
 definition total_order_property : ∀E:excess. Type ≝
   λE:excess. ∀a,b:E. a ≰ b → b < a.
+
+lemma dual_exc: excess→ excess.
+intro E; apply mk_excess; 
+[apply (exc_carr E);|apply (λx,y:E.y≰x);|apply exc_coreflexive;
+|unfold cotransitive; simplify;intros;cases (exc_cotransitive E ??z e);
+  [right|left]assumption]
+qed.

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index fcad3fdc54dc227e4ea3cbd9c3ac7665db07b831..1f605c257e2e13820be92d875ab5249da7cb09a0 100644 (file)
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -14,34 +14,33 @@
 
 include "excess.ma".
 
-record lattice_ : Type ≝ {
-  l_carr: apartness;
-  l_meet: l_carr → l_carr → l_carr;
-  l_meet_refl: ∀x.l_meet x x ≈ x;  
-  l_meet_comm: ∀x,y:l_carr. l_meet x y ≈ l_meet y x;
-  l_meet_assoc: ∀x,y,z:l_carr. l_meet x (l_meet y z) ≈ l_meet (l_meet x y) z;
-  l_strong_extm: ∀x.strong_ext ? (l_meet x)  
+record directed : Type ≝ {
+  dir_carr: apartness;
+  dir_op: dir_carr → dir_carr → dir_carr;
+  dir_op_refl: ∀x.dir_op x x ≈ x;  
+  dir_op_comm: ∀x,y:dir_carr. dir_op x y ≈ dir_op y x;
+  dir_op_assoc: ∀x,y,z:dir_carr. dir_op x (dir_op y z) ≈ dir_op (dir_op x y) z;
+  dir_strong_extop: ∀x.strong_ext ? (dir_op x)  
 }.
 
-definition excl ≝ λl:lattice_.λa,b:l_carr l.ap_apart (l_carr l) a (l_meet l a b).
+definition excl ≝ 
+  λl:directed.λa,b:dir_carr l.ap_apart (dir_carr l) a (dir_op l a b).
 
-lemma excess_of_lattice_: lattice_ → excess.
-intro l; apply (mk_excess (l_carr l) (excl l));
-[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive (l_carr l) x);
-  apply (ap_rewr ??? (l_meet l x x) (l_meet_refl ? x)); assumption;
+lemma excess_of_directed: directed → excess.
+intro l; apply (mk_excess (dir_carr l) (excl l));
+[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive (dir_carr l) x);
+  apply (ap_rewr ??? (dir_op l x x) (dir_op_refl ? x)); assumption;
 | intros 3 (x y z); unfold excl; intro H;
-  cases (ap_cotransitive ??? (l_meet l (l_meet l x z) y) H) (H1 H2); [2:
-    left; apply ap_symmetric; apply (l_strong_extm ? y); 
-    apply (ap_rewl ???? (l_meet_comm ???));
-    apply (ap_rewr ???? (l_meet_comm ???));
+  cases (ap_cotransitive ??? (dir_op l (dir_op l x z) y) H) (H1 H2); [2:
+    left; apply ap_symmetric; apply (dir_strong_extop ? y); 
+    apply (ap_rewl ???? (dir_op_comm ???));
+    apply (ap_rewr ???? (dir_op_comm ???));
     assumption]
-  cases (ap_cotransitive ??? (l_meet l x z) H1) (H2 H3); [left; assumption]
-  right; apply (l_strong_extm ? x); apply (ap_rewr ???? (l_meet_assoc ????));
+  cases (ap_cotransitive ??? (dir_op l x z) H1) (H2 H3); [left; assumption]
+  right; apply (dir_strong_extop ? x); apply (ap_rewr ???? (dir_op_assoc ????));
   assumption]
 qed.    
 
-(* coercion cic:/matita/lattice/excess_of_lattice_.con. *)
-
 record prelattice : Type ≝ {
   pl_carr:> excess;
   meet: pl_carr → pl_carr → pl_carr;
@@ -53,8 +52,8 @@ record prelattice : Type ≝ {
   lem: ∀x,y.(meet x y) ≤ y 
 }.
  
-interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattice/meet.con _ a b).
+interpretation "prelattice meet" 'and a b =
+  (cic:/matita/lattice/meet.con _ a b).
 
 lemma feq_ml: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
@@ -67,87 +66,117 @@ apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
 apply feq_ml; assumption;
 qed.
  
-lemma prelattice_of_lattice_: lattice_ → prelattice.
-intro l_; apply (mk_prelattice (excess_of_lattice_ l_)); [apply (l_meet l_);]
-unfold excess_of_lattice_; try unfold apart_of_excess; simplify;
+lemma prelattice_of_directed: directed → prelattice.
+intro l_; apply (mk_prelattice (excess_of_directed l_)); [apply (dir_op l_);]
+unfold excess_of_directed; try unfold apart_of_excess; simplify;
 unfold excl; simplify;
 [intro x; intro H; elim H; clear H; 
- [apply (l_meet_refl l_ x); 
-  lapply (Ap≫ ? (l_meet_comm ???) t) as H; clear t; 
-  lapply (l_strong_extm l_ ??? H); apply ap_symmetric; assumption
- | lapply (Ap≪ ? (l_meet_refl ?x) t) as H; clear t;
-   lapply (l_strong_extm l_ ??? H); apply (l_meet_refl l_ x);
+ [apply (dir_op_refl l_ x); 
+  lapply (Ap≫ ? (dir_op_comm ???) t) as H; clear t; 
+  lapply (dir_strong_extop l_ ??? H); apply ap_symmetric; assumption
+ | lapply (Ap≪ ? (dir_op_refl ?x) t) as H; clear t;
+   lapply (dir_strong_extop l_ ??? H); apply (dir_op_refl l_ x);
    apply ap_symmetric; assumption]
 |intros 3 (x y H); cases H (H1 H2); clear H;
- [lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ x y)) H1) as H; clear H1;
-  lapply (l_strong_extm l_ ??? H) as H1; clear H;
-  lapply (Ap≪ ? (l_meet_comm ???) H1); apply (ap_coreflexive ?? Hletin);
- |lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ y x)) H2) as H; clear H2;
-  lapply (l_strong_extm l_ ??? H) as H1; clear H;
-  lapply (Ap≪ ? (l_meet_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
+ [lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ x y)) H1) as H; clear H1;
+  lapply (dir_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (dir_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
+ |lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ y x)) H2) as H; clear H2;
+  lapply (dir_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (dir_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
 |intros 4 (x y z H); cases H (H1 H2); clear H;
- [lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ x (l_meet l_ y z))) H1) as H; clear H1;
-  lapply (l_strong_extm l_ ??? H) as H1; clear H;
-  lapply (Ap≪ ? (eq_sym ??? (l_meet_assoc ?x y z)) H1) as H; clear H1;
+ [lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ x (dir_op l_ y z))) H1) as H; clear H1;
+  lapply (dir_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (eq_sym ??? (dir_op_assoc ?x y z)) H1) as H; clear H1;
   apply (ap_coreflexive ?? H);
- |lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ (l_meet l_ x y) z)) H2) as H; clear H2;
-  lapply (l_strong_extm l_ ??? H) as H1; clear H;
-  lapply (Ap≪ ? (l_meet_assoc ?x y z) H1) as H; clear H1;
+ |lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ (dir_op l_ x y) z)) H2) as H; clear H2;
+  lapply (dir_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (dir_op_assoc ?x y z) H1) as H; clear H1;
   apply (ap_coreflexive ?? H);]
 |intros (x y z H); elim H (H1 H1); clear H;
- lapply (Ap≪ ? (l_meet_refl ??) H1) as H; clear H1;
- lapply (l_strong_extm l_ ??? H) as H1; clear H;
- lapply (l_strong_extm l_ ??? H1) as H; clear H1;
- cases (ap_cotransitive ??? (l_meet l_ y z) H);[left|right|right|left] try assumption;
- [apply ap_symmetric;apply (Ap≪ ? (l_meet_comm ???));
- |apply (Ap≫ ? (l_meet_comm ???));
+ lapply (Ap≪ ? (dir_op_refl ??) H1) as H; clear H1;
+ lapply (dir_strong_extop l_ ??? H) as H1; clear H;
+ lapply (dir_strong_extop l_ ??? H1) as H; clear H1;
+ cases (ap_cotransitive ??? (dir_op l_ y z) H);[left|right|right|left] try assumption;
+ [apply ap_symmetric;apply (Ap≪ ? (dir_op_comm ???));
+ |apply (Ap≫ ? (dir_op_comm ???));
  |apply ap_symmetric;] assumption;
 |intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
- lapply (Ap≪ ? (l_meet_refl ??) H) as H1; clear H;
- lapply (l_strong_extm l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
+ lapply (Ap≪ ? (dir_op_refl ??) H) as H1; clear H;
+ lapply (dir_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
  assumption
 |intros 3 (x y H); 
- cut (l_meet l_ x y ≈ l_meet l_ x (l_meet l_ y y)) as H1;[2:
-   intro; lapply (l_strong_extm ???? a); apply (l_meet_refl l_ y);
+ cut (dir_op l_ x y ≈ dir_op l_ x (dir_op l_ y y)) as H1;[2:
+   intro; lapply (dir_strong_extop ???? a); apply (dir_op_refl l_ y);
    apply ap_symmetric; assumption;]
- lapply (Ap≪ ? (eq_sym ??? H1) H); apply (l_meet_assoc l_ x y y);
+ lapply (Ap≪ ? (eq_sym ??? H1) H); apply (dir_op_assoc l_ x y y);
  assumption; ]
 qed.
 
-record lattice : Type ≝ {
-  lat_carr:> prelattice; 
-  join: lat_carr → lat_carr → lat_carr;   
-  join_refl: ∀x.join x x ≈ x;
-  join_comm: ∀x,y:lat_carr. join x y ≈ join y x;
-  join_assoc: ∀x,y,z:lat_carr. join x (join y z) ≈ join (join x y) z;
-  absorbjm: ∀f,g:lat_carr. join f (meet ? f g) ≈ f;
-  absorbmj: ∀f,g:lat_carr. meet ? f (join f g) ≈ f;
-  strong_extj: ∀x.strong_ext ? (join x)
+record lattice_ : Type ≝ {
+  latt_mcarr:> prelattice;
+  latt_jcarr_: prelattice;
+  latt_with: pl_carr latt_jcarr_ = dual_exc (pl_carr latt_mcarr)
 }.
 
+lemma latt_jcarr : lattice_ → prelattice.
+intro l;
+apply (mk_prelattice (dual_exc l)); unfold excess_OF_lattice_;
+cases (latt_with l); simplify;
+[apply meet|apply meet_refl|apply meet_comm|apply meet_assoc|
+apply strong_extm| apply le_to_eqm|apply lem]
+qed. 
+ 
+coercion cic:/matita/lattice/latt_jcarr.con.
+
+interpretation "Lattice meet" 'and a b =
+ (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).  
+
 interpretation "Lattice join" 'or a b =
- (cic:/matita/lattice/join.con _ a b).  
+ (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).  
 
-lemma feq_jl: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∨ a) ≈ (c ∨ b).
-intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
-intro H1; apply H; clear H; apply (strong_extj ???? H1);
-qed.
+record lattice : Type ≝ {
+  latt_carr:> lattice_;
+  absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
+  absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
+}.
 
-lemma feq_jr: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (a ∨ c) ≈ (b ∨ c).
-intros (l a b c H); apply (Eq≈ ? (join_comm ???)); apply (Eq≈ ?? (join_comm ???));
-apply (feq_jl ???? H);
-qed.
+notation "'meet'"        non associative with precedence 50 for @{'meet}.
+notation "'meet_refl'"   non associative with precedence 50 for @{'meet_refl}.
+notation "'meet_comm'"   non associative with precedence 50 for @{'meet_comm}.
+notation "'meet_assoc'"  non associative with precedence 50 for @{'meet_assoc}.
+notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
+notation "'le_to_eqm'"   non associative with precedence 50 for @{'le_to_eqm}.
+notation "'lem'"         non associative with precedence 50 for @{'lem}.
+notation "'join'"        non associative with precedence 50 for @{'join}.
+notation "'join_refl'"   non associative with precedence 50 for @{'join_refl}.
+notation "'join_comm'"   non associative with precedence 50 for @{'join_comm}.
+notation "'join_assoc'"  non associative with precedence 50 for @{'join_assoc}.
+notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
+notation "'le_to_eqj'"   non associative with precedence 50 for @{'le_to_eqj}.
+notation "'lej'"         non associative with precedence 50 for @{'lej}.
 
-lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
-intros (l a b H); lapply (le_to_eqm ??? H) as H1;
-lapply (feq_jl ??? b H1) as H2;
-apply (Eq≈ ?? (join_comm ???));
-apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
-apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
-apply eq_sym; apply absorbjm;
-qed.
+interpretation "Lattice meet"        'meet = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_refl"   'meet_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_comm"   'meet_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_assoc"  'meet_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice le_to_eqm"   'le_to_eqm = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice lem"         'lem = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice join"        'join = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_refl"   'join_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_comm"   'join_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_assoc"  'join_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice le_to_eqj"   'le_to_eqj = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice lej"         'lej = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+
+notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
+notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
+interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
+notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
+notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
+interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
 
-lemma lej: ∀l:lattice.∀x,y:l.x ≤ (x ∨ y).
-intros (l x y); 
-apply (Le≪ ? (absorbmj ? x y)); apply lem;
-qed.
\ No newline at end of file

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index a2d25734217ead71fd14871f92b2264dd0987d01..968ae8f3b65515e9e1411fac2530981e949a52a9 100644 (file)
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -21,21 +21,6 @@ record mlattice_ (R : todgroup) : Type ≝ {
   ml_with_: ms_carr ? ml_mspace_ = apart_of_excess (pl_carr ml_lattice) 
 }.
 
-(*
-lemma ml_lattice: ∀R.mlattice_ R → lattice.
-intros (R ml); apply (mk_lattice (apart_of_metric_space ? (ml_mspace_ ? ml))); try unfold eq;
-cases (ml_with2_ ? ml);
-[apply (join (ml_lattice_ ? ml));|apply (meet (ml_lattice_ ? ml));
-|apply (join_refl (ml_lattice_ R ml));| apply (meet_refl (ml_lattice_ ? ml));
-|apply (join_comm (ml_lattice_ ? ml));| apply (meet_comm (ml_lattice_ ? ml));
-|apply (join_assoc (ml_lattice_ ? ml));|apply (meet_assoc (ml_lattice_ ? ml));
-|apply (absorbjm (ml_lattice_ ? ml)); |apply (absorbmj (ml_lattice_ ? ml));
-|apply (strong_extj (ml_lattice_ ? ml));|apply (strong_extm (ml_lattice_ ? ml));]
-qed.
-
-coercion cic:/matita/metric_lattice/ml_lattice.con.
-*)
-
 lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
 intros (R ml); apply (mk_metric_space R (apart_of_excess ml)); 
 unfold apartness_OF_mlattice_; 
@@ -47,6 +32,7 @@ qed.
 
 coercion cic:/matita/metric_lattice/ml_mspace.con.
 
+alias symbol "plus" = "Abelian group plus".
 record mlattice (R : todgroup) : Type ≝ {
   ml_carr :> mlattice_ R;
   ml_prop1: ∀a,b:ml_carr. 0 < δ a b → a # b;
@@ -90,6 +76,31 @@ intros (R ml x y H); apply ml_prop1; split; [apply mpositive;]
 apply ap_symmetric; assumption;
 qed.
 
+interpretation "Lattive meet le" 'leq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
+
+interpretation "Lattive join le (aka ge)" 'geq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
+
+lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
+intros(l a b H); apply H;
+qed.
+
+lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
+intros(l a b H); apply H;
+qed.
+
+lemma eq_to_eq:∀l:lattice.∀a,b:l.
+  (eq (apart_of_excess (pl_carr (latt_jcarr l))) a b) →
+  (eq (apart_of_excess (pl_carr (latt_mcarr l))) a b).
+intros 3; unfold eq; unfold apartness_OF_lattice;
+unfold apartness_OF_lattice_1; unfold latt_jcarr; simplify;
+unfold dual_exc; simplify; intros 2 (H H1); apply H;
+cases H1;[right|left]assumption;
+qed. 
+
+coercion cic:/matita/metric_lattice/eq_to_eq.con nocomposites.
+
 (* 3.11 *)
 lemma le_mtri: 
   ∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
@@ -97,17 +108,23 @@ intros (R ml x y z Lxy Lyz); apply le_le_eq; [apply mtineq]
 apply (le_transitive ????? (ml_prop2 ?? (y) ??)); 
 cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
   apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
-lapply (le_to_eqm ??? Lxy) as Dxm; lapply (le_to_eqm ??? Lyz) as Dym;
-lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz;
+lapply (le_to_eqm ?? Lxy) as Dxm; lapply (le_to_eqm ?? Lyz) as Dym;
+lapply (le_to_eqj ?? (le_to_ge ??? Lxy)) as Dxj; lapply (le_to_eqj ?? (le_to_ge ??? Lyz)) as Dyj; clear Lxy Lyz;
 apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
 apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
-apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z) (meq_l ????? Dxj));
-apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [
-  apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (x∨y) ? Dyj));]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) z));[
+  apply feq_plusl; apply meq_l; clear Dyj Dxm Dym;
+  unfold apartness_OF_mlattice1;
+  exact (eq_to_eq ??? Dxj);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) (z∨y))); [
+  apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (y∨x) ? Dyj));]
 apply (Eq≈ ? (plus_comm ???));
-apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)) (meq_l ????? (join_comm ?x y)));
+apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)));[
+  apply feq_plusr;
+  apply meq_r; 
+  apply (join_comm y z);]
 apply feq_plusl;
-apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ?x y)));
+apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm x y)));
 apply eq_reflexive;   
 qed.  
 

diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
index 037d3d7dcb416c063b79d5136410ae0b3c900c33..47709bd24c78f5bbfd27b0d528decf4e6741dd4c 100644 (file)
--- a/helm/software/matita/dama/sandwich.ma
+++ b/helm/software/matita/dama/sandwich.ma
@@ -36,11 +36,12 @@ notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
   
 interpretation "tends to" 'tends s x = 
   (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
-    
-alias symbol "and" = "constructive and".
+
 theorem sandwich:
+let ugo ≝ excess_OF_lattice1 in
   ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
-    (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) → 
+    (∀n. (le (excess_OF_lattice1 ml) (xn n) (an n)) ∧ 
+     (le (excess_OF_lattice1 ?) (bn n) (xn n))) → True. 
     an ⇝ x → bn ⇝ x → xn ⇝ x.
 intros (R ml an bn xn x H Ha Hb); 
 unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
@@ -55,7 +56,7 @@ cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2;
 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
   apply (le_transitive ???? (mtineq ???? (an n3)));
   cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
-    lapply (le_mtri ????? H7 H8) as H9; clear H7 H8;
+    lapply (le_mtri ?? ??? (ge_to_le ??? H7) (ge_to_le ??? H8)) as H9; clear H7 H8;
     lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
     apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
     apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???));