]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed bugs found by csc
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 Nov 2007 18:27:15 +0000 (18:27 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 Nov 2007 18:27:15 +0000 (18:27 +0000)
helm/software/matita/dama/excedence.ma
helm/software/matita/dama/ordered_groups.ma
helm/software/matita/dama/valued_lattice.ma [new file with mode: 0644]

index 3b2afd5dc982b86c8a8308018b72bc599bc04fc2..c2a5ffd4fde20049391060de83b85f2cd22cf310 100644 (file)
@@ -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.
index cc7e739280cbbd58e277850e2c300e1fe350da88..d9be248d0c01f45094300432a1012c152d130746 100644 (file)
@@ -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/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/valued_lattice.ma
new file mode 100644 (file)
index 0000000..83a062d
--- /dev/null
@@ -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 ? ?));
+
+
+