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 (**************************************************************************)
17 include "ordered_group.ma".
19 record vlattice (R : togroup) : Type ≝ {
22 join: wl_carr → wl_carr → wl_carr;
23 meet: wl_carr → wl_carr → wl_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 y) ≤ value (meet x (join y z))
37 interpretation "valued lattice meet" 'and a b =
38 (cic:/matita/prevalued_lattice/meet.con _ _ a b).
40 interpretation "valued lattice join" 'or a b =
41 (cic:/matita/prevalued_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/prevalued_lattice/value.con _ _ a).
46 notation "\mu" non associative with precedence 80 for @{ 'value }.
47 interpretation "lattice value" 'value = (cic:/matita/prevalued_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≈ (μz + μx) (modular_mjp ????));
54 apply (Eq≈ (μz + μy) H); clear H;
55 apply (Eq≈ (μ(z∨y) + μ(z∧y)) (modular_mjp ??z y));
56 apply (plus_cancl ??? (- μ (z ∨ y)));
57 apply (Eq≈ ? (plus_assoc ????));
58 apply (Eq≈ (0+ μ(z∧y)) (opp_inverse ??));
59 apply (Eq≈ ? (zero_neutral ??));
60 apply (Eq≈ (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ? (plus_assoc ????));
61 apply (Eq≈ (0+ μ(z∧x)) ? (opp_inverse ??));
62 apply (Eq≈ (μ (z ∧ x)) H1 (zero_neutral ??));
65 lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
67 lapply (modular_mjp ?? y z) as H1;
68 apply (plus_cancr ??? (μ(y ∧ z)));
69 apply (Eq≈ ? H1); clear H1;
70 apply (Eq≈ ?? (plus_assoc ????));
71 apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??));
72 apply (Eq≈ ?? (plus_comm ???));
73 apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
77 lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
78 (* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *)
81 lapply (modular_mjp ?? y z) as H1;
82 apply (plus_cancl ??? (μ(y ∨ z)));
83 apply (Eq≈ ? H1); clear H1;
84 apply (Eq≈ ?? (plus_comm ???));
85 apply (Eq≈ ?? (plus_assoc ????));
86 apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??));
87 apply (Eq≈ ?? (plus_comm ???));
88 apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
92 lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
94 lapply (modular_mjp ?? x (y ∨ z)) as H1;
95 apply (Eq≈ (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ? (feq_plusr ???? H1)); clear H1;
96 apply (Eq≈ ? ? (plus_comm ???));
97 apply (Eq≈ (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ? (plus_assoc ????));
98 apply (Eq≈ (0+μ(x∧(y∨z))) ? (opp_inverse ??));
99 apply (Eq≈ (μ(x∧(y∨z))) ? (zero_neutral ??));
103 lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
105 lapply (modular_mjp ?? x (y ∧ z)) as H1;
106 apply (Eq≈ (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
107 apply (Eq≈ ? ? (plus_comm ???));
108 apply (Eq≈ (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ? (plus_assoc ????));
109 apply (Eq≈ (0+ μ(x∨y∧z)) ? (opp_inverse ??));
110 apply eq_sym; apply zero_neutral;
113 lemma step1_3_57': ∀R.∀L:vlattice R.∀x,y,z:L.
114 μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
116 apply (Eq≈ ? (modularjm ?? x y z));
117 apply (Eq≈ ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z)))); [
118 apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
119 apply (Eq≈ (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
120 apply feq_plusl; apply feq_opp;
121 apply (Eq≈ ? (meet_assoc ?????));
122 apply (Eq≈ ? (meet_comm ????));
124 apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
125 apply feq_plusr; apply plus_assoc;
128 lemma step1_3_57: ∀R.∀L:vlattice R.∀x,y,z:L.
129 μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
131 apply (Eq≈ ? (modularmj ?? x y z));
132 apply (Eq≈ ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z)))); [
133 apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);]
134 apply (Eq≈ (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
135 apply feq_plusl; apply feq_opp;
136 apply (Eq≈ ? (join_assoc ?????));
137 apply (Eq≈ ? (join_comm ????));
139 apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
140 apply feq_plusr; apply plus_assoc;
145 lemma join_meet_le_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z).
147 apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????)));
148 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [
149 apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;]
150 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [
151 apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm]
152 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [
153 apply feq_plusl; apply (Eq≈ (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
154 apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
155 apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
156 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [
157 repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∧x)∨y)) (eq_opp_opp_x_x ??));
159 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [
160 apply eq_sym; apply plus_assoc;]
161 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [
162 repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
163 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [
164 repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
165 apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
166 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
167 apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∨z))) (eq_sym ??? (plus_assoc ????)));
168 apply feq_plusl; apply plus_comm;]
169 apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
170 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
171 apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????)));
172 apply feq_plusl; apply plus_comm;]
173 apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
174 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
175 apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
176 apply opp_inverse; apply eq_reflexive;]
177 apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
178 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
179 apply eq_sym; apply zero_neutral;]
180 apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
181 repeat apply feq_plusr; apply plus_comm;]
182 apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
183 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
184 apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
186 apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
187 repeat apply feq_plusr; apply modularj;]
188 apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????));
189 apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
190 apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse]
191 apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;]
192 repeat apply fle_plusl; apply join_meet_le;
195 lemma meet_le_meet_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)).
197 apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????)));
198 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [
199 apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;]
200 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [
201 apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj]
202 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [
203 apply feq_plusl; apply (Eq≈ (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
204 apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
205 apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
206 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [
207 repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∨x)∧y)) (eq_opp_opp_x_x ??));
209 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [
210 apply eq_sym; apply plus_assoc;]
211 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [
212 repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
213 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [
214 repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
215 apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
216 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
217 apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∧z))) (eq_sym ??? (plus_assoc ????)));
218 apply feq_plusl; apply plus_comm;]
219 apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
220 repeat apply feq_plusr; apply (Eq≈ ?? (plus_assoc ????));
221 apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????)));
222 apply feq_plusl; apply plus_comm;]
223 apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
224 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
225 apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
226 apply opp_inverse; apply eq_reflexive;]
227 apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
228 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
229 apply eq_sym; apply zero_neutral;]
230 apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
231 repeat apply feq_plusr; apply plus_comm;]
232 apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
233 repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
234 apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
236 apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
237 repeat apply feq_plusr; apply modularm;]
238 apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????));
239 apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
240 apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse]
241 apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;]
242 repeat apply fle_plusl; apply meet_join_le;