matita/dama/valued_lattice.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/valued_lattice/".
  16
  17 include "ordered_groups.ma".
  18
  19 record vlattice (R : ogroup) : Type ≝ {
  20   vl_carr:> Type;
  21   value: vl_carr → R;
  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 y) ≤ value (meet x (join y z))
  35 }.
  36
  37 interpretation "valued lattice meet" 'and a b =
  38  (cic:/matita/valued_lattice/meet.con _ _ a b).
  39
  40 interpretation "valued lattice join" 'or a b =
  41  (cic:/matita/valued_lattice/join.con _ _ a b).
  42
  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).
  45
  46 notation "\mu" non associative with precedence 80 for @{ 'value }.
  47 interpretation "lattice value" 'value = (cic:/matita/valued_lattice/value.con _ _).
  48
  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)) ? (modular_mjp ??z y));
  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 ??));
  63 qed.
  64
  65 lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
  66 intros (R L y z);
  67 lapply (modular_mjp ?? y z) as H1;
  68 apply (plus_cancr ??? (μ(y ∧ z)));
  69 apply (eq_trans ?? ? ? H1); clear H1;
  70 apply (eq_trans ?? ? ?? (plus_assoc ????));
  71 apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));
  72 apply (eq_trans ?? ? ?? (plus_comm ???));
  73 apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
  74 apply eq_reflexive.
  75 qed.
  76
  77 lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
  78 intros (R L y z);
  79 lapply (modular_mjp ?? y z) as H1;
  80 apply (plus_cancl ??? (μ(y ∨ z)));
  81 apply (eq_trans ?? ? ? H1); clear H1;
  82 apply (eq_trans ????? (plus_comm ???));
  83 apply (eq_trans ?? ? ?? (plus_assoc ????));
  84 apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));
  85 apply (eq_trans ?? ? ?? (plus_comm ???));
  86 apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
  87 apply eq_reflexive.
  88 qed.
  89
  90 lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
  91 intros (R L x y z);
  92 lapply (modular_mjp ?? x (y ∨ z)) as H1;
  93 apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z)))); [2: apply feq_plusr; apply H1;] clear H1;
  94 apply (eq_trans ?? ? ?? (plus_comm ???));
  95 apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????));
  96 apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??));
  97 apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??));
  98 apply eq_reflexive.
  99 qed.
 100
 101 lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
 102 intros (R L x y z);
 103 lapply (modular_mjp ?? x (y ∧ z)) as H1;
 104 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;
 105 apply (eq_trans ?? ? ?? (plus_comm ???));
 106 apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z))); [2: apply eq_sym; apply plus_assoc]
 107 apply (eq_trans ?? (0+ μ(x∨y∧z))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse]
 108 apply eq_sym; apply zero_neutral;
 109 qed.
 110
 111 lemma step1_3_57': ∀R.∀L:vlattice R.∀x,y,z:L.
 112   μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
 113 intros (R L x y z);
 114 apply (eq_trans ?? ? ? (modularjm ?? x y z));
 115 apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [
 116   apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
 117 apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
 118   apply feq_plusl; apply feq_opp;
 119   apply (eq_trans ?? ? ? (meet_assoc ?????));
 120   apply (eq_trans ?? ? ? (meet_comm ????));
 121   apply eq_reflexive;]
 122 apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
 123 apply feq_plusr; apply plus_assoc;
 124 qed.
 125
 126 lemma step1_3_57: ∀R.∀L:vlattice R.∀x,y,z:L.
 127   μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
 128 intros (R L x y z);
 129 apply (eq_trans ?? ? ? (modularmj ?? x y z));
 130 apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
 131   apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);]
 132 apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
 133   apply feq_plusl; apply feq_opp;
 134   apply (eq_trans ?? ? ? (join_assoc ?????));
 135   apply (eq_trans ?? ? ? (join_comm ????));
 136   apply eq_reflexive;]
 137 apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
 138 apply feq_plusr; apply plus_assoc;
 139 qed.
 140
 141 (* LEMMA 3.57 *)
 142
 143 lemma join_meet_le_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z).
 144 intros (R L x y z);
 145 apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????)));
 146 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [
 147   apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;]
 148 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [
 149   apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm]
 150 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [
 151   apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
 152     apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
 153   apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
 154 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [
 155   repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??));
 156   apply join_comm;]
 157 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [
 158   apply eq_sym; apply plus_assoc;]
 159 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [
 160   repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
 161 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [
 162   repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
 163 apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
 164   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 165   apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????)));
 166   apply feq_plusl; apply plus_comm;]
 167 apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
 168   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 169   apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
 170   apply feq_plusl; apply plus_comm;]
 171 apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
 172   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 173   apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
 174   apply opp_inverse; apply eq_reflexive;]
 175 apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
 176   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
 177   apply eq_sym; apply zero_neutral;]
 178 apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
 179   repeat apply feq_plusr; apply plus_comm;]
 180 apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
 181   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 182   apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
 183   apply plus_comm;]
 184 apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
 185   repeat apply feq_plusr; apply modularj;]
 186 apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????));
 187 apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
 188 apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse]
 189 apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;]
 190 repeat apply fle_plusl; apply join_meet_le;
 191 qed.
 192
 193 lemma meet_le_meet_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)).
 194 intros (R L x y z);
 195 apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????)));
 196 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [
 197   apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;]
 198 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [
 199   apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj]
 200 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [
 201   apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
 202     apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
 203   apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
 204 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [
 205   repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??));
 206   apply meet_comm;]
 207 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [
 208   apply eq_sym; apply plus_assoc;]
 209 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [
 210   repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
 211 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [
 212   repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
 213 apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
 214   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 215   apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????)));
 216   apply feq_plusl; apply plus_comm;]
 217 apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
 218   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 219   apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
 220   apply feq_plusl; apply plus_comm;]
 221 apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
 222   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 223   apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
 224   apply opp_inverse; apply eq_reflexive;]
 225 apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
 226   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
 227   apply eq_sym; apply zero_neutral;]
 228 apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
 229   repeat apply feq_plusr; apply plus_comm;]
 230 apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
 231   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
 232   apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
 233   apply plus_comm;]
 234 apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
 235   repeat apply feq_plusr; apply modularm;]
 236 apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????));
 237 apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
 238 apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse]
 239 apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;]
 240 repeat apply fle_plusl; apply meet_join_le;
 241 qed.