1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/valued_lattice/".
17 include "ordered_groups.ma".
19 record vlattice (R : ogroup) : Type ≝ {
22 join: vl_carr → vl_carr → vl_carr;
23 meet: vl_carr → vl_carr → vl_carr;
24 meet_refl: ∀x. value (meet x x) ≈ value x;
25 join_refl: ∀x. value (join x x) ≈ value x;
26 meet_comm: ∀x,y. value (meet x y) ≈ value (meet y x);
27 join_comm: ∀x,y. value (join x y) ≈ value (join y x);
28 join_assoc: ∀x,y,z. value (join x (join y z)) ≈ value (join (join x y) z);
29 meet_assoc: ∀x,y,z. value (meet x (meet y z)) ≈ value (meet (meet x y) z);
30 meet_wins1: ∀x,y. value (join x (meet x y)) ≈ value x;
31 meet_wins2: ∀x,y. value (meet x (join x y)) ≈ value x;
32 modular_mjp: ∀x,y. value (join x y) + value (meet x y) ≈ value x + value y;
33 join_meet_le: ∀x,y,z. value (join x (meet y z)) ≤ value (join x y);
34 meet_join_le: ∀x,y,z. value (meet x (join y z)) ≤ value (meet x y)
37 interpretation "valued lattice meet" 'and a b =
38 (cic:/matita/valued_lattice/meet.con _ _ a b).
40 interpretation "valued lattice join" 'or a b =
41 (cic:/matita/valued_lattice/join.con _ _ a b).
43 notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
44 interpretation "lattice value" 'value2 a = (cic:/matita/valued_lattice/value.con _ _ a).
46 notation "\mu" non associative with precedence 80 for @{ 'value }.
47 interpretation "lattice value" 'value = (cic:/matita/valued_lattice/value.con _ _).
49 lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L.
50 μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
51 intros (R L x y z H H1);
52 apply (plus_cancr ??? (μ(z∧x)));
53 apply (eq_trans ?? (μz + μx) ? (modular_mjp ????));
54 apply (eq_trans ?? (μz + μy) ? H); clear H;
55 apply (eq_trans ?? (μ(z∨y) + μ(z∧y))); [1: apply eq_sym; apply modular_mjp]
56 apply (plus_cancl ??? (- μ (z ∨ y)));
57 apply (eq_trans ?? ? ? (plus_assoc ????));
58 apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??));
59 apply (eq_trans ?? ? ? (zero_neutral ??));
60 apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????));
61 apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??));
62 apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??));
65 lemma step1_3_57: ∀R.∀L:vlattice R.∀x,y,z:L.
66 μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
68 cut (μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z)))); [2:
69 lapply (modular_mjp ?? x (y ∨ z)) as H1;
70 apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? H1); clear H1;
71 apply (eq_trans ?? ? ?? (plus_comm ???));
72 (* apply (eq_trans ?? (0+μ(x∧(y∧z))) ?? (opp_inverse ??)); ASSERT FALSE *)
73 apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z)))); [2: apply eq_sym; apply plus_assoc;]
74 apply (eq_trans ?? (0+μ(x∧(y∨z)))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse;]
75 (* apply (eq_trans ?? ? ? (eq_refl ??) (zero_neutral ??)); ASSERT FALSE *)
76 apply (eq_trans ?? (μ(x∧(y∨z)))); [apply eq_reflexive| apply eq_sym; apply zero_neutral]]
77 apply (eq_trans ?? ? ? Hcut); clear Hcut;
78 cut ( μ(y∨z) ≈ μy + μz + -μ (y ∧ z)); [2:
79 lapply (modular_mjp ?? y z) as H1;
80 apply (plus_cancr ??? (μ(y ∧ z)));
81 apply (eq_trans ?? ? ? H1); clear H1;
82 apply (eq_trans ?? ? ?? (plus_assoc ????));
83 apply (eq_trans ?? (μy+ μz + 0)); [2: apply feq_plusl; apply eq_sym; apply opp_inverse]
84 apply (eq_trans ?? ? ?? (plus_comm ???));
85 apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
87 apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
88 apply feq_plusr; apply feq_plusl; apply Hcut] clear Hcut;
89 apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
90 apply feq_plusl; apply feq_opp;
91 apply (eq_trans ?? ? ? (join_assoc ?????));
92 apply (eq_trans ?? ? ? (join_comm ????));
94 apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
95 apply feq_plusr; apply plus_assoc;
98 lemma meet_join_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)).
100 apply (le_rewr ??? ? (step1_3_57 ?????));
101 apply (le_rewr ??? (μ x + μ y + μ z + -μ (y ∧ z) + -μ(z ∨ (x ∨ y))) (foo ?????));
102 apply (le_rewr ??? (μ x + μ y + μ z + -μ (y ∧ z) + -μ((z ∨ x) ∨ y)));
103 [ apply feq_plusl; apply eq_opp_sym; apply join_assoc;]
104 lapply (meet_join_le ?? z x y);
105 cut (- μ (z ∨ x ∨ y) ≈ - μ (z ∨ x) - μ y + μ (y ∧ (z ∨ x)));
109 lemma join_meet_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z).
110 (* hint per duplicati? *)
112 apply (le_rewr ??? (0 + μ (x ∨ z)) (zero_neutral ??));
113 apply (le_rewr ??? (μ (x ∨ z) + 0) (plus_comm ???));
114 apply (le_rewr ??? (μ (x ∨ z) + (-μ(y ∨ z) + μ(y ∨ z))) (opp_inverse ? ?));