From: Enrico Tassi Date: Mon, 26 Nov 2007 16:54:32 +0000 (+0000) Subject: reorganization of many files according to the new basic picture. X-Git-Tag: make_still_working~5772 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=988788642009674995382eed87606faca201ac1c;p=helm.git reorganization of many files according to the new basic picture. todo: premetric lattice and the various coercions --- 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/lattice.ma b/helm/software/matita/dama/lattice.ma new file mode 100644 index 000000000..a1cea05b0 --- /dev/null +++ b/helm/software/matita/dama/lattice.ma @@ -0,0 +1,94 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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 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 + }. + +interpretation "Lattice meet" 'and a b = + (cic:/matita/lattices/l_meet.con _ a b). + +interpretation "Lattice join" 'or a b = + (cic:/matita/lattices/l_join.con _ a b). + +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. + +coercion cic:/matita/lattices/ordered_set_of_lattice.con. +*) \ No newline at end of file diff --git a/helm/software/matita/dama/lattices.ma b/helm/software/matita/dama/lattices.ma deleted file mode 100644 index 8f2aa763d..000000000 --- a/helm/software/matita/dama/lattices.ma +++ /dev/null @@ -1,77 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/lattices/". - -include "ordered_sets.ma". - -record is_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 - }. - -interpretation "Lattice meet" 'and a b = - (cic:/matita/lattices/l_meet.con _ a b). - -interpretation "Lattice join" 'or a b = - (cic:/matita/lattices/l_join.con _ a b). - -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. - -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/preweighted_lattice.ma b/helm/software/matita/dama/preweighted_lattice.ma new file mode 100644 index 000000000..9a46fb319 --- /dev/null +++ b/helm/software/matita/dama/preweighted_lattice.ma @@ -0,0 +1,243 @@ +(**************************************************************************) +(* ___ *) +(* ||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/preweighted_lattice/". + +include "ordered_groups.ma". + +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); + join_comm: ∀x,y. value (join x y) ≈ value (join y x); + join_assoc: ∀x,y,z. value (join x (join y z)) ≈ value (join (join x y) z); + meet_assoc: ∀x,y,z. value (meet x (meet y z)) ≈ value (meet (meet x y) z); + meet_wins1: ∀x,y. value (join x (meet x y)) ≈ value x; + meet_wins2: ∀x,y. value (meet x (join x y)) ≈ value x; + modular_mjp: ∀x,y. value (join x y) + value (meet x y) ≈ value x + value y; + join_meet_le: ∀x,y,z. value (join x (meet y z)) ≤ value (join x y); + meet_join_le: ∀x,y,z. value (meet x y) ≤ value (meet x (join y z)) +}. + +interpretation "valued lattice meet" 'and a b = + (cic:/matita/preweighted_lattice/meet.con _ _ a b). + +interpretation "valued lattice join" 'or 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/preweighted_lattice/value.con _ _ a). + +notation "\mu" non associative with precedence 80 for @{ 'value }. +interpretation "lattice value" 'value = (cic:/matita/preweighted_lattice/value.con _ _). + +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))); +apply (eq_trans ?? (μz + μx) ? (modular_mjp ????)); +apply (eq_trans ?? (μz + μy) ? H); clear H; +apply (eq_trans ?? (μ(z∨y) + μ(z∧y)) ? (modular_mjp ??z y)); +apply (plus_cancl ??? (- μ (z ∨ y))); +apply (eq_trans ?? ? ? (plus_assoc ????)); +apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??)); +apply (eq_trans ?? ? ? (zero_neutral ??)); +apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????)); +apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??)); +apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??)); +qed. + +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))); +apply (eq_trans ?? ? ? H1); clear H1; +apply (eq_trans ?? ? ?? (plus_assoc ????)); +apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??)); +apply (eq_trans ?? ? ?? (plus_comm ???)); +apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??))); +apply eq_reflexive. +qed. + +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); +lapply (modular_mjp ?? y z) as H1; +apply (plus_cancl ??? (μ(y ∨ z))); +apply (eq_trans ?? ? ? H1); clear H1; +apply (eq_trans ????? (plus_comm ???)); +apply (eq_trans ?? ? ?? (plus_assoc ????)); +apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??)); +apply (eq_trans ?? ? ?? (plus_comm ???)); +apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??))); +apply eq_reflexive. +qed. + +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; +apply (eq_trans ?? ? ?? (plus_comm ???)); +apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????)); +apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??)); +apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??)); +apply eq_reflexive. +qed. + +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; +apply (eq_trans ?? ? ?? (plus_comm ???)); +apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ?? (plus_assoc ????)); +apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??)); +apply eq_sym; apply zero_neutral; +qed. + +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)); +apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [ + apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);] +apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2: + apply feq_plusl; apply feq_opp; + apply (eq_trans ?? ? ? (meet_assoc ?????)); + apply (eq_trans ?? ? ? (meet_comm ????)); + apply eq_reflexive;] +apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????)); +apply feq_plusr; apply plus_assoc; +qed. + +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)); +apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [ + apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);] +apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2: + apply feq_plusl; apply feq_opp; + apply (eq_trans ?? ? ? (join_assoc ?????)); + apply (eq_trans ?? ? ? (join_comm ????)); + apply eq_reflexive;] +apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????)); +apply feq_plusr; apply plus_assoc; +qed. + +(* LEMMA 3.57 *) + +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))); [ + apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;] +apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [ + apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm] +apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [ + apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [ + apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;] + apply eq_sym; apply eq_opp_plus_plus_opp_opp;] +apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [ + repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??)); + apply join_comm;] +apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [ + apply eq_sym; apply plus_assoc;] +apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;] +apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply eq_sym; apply plus_assoc;] +apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????))); + apply feq_plusl; apply plus_comm;] +apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????))); + apply feq_plusl; apply plus_comm;] +apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???)); + apply opp_inverse; apply eq_reflexive;] +apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???)); + apply eq_sym; apply zero_neutral;] +apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply plus_comm;] +apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl; + apply plus_comm;] +apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [ + repeat apply feq_plusr; apply modularj;] +apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????)); +apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral] +apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse] +apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;] +repeat apply fle_plusl; apply join_meet_le; +qed. + +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))); [ + apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;] +apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [ + apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj] +apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [ + apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [ + apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;] + apply eq_sym; apply eq_opp_plus_plus_opp_opp;] +apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [ + repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??)); + apply meet_comm;] +apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [ + apply eq_sym; apply plus_assoc;] +apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;] +apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply eq_sym; apply plus_assoc;] +apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????))); + apply feq_plusl; apply plus_comm;] +apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????))); + apply feq_plusl; apply plus_comm;] +apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???)); + apply opp_inverse; apply eq_reflexive;] +apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???)); + apply eq_sym; apply zero_neutral;] +apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply plus_comm;] +apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); + apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl; + apply plus_comm;] +apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [ + repeat apply feq_plusr; apply modularm;] +apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????)); +apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral] +apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse] +apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;] +repeat apply fle_plusl; apply meet_join_le; +qed. diff --git a/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/valued_lattice.ma deleted file mode 100644 index 610bf7d35..000000000 --- a/helm/software/matita/dama/valued_lattice.ma +++ /dev/null @@ -1,243 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/valued_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; - 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); - join_comm: ∀x,y. value (join x y) ≈ value (join y x); - join_assoc: ∀x,y,z. value (join x (join y z)) ≈ value (join (join x y) z); - meet_assoc: ∀x,y,z. value (meet x (meet y z)) ≈ value (meet (meet x y) z); - meet_wins1: ∀x,y. value (join x (meet x y)) ≈ value x; - meet_wins2: ∀x,y. value (meet x (join x y)) ≈ value x; - modular_mjp: ∀x,y. value (join x y) + value (meet x y) ≈ value x + value y; - join_meet_le: ∀x,y,z. value (join x (meet y z)) ≤ value (join x y); - meet_join_le: ∀x,y,z. value (meet x y) ≤ value (meet x (join y z)) -}. - -interpretation "valued lattice meet" 'and a b = - (cic:/matita/valued_lattice/meet.con _ _ a b). - -interpretation "valued lattice join" 'or a b = - (cic:/matita/valued_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). - -notation "\mu" non associative with precedence 80 for @{ 'value }. -interpretation "lattice value" 'value = (cic:/matita/valued_lattice/value.con _ _). - -lemma feq_joinr: ∀R.∀L:vlattice 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))); -apply (eq_trans ?? (μz + μx) ? (modular_mjp ????)); -apply (eq_trans ?? (μz + μy) ? H); clear H; -apply (eq_trans ?? (μ(z∨y) + μ(z∧y)) ? (modular_mjp ??z y)); -apply (plus_cancl ??? (- μ (z ∨ y))); -apply (eq_trans ?? ? ? (plus_assoc ????)); -apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??)); -apply (eq_trans ?? ? ? (zero_neutral ??)); -apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????)); -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). -intros (R L y z); -lapply (modular_mjp ?? y z) as H1; -apply (plus_cancr ??? (μ(y ∧ z))); -apply (eq_trans ?? ? ? H1); clear H1; -apply (eq_trans ?? ? ?? (plus_assoc ????)); -apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??)); -apply (eq_trans ?? ? ?? (plus_comm ???)); -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). -(* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *) -(* exact modularj; *) -intros (R L y z); -lapply (modular_mjp ?? y z) as H1; -apply (plus_cancl ??? (μ(y ∨ z))); -apply (eq_trans ?? ? ? H1); clear H1; -apply (eq_trans ????? (plus_comm ???)); -apply (eq_trans ?? ? ?? (plus_assoc ????)); -apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??)); -apply (eq_trans ?? ? ?? (plus_comm ???)); -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))). -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; -apply (eq_trans ?? ? ?? (plus_comm ???)); -apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????)); -apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??)); -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))). -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; -apply (eq_trans ?? ? ?? (plus_comm ???)); -apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ?? (plus_assoc ????)); -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. - μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)). -intros (R L x y z); -apply (eq_trans ?? ? ? (modularjm ?? x y z)); -apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [ - apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);] -apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2: - apply feq_plusl; apply feq_opp; - apply (eq_trans ?? ? ? (meet_assoc ?????)); - apply (eq_trans ?? ? ? (meet_comm ????)); - apply eq_reflexive;] -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. - μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)). -intros (R L x y z); -apply (eq_trans ?? ? ? (modularmj ?? x y z)); -apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [ - apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);] -apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2: - apply feq_plusl; apply feq_opp; - apply (eq_trans ?? ? ? (join_assoc ?????)); - apply (eq_trans ?? ? ? (join_comm ????)); - apply eq_reflexive;] -apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????)); -apply feq_plusr; apply plus_assoc; -qed. - -(* LEMMA 3.57 *) - -lemma join_meet_le_join: ∀R.∀L:vlattice 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))); [ - apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [ - apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [ - apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [ - apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;] - apply eq_sym; apply eq_opp_plus_plus_opp_opp;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [ - repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??)); - apply join_comm;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [ - apply eq_sym; apply plus_assoc;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply eq_sym; apply plus_assoc;] -apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???)); - apply opp_inverse; apply eq_reflexive;] -apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???)); - apply eq_sym; apply zero_neutral;] -apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply plus_comm;] -apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl; - apply plus_comm;] -apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply modularj;] -apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????)); -apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral] -apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse] -apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;] -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)). -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))); [ - apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [ - apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [ - apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [ - apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;] - apply eq_sym; apply eq_opp_plus_plus_opp_opp;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [ - repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??)); - apply meet_comm;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [ - apply eq_sym; apply plus_assoc;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply eq_sym; apply plus_assoc;] -apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???)); - apply opp_inverse; apply eq_reflexive;] -apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???)); - apply eq_sym; apply zero_neutral;] -apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply plus_comm;] -apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl; - apply plus_comm;] -apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply modularm;] -apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????)); -apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral] -apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse] -apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;] -repeat apply fle_plusl; apply meet_join_le; -qed.