From 9d60f524ea49744e5339a3da981a7263ea92ace6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 28 Nov 2007 17:00:44 +0000
Subject: [PATCH] ...

---
 helm/software/matita/dama/excedence.ma      |  3 +
 helm/software/matita/dama/lattice.ma        | 75 +++++----------------
 helm/software/matita/dama/metric_lattice.ma | 37 +++++++++-
 helm/software/matita/dama/ordered_group.ma  |  5 ++
 helm/software/matita/dama/sequence.ma       |  5 ++
 5 files changed, 65 insertions(+), 60 deletions(-)

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 34e253b89..22612e2c1 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -181,3 +181,6 @@ cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)]
 right; assumption;
 qed.
     
+lemma le_le_eq: ∀E:excedence.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
+intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 20d746a0a..46662b588 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -38,60 +38,21 @@ interpretation "Lattice meet" 'and a b =
 interpretation "Lattice join" 'or a b =
  (cic:/matita/lattice/join.con _ a b).
 
-(*
-include "ordered_set.ma".
-
-record lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
-   l_comm_j: symmetric ? join;
-   l_associative_j: associative ? join;
-   l_comm_m: symmetric ? meet;
-   l_associative_m: associative ? meet;
-   (* other properties *)
-   l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
-   l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
- }.
-
-record lattice : Type \def
- { l_carrier:> Type;
-   l_join: l_carrier→l_carrier→l_carrier;
-   l_meet: l_carrier→l_carrier→l_carrier;
-   l_lattice_properties:> is_lattice ? l_join l_meet
- }.
-
-definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
-
-definition ordered_set_of_lattice: lattice → ordered_set.
- intros (L);
- apply mk_ordered_set;
-  [2: apply (le L)
-  | skip
-  | apply mk_is_order_relation;
-     [ unfold reflexive;
-       intros;
-       unfold;
-       rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
-       rewrite > l_adsorb_m_j;
-        [ reflexivity
-        | apply (l_lattice_properties L)
-        ]
-     | intros;
-       unfold transitive;
-       unfold le;
-       intros;
-       rewrite < H;
-       rewrite > (l_associative_m ? ? ? L);
-       rewrite > H1;
-       reflexivity
-     | unfold antisimmetric;
-       unfold le;
-       intros;
-       rewrite < H;
-       rewrite > (l_comm_m ? ? ? L);
-       assumption
-     ]
-  ]
-qed.
-
-coercion cic:/matita/lattices/ordered_set_of_lattice.con.
-*)
+definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
+
+lemma excedence_of_lattice: lattice → excedence.
+intro l; apply (mk_excedence l (excl l));
+[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
+  apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
+| intros 3 (x y z); unfold excl; intro H;
+  cases (ap_cotransitive ??? (x∧z∧y) H) (H1 H2); [2:
+    left; apply ap_symmetric; apply (strong_extm ? y); 
+    apply (ap_rewl ???? (meet_comm ???));
+    apply (ap_rewr ???? (meet_comm ???));
+    assumption]
+  cases (ap_cotransitive ??? (x∧z) H1) (H2 H3); [left; assumption]
+  right; apply (strong_extm ? x); apply (ap_rewr ???? (meet_assoc ????));
+  assumption]
+qed.    
+
+coercion cic:/matita/lattice/excedence_of_lattice.con.
\ 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 c8a9c895f..56120525d 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -17,14 +17,14 @@ set "baseuri" "cic:/matita/metric_lattice/".
 include "metric_space.ma".
 include "lattice.ma".
 
-record mlattice (R : ogroup) : Type ≝ {
+record mlattice_ (R : ogroup) : Type ≝ {
   ml_mspace_: metric_space R;
   ml_lattice:> lattice;
   ml_with_: ms_carr ? ml_mspace_ = ap_carr (l_carr ml_lattice)
 }.
 
-lemma ml_mspace: ∀R.mlattice R → metric_space R.
-intros (R ml); apply (mk_metric_space R ml); unfold Type_OF_mlattice;
+lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
+intros (R ml); apply (mk_metric_space R ml); unfold Type_OF_mlattice_;
 cases (ml_with_ ? ml); simplify;
 [apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml));
 |apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml));
@@ -32,3 +32,34 @@ cases (ml_with_ ? ml); simplify;
 qed.
 
 coercion cic:/matita/metric_lattice/ml_mspace.con.
+
+record is_mlattice (R : ogroup) (ml: mlattice_ R) : Type ≝ {
+  ml_prop1: ∀a,b:ml. 0 < δ a b → a # b;
+  ml_prop2: ∀a,b,c:ml. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ δ b c
+}.
+
+record mlattice (R : ogroup) : Type ≝ {
+  ml_carr :> mlattice_ R;
+  ml_props:> is_mlattice R ml_carr
+}.
+
+axiom meq_joinl: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δx y ≈ δz y.
+
+lemma meq_joinr: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δy x ≈ δy z.
+intros; apply (eq_trans ???? (msymmetric ??y x));
+apply (eq_trans ????? (msymmetric ??z y)); apply meq_joinl; assumption;
+qed.
+
+(*
+lemma foo: ∀R.∀ml:mlattice R.∀x,y,z:ml. δx y ≈ δ(y∨x) (y∨z).
+intros; apply le_le_eq; [
+  apply (le_rewr ???? (meq_joinl ????? (join_comm ???)));
+  apply (le_rewr ???? (meq_joinr ????? (join_comm ???)));
+*) 
+
+(* 3.11 *)
+lemma le_mtri: 
+  ∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
+intros (R ml x y z Lxy Lyz); apply le_le_eq; [apply mtineq]
+apply (le_transitive ????? (ml_prop2 ?? ml (y∧x) ??)); 
+(* auto type. assert failure *)
diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 9b37286fc..439a6e262 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -118,6 +118,11 @@ apply (le_rewr ??? (0+g) (plus_comm ???));
 apply (le_rewr ??? (g) (zero_neutral ??) H);
 qed.
 
+lemma fle_plusr: ∀G:ogroup. ∀f,g,h:G. f≤g → f+h≤g+h.
+intros (G f g h H); apply (le_rewl ???? (plus_comm ???)); 
+apply (le_rewr ???? (plus_comm ???)); apply fle_plusl; assumption;
+qed.
+
 lemma plus_cancl_le: 
   ∀G:ogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y.
 intros 5 (G x y z L);
diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma
index 9edc871e5..1350545ae 100644
--- a/helm/software/matita/dama/sequence.ma
+++ b/helm/software/matita/dama/sequence.ma
@@ -58,7 +58,12 @@ intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
 qed.
 
+include "ordered_group.ma".
+include "nat/orders.ma".
 
+definition tends ≝ 
+  λO:ogroup.λs:sequence O.
+    ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
 
 definition increasing ≝ 
   λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
-- 
2.39.2