From 988788642009674995382eed87606faca201ac1c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 26 Nov 2007 16:54:32 +0000 Subject: [PATCH] reorganization of many files according to the new basic picture. todo: premetric lattice and the various coercions --- .../dama/constructive_pointfree/lebesgue.ma | 2 +- .../matita/dama/integration_algebras.ma | 2 +- .../matita/dama/{lattices.ma => lattice.ma} | 21 +++++++++- helm/software/matita/dama/metric_lattice.ma | 34 +++++++++++++++++ helm/software/matita/dama/metric_set.ma | 32 ++++++++++++++++ ...lued_lattice.ma => preweighted_lattice.ma} | 38 +++++++++---------- 6 files changed, 106 insertions(+), 23 deletions(-) rename helm/software/matita/dama/{lattices.ma => lattice.ma} (80%) create mode 100644 helm/software/matita/dama/metric_lattice.ma create mode 100644 helm/software/matita/dama/metric_set.ma rename helm/software/matita/dama/{valued_lattice.ma => preweighted_lattice.ma} (92%) diff --git a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma index a739ed715..0dac6fc99 100644 --- a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma +++ b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/lebesgue/". include "reals.ma". -include "lattices.ma". +include "lattice.ma". axiom ltT : ∀R:real.∀a,b:R.Type. diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma index cbe629dac..c37a1f0b1 100644 --- a/helm/software/matita/dama/integration_algebras.ma +++ b/helm/software/matita/dama/integration_algebras.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/integration_algebras/". include "vector_spaces.ma". -include "lattices.ma". +include "lattice.ma". (**************** Riesz Spaces ********************) diff --git a/helm/software/matita/dama/lattices.ma b/helm/software/matita/dama/lattice.ma similarity index 80% rename from helm/software/matita/dama/lattices.ma rename to helm/software/matita/dama/lattice.ma index 8f2aa763d..a1cea05b0 100644 --- a/helm/software/matita/dama/lattices.ma +++ b/helm/software/matita/dama/lattice.ma @@ -14,9 +14,25 @@ set "baseuri" "cic:/matita/lattices/". +include "excedence.ma". + +record lattice : Type ≝ { + l_carr:> apartness; + join: l_carr → l_carr → l_carr; + meet: l_carr → l_carr → l_carr; + 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 y x) z; + meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet y x) z; + absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f; + absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f +}. + + +(* include "ordered_sets.ma". -record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def +record lattice (C:Type) (join,meet:C→C→C) : Prop \def { (* abelian semigroup properties *) l_comm_j: symmetric ? join; l_associative_j: associative ? join; @@ -74,4 +90,5 @@ definition ordered_set_of_lattice: lattice → ordered_set. ] qed. -coercion cic:/matita/lattices/ordered_set_of_lattice.con. \ No newline at end of file +coercion cic:/matita/lattices/ordered_set_of_lattice.con. +*) \ No newline at end of file diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma new file mode 100644 index 000000000..62a84090c --- /dev/null +++ b/helm/software/matita/dama/metric_lattice.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/metric_lattice/". + +include "metric_set.ma". +include "lattice.ma". + +record mlattice (R : ogroup) : Type ≝ { + ml_mset_: metric_set R; + ml_lattice:> lattice; + ml_with_: ms_carr ? ml_mset_ = ap_carr (l_carr ml_lattice) +}. + +lemma ml_mset: ∀R.mlattice R → metric_set R. +intros (R ml); apply (mk_metric_set R ml); unfold Type_OF_mlattice; +cases (ml_with_ ? ml); simplify; +[apply (metric ? (ml_mset_ ? ml));|apply (mpositive ? (ml_mset_ ? ml)); +|apply (mreflexive ? (ml_mset_ ? ml));|apply (msymmetric ? (ml_mset_ ? ml)); +|apply (mtineq ? (ml_mset_ ? ml))] +qed. + +coercion cic:/matita/metric_lattice/ml_mset.con. diff --git a/helm/software/matita/dama/metric_set.ma b/helm/software/matita/dama/metric_set.ma new file mode 100644 index 000000000..74cb7d51c --- /dev/null +++ b/helm/software/matita/dama/metric_set.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/metric_set/". + +include "ordered_groups.ma". + +record metric_set (R : ogroup) : Type ≝ { + ms_carr :> Type; + metric: ms_carr → ms_carr → R; + mpositive: ∀a,b:ms_carr. metric a b ≤ 0; + mreflexive: ∀a. metric a a ≈ 0; + msymmetric: ∀a,b. metric a b ≈ metric b a; + mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b + (* manca qualcosa per essere una metrica e non una semimetrica *) +}. + +notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}. +interpretation "metric" 'delta2 a b = (cic:/matita/metric_set/metric.con _ _ a b). +notation "\delta" non associative with precedence 80 for @{ 'delta }. +interpretation "metric" 'delta = (cic:/matita/metric_set/metric.con _ _). diff --git a/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/preweighted_lattice.ma similarity index 92% rename from helm/software/matita/dama/valued_lattice.ma rename to helm/software/matita/dama/preweighted_lattice.ma index 610bf7d35..9a46fb319 100644 --- a/helm/software/matita/dama/valued_lattice.ma +++ b/helm/software/matita/dama/preweighted_lattice.ma @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/valued_lattice/". +set "baseuri" "cic:/matita/preweighted_lattice/". include "ordered_groups.ma". -record vlattice (R : ogroup) : Type ≝ { - vl_carr:> Type; - value: vl_carr → R; - join: vl_carr → vl_carr → vl_carr; - meet: vl_carr → vl_carr → vl_carr; +record wlattice (R : ogroup) : Type ≝ { + wl_carr:> Type; + value: wl_carr → R; + join: wl_carr → wl_carr → wl_carr; + meet: wl_carr → wl_carr → wl_carr; meet_refl: ∀x. value (meet x x) ≈ value x; join_refl: ∀x. value (join x x) ≈ value x; meet_comm: ∀x,y. value (meet x y) ≈ value (meet y x); @@ -35,18 +35,18 @@ record vlattice (R : ogroup) : Type ≝ { }. interpretation "valued lattice meet" 'and a b = - (cic:/matita/valued_lattice/meet.con _ _ a b). + (cic:/matita/preweighted_lattice/meet.con _ _ a b). interpretation "valued lattice join" 'or a b = - (cic:/matita/valued_lattice/join.con _ _ a b). + (cic:/matita/preweighted_lattice/join.con _ _ a b). notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}. -interpretation "lattice value" 'value2 a = (cic:/matita/valued_lattice/value.con _ _ a). +interpretation "lattice value" 'value2 a = (cic:/matita/preweighted_lattice/value.con _ _ a). notation "\mu" non associative with precedence 80 for @{ 'value }. -interpretation "lattice value" 'value = (cic:/matita/valued_lattice/value.con _ _). +interpretation "lattice value" 'value = (cic:/matita/preweighted_lattice/value.con _ _). -lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L. +lemma feq_joinr: ∀R.∀L:wlattice R.∀x,y,z:L. μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y). intros (R L x y z H H1); apply (plus_cancr ??? (μ(z∧x))); @@ -62,7 +62,7 @@ apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??)); apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??)); qed. -lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z). +lemma modularj: ∀R.∀L:wlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z). intros (R L y z); lapply (modular_mjp ?? y z) as H1; apply (plus_cancr ??? (μ(y ∧ z))); @@ -74,7 +74,7 @@ apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??))); apply eq_reflexive. qed. -lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z). +lemma modularm: ∀R.∀L:wlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z). (* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *) (* exact modularj; *) intros (R L y z); @@ -89,7 +89,7 @@ apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??))); apply eq_reflexive. qed. -lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))). +lemma modularmj: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))). intros (R L x y z); lapply (modular_mjp ?? x (y ∨ z)) as H1; apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? (feq_plusr ???? H1)); clear H1; @@ -100,7 +100,7 @@ apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??)); apply eq_reflexive. qed. -lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))). +lemma modularjm: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))). intros (R L x y z); lapply (modular_mjp ?? x (y ∧ z)) as H1; apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1; @@ -110,7 +110,7 @@ apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??)); apply eq_sym; apply zero_neutral; qed. -lemma step1_3_57': ∀R.∀L:vlattice R.∀x,y,z:L. +lemma step1_3_57': ∀R.∀L:wlattice R.∀x,y,z:L. μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)). intros (R L x y z); apply (eq_trans ?? ? ? (modularjm ?? x y z)); @@ -125,7 +125,7 @@ apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????)); apply feq_plusr; apply plus_assoc; qed. -lemma step1_3_57: ∀R.∀L:vlattice R.∀x,y,z:L. +lemma step1_3_57: ∀R.∀L:wlattice R.∀x,y,z:L. μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)). intros (R L x y z); apply (eq_trans ?? ? ? (modularmj ?? x y z)); @@ -142,7 +142,7 @@ qed. (* LEMMA 3.57 *) -lemma join_meet_le_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). +lemma join_meet_le_join: ∀R.∀L:wlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). intros (R L x y z); apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????))); apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [ @@ -192,7 +192,7 @@ apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; a repeat apply fle_plusl; apply join_meet_le; qed. -lemma meet_le_meet_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). +lemma meet_le_meet_join: ∀R.∀L:wlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). intros (R L x y z); apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????))); apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [ -- 2.39.2