X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=1f605c257e2e13820be92d875ab5249da7cb09a0;hb=55dc87ec418b5b8afe10164cfc61b5ad80a88e6c;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..1f605c257 100644
--- 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