From 879bd09378045136dc96c7a6f066576003f1574b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 22 Nov 2007 16:58:04 +0000 Subject: [PATCH] lemma finisced --- helm/software/matita/dama/valued_lattice.ma | 83 ++++++++++++++++++++- 1 file changed, 80 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/valued_lattice.ma index ca30ddd0f..53855975d 100644 --- a/helm/software/matita/dama/valued_lattice.ma +++ b/helm/software/matita/dama/valued_lattice.ma @@ -30,7 +30,7 @@ record vlattice (R : ogroup) : Type ≝ { 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 y) ≤ value (join x (meet y z)); + 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)) }. @@ -90,7 +90,7 @@ 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))) ?? H1); clear H1; +apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z)))); [2: apply feq_plusr; apply H1;] clear H1; apply (eq_trans ?? ? ?? (plus_comm ???)); (* apply (eq_trans ?? (0+μ(x∧(y∧z))) ?? (opp_inverse ??)); ASSERT FALSE *) apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z)))); [2: apply eq_sym; apply plus_assoc;] @@ -100,6 +100,31 @@ apply (eq_trans ?? (μ(x∧(y∨z)))); [apply eq_reflexive] apply eq_sym; apply zero_neutral. 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))); [2: apply eq_sym; apply plus_assoc] +apply (eq_trans ?? (0+ μ(x∨y∧z))); [2: apply feq_plusr; apply eq_sym; apply 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); @@ -115,7 +140,59 @@ apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????)); apply feq_plusr; apply plus_assoc; qed. -lemma meet_join_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). +(* 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))); [ -- 2.39.2