X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=83d138526ae9fea77477599aa4d3ab7b6e5bce5e;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=20d746a0a69ca9a5517e04bb2de3a5012d94713c;hpb=a2fe87da00fb5b9a39e9a1c7d796c61d4c7346af;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 20d746a0a..83d138526 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -12,86 +12,221 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/lattice/".
+include "excess.ma".
 
-include "excedence.ma".
+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)  
+}.
 
-record lattice : Type ≝ {
-  l_carr:> apartness;
-  join: l_carr → l_carr → l_carr;
-  meet: l_carr → l_carr → l_carr;
-  join_refl: ∀x.join x x ≈ x;
+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_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.    
+
+record semi_lattice : Type ≝ {
+  sl_exc:> excess;
+  meet: sl_exc → sl_exc → sl_exc;
   meet_refl: ∀x.meet x x ≈ x;  
-  join_comm: ∀x,y:l_carr. join x y ≈ join y x;
-  meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
-  join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z;
-  meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z;
-  absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
-  absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f;
-  strong_extj: ∀x.strong_ext ? (join x);
-  strong_extm: ∀x.strong_ext ? (meet x)
+  meet_comm: ∀x,y. meet x y ≈ meet y x;
+  meet_assoc: ∀x,y,z. 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 
 }.
+ 
+interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/meet.con _ a b).
+
+lemma 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);
+qed.
+
+lemma 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;
+qed.
+ 
+ 
+(*
+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 (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≪ ? (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≪ ? (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≪ ? (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≪ ? (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≪ ? (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 (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 (sl_op_assoc l_ x y y);
+ assumption; ]
+qed.
+*)
+
+
+record lattice_ : Type ≝ {
+  latt_mcarr:> semi_lattice;
+  latt_jcarr_: semi_lattice;
+  latt_with:  sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr)
+}.
+
+lemma latt_jcarr : lattice_ → semi_lattice.
+intro l;
+apply (mk_semi_lattice (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 _ 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).  
 
-(*
-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.
+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/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 _)).
 
-coercion cic:/matita/lattices/ordered_set_of_lattice.con.
-*)