X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=787ee3e8e267b18c129d28f0e4abd400c045ae96;hb=954ed2eaf305a60d7e046206472bc0397a421ad2;hp=46662b5881f8990bd9c4e7d77d482a265b993c8a;hpb=9d60f524ea49744e5339a3da981a7263ea92ace6;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 46662b588..787ee3e8e 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/lattice/".
 
-include "excedence.ma".
+
+include "excess.ma".
 
 record lattice : Type ≝ {
   l_carr:> apartness;
@@ -40,8 +40,8 @@ interpretation "Lattice join" 'or a b =
 
 definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
 
-lemma excedence_of_lattice: lattice → excedence.
-intro l; apply (mk_excedence l (excl l));
+lemma excess_of_lattice: lattice → excess.
+intro l; apply (mk_excess 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;
@@ -55,4 +55,33 @@ intro l; apply (mk_excedence l (excl l));
   assumption]
 qed.    
 
-coercion cic:/matita/lattice/excedence_of_lattice.con.
\ No newline at end of file
+coercion cic:/matita/lattice/excess_of_lattice.con.
+
+lemma feq_ml: ∀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_extm ???? H1);
+qed.
+
+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.
+
+lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
+intros (l a b H); 
+  unfold le in H; unfold excess_of_lattice in H;
+  unfold excl in H; simplify in H; 
+unfold eq; assumption;
+qed.
+
+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.
+
+
+