X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=78046c688ead8c5561ad629785fce67f98ea52c1;hb=6ba374cbb94797e58cd997c5b41099dd9f679a57;hp=fcad3fdc54dc227e4ea3cbd9c3ac7665db07b831;hpb=24b1ff241e9b3428f8f5275a4ac9e8d0ca20d82f;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index fcad3fdc5..78046c688 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -14,140 +14,433 @@
 
 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 semi_lattice_base : Type ≝ {
+  sl_carr:> apartness;
+  sl_op: sl_carr → sl_carr → sl_carr;
+  sl_op_refl: ∀x.sl_op x x ≈ x;  
+  sl_op_comm: ∀x,y:sl_carr. sl_op x y ≈ sl_op y x;
+  sl_op_assoc: ∀x,y,z:sl_carr. sl_op x (sl_op y z) ≈ sl_op (sl_op x y) z;
+  sl_strong_extop: ∀x.strong_ext ? (sl_op x)  
 }.
 
-definition excl ≝ λl:lattice_.λa,b:l_carr l.ap_apart (l_carr l) a (l_meet 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;
-| 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 ???));
-    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 ????));
-  assumption]
+notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }.
+interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b).
+
+lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
+intro l;
+apply mk_excess;
+[1: apply mk_excess_;
+    [1: apply mk_excess_dual_smart;
+         
+  apply (mk_excess_base (sl_carr l));
+    [1: apply (λa,b:sl_carr l.a # (a ✗ b));
+    |2: unfold; intros 2 (x H); simplify in H;
+        lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
+        apply (ap_coreflexive ?? H1);
+    |3: unfold; simplify; intros (x y z H1);
+        cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
+          lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
+          lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
+          lapply (sl_strong_extop ???? H22); clear H22; 
+          left; apply ap_symmetric; assumption;]
+        cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
+        right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
+        apply (sl_strong_extop ???? H31);]
+
+    |2:
+    apply apartness_of_excess_base; 
+    
+  apply (mk_excess_base (sl_carr l));
+    [1: apply (λa,b:sl_carr l.a # (a ✗ b));
+    |2: unfold; intros 2 (x H); simplify in H;
+        lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
+        apply (ap_coreflexive ?? H1);
+    |3: unfold; simplify; intros (x y z H1);
+        cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
+          lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
+          lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
+          lapply (sl_strong_extop ???? H22); clear H22; 
+          left; apply ap_symmetric; assumption;]
+        cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
+        right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
+        apply (sl_strong_extop ???? H31);]
+    
+    |3: apply refl_eq;]
+|2,3: intros (x y H); assumption;]         
 qed.    
 
-(* coercion cic:/matita/lattice/excess_of_lattice_.con. *)
-
-record prelattice : Type ≝ {
-  pl_carr:> excess;
-  meet: pl_carr → pl_carr → pl_carr;
-  meet_refl: ∀x.meet x x ≈ x;  
-  meet_comm: ∀x,y:pl_carr. meet x y ≈ meet y x;
-  meet_assoc: ∀x,y,z:pl_carr. meet x (meet y z) ≈ meet (meet x y) z;
-  strong_extm: ∀x.strong_ext ? (meet x);
-  le_to_eqm: ∀x,y.x ≤ y → x ≈ meet x y;
-  lem: ∀x,y.(meet x y) ≤ y 
+record semi_lattice : Type ≝ {
+  sl_exc:> excess;
+  sl_meet: sl_exc → sl_exc → sl_exc;
+  sl_meet_refl: ∀x.sl_meet x x ≈ x;  
+  sl_meet_comm: ∀x,y. sl_meet x y ≈ sl_meet y x;
+  sl_meet_assoc: ∀x,y,z. sl_meet x (sl_meet y z) ≈ sl_meet (sl_meet x y) z;
+  sl_strong_extm: ∀x.strong_ext ? (sl_meet x);
+  sl_le_to_eqm: ∀x,y.x ≤ y → x ≈ sl_meet x y;
+  sl_lem: ∀x,y.(sl_meet x y) ≤ y 
 }.
  
-interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattice/meet.con _ a b).
+interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
 
-lemma feq_ml: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
+lemma sl_feq_ml: ∀ml:semi_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);
+intro H1; apply H; clear H; apply (sl_strong_extm ???? H1);
 qed.
 
-lemma feq_mr: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
+lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
 intros (l a b c H); 
-apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
-apply feq_ml; assumption;
+apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???));
+apply sl_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 semi_lattice_of_semi_lattice_base: semi_lattice_base → semi_lattice.
+intro slb; apply (mk_semi_lattice (excess_of_semi_lattice_base slb));
+[1: apply (sl_op slb);
+|2: intro x; apply (eq_trans (excess_of_semi_lattice_base slb)); [2: 
+      apply (sl_op_refl slb);|1:skip] (sl_op slb x x)); ? (sl_op_refl slb x));
+
+ unfold excess_of_semi_lattice_base; simplify;
+    intro H; elim H;
+    [ 
+    
+    
+    lapply (ap_rewl (excess_of_semi_lattice_base slb) x ? (sl_op slb x x) 
+      (eq_sym (excess_of_semi_lattice_base slb) ?? (sl_op_refl slb x)) t);
+    change in x with (sl_carr slb);
+    apply (Ap≪ (x ✗ x)); (sl_op_refl slb x)); 
+
+whd in H; elim H; clear H;
+    [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t);
+
+prelattice (excess_of_directed l_)); [apply (sl_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 (sl_op_refl l_ x); 
+  lapply (Ap≫ ? (sl_op_comm ???) t) as H; clear t; 
+  lapply (sl_strong_extop l_ ??? H); apply ap_symmetric; assumption
+ | lapply (Ap≪ ? (sl_op_refl ?x) t) as H; clear t;
+   lapply (sl_strong_extop l_ ??? H); apply (sl_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≪ ? (sl_op_refl ? (sl_op l_ x y)) H1) as H; clear H1;
+  lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (sl_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
+ |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ y x)) H2) as H; clear H2;
+  lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (sl_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≪ ? (sl_op_refl ? (sl_op l_ x (sl_op l_ y z))) H1) as H; clear H1;
+  lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (eq_sym ??? (sl_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≪ ? (sl_op_refl ? (sl_op l_ (sl_op l_ x y) z)) H2) as H; clear H2;
+  lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+  lapply (Ap≪ ? (sl_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≪ ? (sl_op_refl ??) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (sl_strong_extop l_ ??? H1) as H; clear H1;
+ cases (ap_cotransitive ??? (sl_op l_ y z) H);[left|right|right|left] try assumption;
+ [apply ap_symmetric;apply (Ap≪ ? (sl_op_comm ???));
+ |apply (Ap≫ ? (sl_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≪ ? (sl_op_refl ??) H) as H1; clear H;
+ lapply (sl_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 (sl_op l_ x y ≈ sl_op l_ x (sl_op l_ y y)) as H1;[2:
+   intro; lapply (sl_strong_extop ???? a); apply (sl_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 (sl_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)
+(* ED(≰,≱) → EB(≰') → ED(≰',≱') *)
+lemma subst_excess_base: excess_dual → excess_base → excess_dual.
+intros; apply (mk_excess_dual_smart e1);
+qed.
+
+(* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *)
+lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_.
+intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity;
+qed. 
+
+(* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *)
+alias symbol "nleq" = "Excess excess_".
+lemma subst_excess_: ∀e:excess. ∀e1:excess_. 
+  (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) →
+  (∀y,x:e1.y ≰ x ∨ x ≰ y →  y # x) →
+  excess.
+intros (e e1 H1 H2); apply (mk_excess e1 H1 H2); 
+qed. 
+
+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.
+  ∀e:excess. 
+  ∀p:exc_ap l = exc_ap e.
+  (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) →
+  (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) → 
+  semi_lattice.
+[1,2:intro M;
+ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+ cases p; apply M;
+|intros (l e p H1 H2);
+ apply (mk_semi_lattice e);
+   [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+     cases p; simplify; apply (sl_meet l);
+   |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl;
+   |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm;
+   |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc;  
+   |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm;
+   |6: clear H2; apply hole; apply H1;
+   |7: clear H1; apply hole; apply H2;]]
+qed.
+
+lemma excess_of_excess_base: excess_base → excess.
+intro eb;
+apply mk_excess;
+  [apply (mk_excess_ (mk_excess_dual_smart eb));
+    [apply (apartness_of_excess_base eb);
+    |reflexivity]
+  |2,3: intros; assumption]
+qed. 
+
+lemma subst_excess_preserves_aprtness:
+  ∀l:semi_lattice.
+  ∀e:excess.
+  ∀p,H1,H2. 
+  exc_ap l = exc_ap (subst_excess l e p H1 H2).
+intros; 
+unfold subst_excess;
+simplify; assumption;
+qed.
+
+
+lemma subst_excess__preserves_aprtness:
+  ∀l:excess.
+  ∀e:excess_base.
+  ∀p,H1,H2. 
+  exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2).
+intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify);
+(unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p);
+intros; cases p;
+reflexivity;
+qed.
+
+lemma subst_excess_base_in_excess_:
+  ∀d:excess_.
+  ∀eb:excess_base.
+  ∀p:exc_carr d = exc_carr eb.
+  excess_.
+intros (e_ eb);
+apply (subst_dual_excess e_);
+  [apply (subst_excess_base e_ eb);
+  |assumption]
+qed.
+
+lemma subst_excess_base_in_excess:
+  ∀d:excess.
+  ∀eb:excess_base.
+  ∀p:exc_carr d = exc_carr eb.
+  (∀y1,x1:eb. (?(ap_apart d)) y1  x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
+  (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 →  (?(ap_apart d)) y2 x2) →
+  excess.
+[1,3,4:apply Type|2,5:intro f; cases p; apply f]
+intros (d eb p H1 H2);
+apply (subst_excess_ d);
+  [apply (subst_excess_base_in_excess_ d eb p);
+  |apply hole; clear H2; 
+   change in ⊢ (%→%→?) with (exc_carr eb);      
+   change in ⊢ (?→?→?→? (? % ? ?) (? % ? ?)) with eb; intros (y x H3);
+   apply H1; generalize in match H3;
+   unfold ap_apart; unfold subst_excess_base_in_excess_;
+   unfold subst_dual_excess; simplify; 
+   generalize in match x;
+   generalize in match y;
+   cases p; simplify; intros; assumption;
+  |apply hole; clear H1; 
+   change in ⊢ (%→%→?) with (exc_carr eb);      
+   change in ⊢ (?→?→? (? % ? ?) (? % ? ?)→?) with eb; intros (y x H3);
+   unfold ap_apart; unfold subst_excess_base_in_excess_;
+   unfold subst_dual_excess; simplify; generalize in match (H2 ?? H3);
+   generalize in match x; generalize in match y; cases p;
+   intros; assumption;]
+qed.    
+
+lemma tech1: ∀e:excess.
+ ∀eb:excess_base.
+ ∀p,H1,H2.
+ exc_ap e = exc_ap_  (subst_excess_base_in_excess e eb p H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; simplify;
+unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; simplify; reflexivity;
+qed.
+
+lemma tech2: 
+ ∀e:excess_.∀eb.∀p.
+  exc_ap e = exc_ap (mk_excess_ (subst_excess_base e eb) (exc_ap e) p).
+intros (e eb p);unfold exc_ap; simplify; cases p; simplify; reflexivity;
+qed.
+  
+(*
+lemma eq_fap:
+ ∀a1,b1,a2,b2,a3,b3,a4,b4,a5,b5.
+ a1=b1 → a2=b2 → a3=b3 → a4=b4 → a5=b5 → mk_apartness a1 a2 a3 a4 a5 = mk_apartness b1 b2 b3 b4 b5.
+intros; cases H; cases H1; cases H2; cases H3; cases H4; reflexivity;
+qed.
+*)
+
+lemma subst_excess_base_in_excess_preserves_apartness:
+ ∀e:excess.
+ ∀eb:excess_base.
+ ∀H,H1,H2.
+ apartness_OF_excess e =
+ apartness_OF_excess (subst_excess_base_in_excess e eb H H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; unfold apartness_OF_excess;
+simplify in ⊢ (? ? ? (? %));
+rewrite < (tech2 e eb );
+reflexivity;
+qed.
+ 
+ 
+ 
+alias symbol "nleq" = "Excess base excess".
+lemma subst_excess_base_in_semi_lattice: 
+  ∀sl:semi_lattice.
+  ∀eb:excess_base.
+  ∀p:exc_carr sl = exc_carr eb.
+  (∀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 → (?(eq sl)) x3 ((?(sl_meet sl)) x3 y3)) →
+  (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) → 
+  semi_lattice.
+[2:apply Prop|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_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; 
+   generalize in match x as x; generalize in match y as y;
+   cases FALSE;
+   (*
+   (reduce in H ⊢ %; cases H; simplify; intros; assumption); 
+   
+   
+   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);
+   generalize in match OK; generalize in match x as x; generalize in match y as y;
+   cases H; simplify; (* funge, ma devo fare 2 rewrite in un colpo solo *)
+   *) 
+  |cases FALSE;
+  ] 
+qed.
+
+record lattice_ : Type ≝ {
+  latt_mcarr:> semi_lattice;
+  latt_jcarr_: semi_lattice;
+  W1:?; W2:?; W3:?; W4:?; W5:?;
+  latt_with1: latt_jcarr_ = subst_excess_base_in_semi_lattice latt_jcarr_
+    (excess_base_OF_semi_lattice latt_mcarr) W1 W2 W3 W4 W5   
 }.
 
+lemma latt_jcarr : lattice_ → semi_lattice.
+intro l; apply (subst_excess_base_in_semi_lattice (latt_jcarr_ l) (excess_base_OF_semi_lattice (latt_mcarr l)) (W1 l) (W2 l) (W3 l) (W4 l) (W5 l));
+qed.
+    
+coercion cic:/matita/lattice/latt_jcarr.con.
+
+interpretation "Lattice meet" 'and a b =
+ (cic:/matita/lattice/sl_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/sl_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
+}.
+
+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}.
+
+interpretation "Lattice meet"        'meet        = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_refl"   'meet_refl   = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_comm"   'meet_comm   = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_assoc"  'meet_assoc  = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice le_to_eqm"   'le_to_eqm   = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice lem"         'lem         = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice join"        'join        = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_refl"   'join_refl   = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_comm"   'join_comm   = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_assoc"  'join_assoc  = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice le_to_eqj"   'le_to_eqj   = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice lej"         'lej         = (cic:/matita/lattice/sl_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}.
+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_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
+
+
+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 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);
+(* these coercions help unification, handmaking a bit of conversion 
+   over an open term 
+*)
+lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
+intros(l a b H); apply H;
 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;
+lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
+intros(l a b H); apply H;
 qed.
 
-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
+coercion cic:/matita/lattice/le_to_ge.con nocomposites.
+coercion cic:/matita/lattice/ge_to_le.con nocomposites.
\ No newline at end of file