snapshot with more duality, almost where we left without duality

[helm.git] / helm / software / matita / dama / lattice.ma

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 83d138526ae9fea77477599aa4d3ab7b6e5bce5e..ef02134256330b43f7a4006fed38a7702a9546a6 100644 (file)
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -71,26 +71,26 @@ qed.
 
 record semi_lattice : Type ≝ {
   sl_exc:> excess;
-  meet: sl_exc → sl_exc → sl_exc;
-  meet_refl: ∀x.meet x x ≈ 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 
+  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 "semi 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:semi_lattice.∀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:semi_lattice.∀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.
  
  
@@ -173,17 +173,17 @@ 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]
+[apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc|
+apply sl_strong_extm| apply sl_le_to_eqm|apply sl_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).  
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).  
 
 interpretation "Lattice join" 'or a b =
- (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).  
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).  
 
 record lattice : Type ≝ {
   latt_carr:> lattice_;
@@ -206,27 +206,47 @@ 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 _)).
+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}.
-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 _)).
+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).
+
+(* 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 ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
+intros(l a b H); apply H;
+qed.
+
+coercion cic:/matita/lattice/le_to_ge.con nocomposites.
+coercion cic:/matita/lattice/ge_to_le.con nocomposites.
\ No newline at end of file