From 952ced6c96e98fa678c59729d18975f9a376623e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 17 Nov 2007 18:27:15 +0000 Subject: [PATCH] fixed bugs found by csc --- matita/dama/excedence.ma | 20 ++++++---- matita/dama/ordered_groups.ma | 57 ++++++++++++++++++++++++++-- matita/dama/valued_lattice.ma | 70 +++++++++++++++++++++++++++++++++++ 3 files changed, 136 insertions(+), 11 deletions(-) create mode 100644 matita/dama/valued_lattice.ma diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma index 3b2afd5dc..c2a5ffd4f 100644 --- a/matita/dama/excedence.ma +++ b/matita/dama/excedence.ma @@ -21,7 +21,7 @@ include "constructive_higher_order_relations.ma". record excedence : Type ≝ { exc_carr:> Type; - exc_relation: exc_carr → exc_carr → Type; (* Big bug: era in Prop!!! *) + exc_relation: exc_carr → exc_carr → Type; exc_coreflexive: coreflexive ? exc_relation; exc_cotransitive: cotransitive ? exc_relation }. @@ -127,12 +127,6 @@ intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *) qed. -(* CSC: lo avevi gia' dimostrato; ho messo apply! *) -theorem le_le_to_eq: ∀E:excedence.∀x,y:E. x ≤ y → y ≤ x → x ≈ y. -apply le_antisymmetric; -qed. - -(* CSC: perche' quel casino: bastava intros; assumption! *) lemma unfold_apart: ∀E:excedence. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y. intros; assumption; qed. @@ -155,4 +149,14 @@ qed. lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x. intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); apply ap_symmetric; assumption; -qed. \ No newline at end of file +qed. + +lemma exc_rewl: ∀A:excedence.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. +intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption] +cases Exy; right; assumption; +qed. + +lemma exc_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x. +intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption] +elim (Exy); left; assumption; +qed. diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma index cc7e73928..d9be248d0 100644 --- a/matita/dama/ordered_groups.ma +++ b/matita/dama/ordered_groups.ma @@ -37,9 +37,45 @@ coercion cic:/matita/ordered_groups/og_abelian_group.con. *) record ogroup : Type ≝ { og_carr:> pre_ogroup; - fle_plusr: ∀f,g,h:og_carr. f≤g → f+h≤g+h + exc_canc_plusr: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g }. +lemma fexc_plusr: + ∀G:ogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z. +intros 5 (G x y z L); apply (exc_canc_plusr ??? (-z)); +apply (exc_rewl ??? (x + (z + -z)) (plus_assoc ????)); +apply (exc_rewl ??? (x + (-z + z)) (plus_comm ??z)); +apply (exc_rewl ??? (x+0) (opp_inverse ??)); +apply (exc_rewl ??? (0+x) (plus_comm ???)); +apply (exc_rewl ??? x (zero_neutral ??)); +apply (exc_rewr ??? (y + (z + -z)) (plus_assoc ????)); +apply (exc_rewr ??? (y + (-z + z)) (plus_comm ??z)); +apply (exc_rewr ??? (y+0) (opp_inverse ??)); +apply (exc_rewr ??? (0+y) (plus_comm ???)); +apply (exc_rewr ??? y (zero_neutral ??) L); +qed. + +coercion cic:/matita/ordered_groups/fexc_plusr.con nocomposites. + +lemma exc_canc_plusl: ∀G:ogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g. +intros 5 (G x y z L); apply (exc_canc_plusr ??? z); +apply (exc_rewl ??? (z+x) (plus_comm ???)); +apply (exc_rewr ??? (z+y) (plus_comm ???) L); +qed. + +lemma fexc_plusl: + ∀G:ogroup.∀x,y,z:G. x ≰ y → z+x ≰ z+y. +intros 5 (G x y z L); apply (exc_canc_plusl ??? (-z)); +apply (exc_rewl ???? (plus_assoc ??z x)); +apply (exc_rewr ???? (plus_assoc ??z y)); +apply (exc_rewl ??? (0+x) (opp_inverse ??)); +apply (exc_rewr ??? (0+y) (opp_inverse ??)); +apply (exc_rewl ???? (zero_neutral ??)); +apply (exc_rewr ???? (zero_neutral ??) L); +qed. + +coercion cic:/matita/ordered_groups/fexc_plusl.con nocomposites. + lemma plus_cancr_le: ∀G:ogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y. intros 5 (G x y z L); @@ -53,7 +89,7 @@ apply (le_rewr ??? (y+0) (plus_comm ???)); apply (le_rewr ??? (y+(-z+z)) (opp_inverse ??)); apply (le_rewr ??? (y+(z+ -z)) (plus_comm ??z)); apply (le_rewr ??? (y+z+ -z) (plus_assoc ????)); -apply (fle_plusr ??? (-z) L); +intro H; apply L; clear L; apply (exc_canc_plusr ??? (-z) H); qed. lemma fle_plusl: ∀G:ogroup. ∀f,g,h:G. f≤g → h+f≤h+g. @@ -85,7 +121,14 @@ apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????)); apply (fle_plusl ??? (-z) L); qed. - +lemma exc_opp_x_zero_to_exc_zero_x: + ∀G:ogroup.∀x:G.-x ≰ 0 → 0 ≰ x. +intros (G x H); apply (exc_canc_plusr ??? (-x)); +apply (exc_rewr ???? (plus_comm ???)); +apply (exc_rewr ???? (opp_inverse ??)); +apply (exc_rewl ???? (zero_neutral ??) H); +qed. + lemma le_zero_x_to_le_opp_x_zero: ∀G:ogroup.∀x:G.0 ≤ x → -x ≤ 0. intros (G x Px); apply (plus_cancr_le ??? x); @@ -93,6 +136,14 @@ apply (le_rewl ??? 0 (opp_inverse ??)); apply (le_rewr ??? x (zero_neutral ??) Px); qed. +lemma exc_zero_opp_x_to_exc_x_zero: + ∀G:ogroup.∀x:G. 0 ≰ -x → x ≰ 0. +intros (G x H); apply (exc_canc_plusl ??? (-x)); +apply (exc_rewr ???? (plus_comm ???)); +apply (exc_rewl ???? (opp_inverse ??)); +apply (exc_rewr ???? (zero_neutral ??) H); +qed. + lemma le_x_zero_to_le_zero_opp_x: ∀G:ogroup.∀x:G. x ≤ 0 → 0 ≤ -x. intros (G x Lx0); apply (plus_cancr_le ??? x); diff --git a/matita/dama/valued_lattice.ma b/matita/dama/valued_lattice.ma new file mode 100644 index 000000000..83a062de5 --- /dev/null +++ b/matita/dama/valued_lattice.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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; + meet_join_plus: ∀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 (join y z)) ≤ value (meet x y) +}. + +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 _ _). + +axiom foo: ∀R.∀L:vlattice R.∀x,y,z:L. + μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)). + +lemma meet_join_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). +intros (R L x y z); +apply (le_rewr ??? (μ x + μ y + μ z + -μ (y ∧ z) + -μ(z ∨ (x ∨ y))) (foo ?????)); +apply (le_rewr ??? (μ x + μ y + μ z + -μ (y ∧ z) + -μ((z ∨ x) ∨ y))); + [ apply feq_plusl; apply eq_opp_sym; apply join_assoc;] +lapply (meet_join_le ?? z x y); +cut (- μ (z ∨ x ∨ y) ≈ - μ (z ∨ x) - μ y + μ (y ∧ (z ∨ x))); + [2: + + +lemma join_meet_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). +(* hint per duplicati? *) +intros (R L x y z); +apply (le_rewr ??? (0 + μ (x ∨ z)) (zero_neutral ??)); +apply (le_rewr ??? (μ (x ∨ z) + 0) (plus_comm ???)); +apply (le_rewr ??? (μ (x ∨ z) + (-μ(y ∨ z) + μ(y ∨ z))) (opp_inverse ? ?)); + + + -- 2.39.2