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   meet_join_plus: ∀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)
  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 foo: ∀R.∀L:vlattice R.∀x,y,z:L.
  50   μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
  51 intros (R L x y z);
  52 lapply (meet_join_plus ? ? x (y ∨ z)) as H;
  53 lapply (meet_join_plus ? ? y z) as H1;
  54  (*CSC: A questo punto ti servono dei lemmi sui gruppi che non sono ancora
  55    stati dimostrati. E una valanga di passi di riscrittura :-)
  56  *)
  57
  58
  59 lemma meet_join_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)).
  60 intros (R L x y z);
  61 apply (le_rewr ??? (μ x + μ y + μ z + -μ (y ∧ z) + -μ(z ∨ (x ∨ y))) (foo ?????));
  62 apply (le_rewr ??? (μ x + μ y + μ z + -μ (y ∧ z) + -μ((z ∨ x) ∨ y)));
  63   [ apply feq_plusl; apply eq_opp_sym; apply join_assoc;]
  64 lapply (meet_join_le ?? z x y);
  65 cut (- μ (z ∨ x ∨ y) ≈ - μ (z ∨ x) - μ y + μ (y ∧ (z ∨ x)));
  66  [2:
  67
  68
  69 lemma join_meet_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z).
  70 (* hint per duplicati? *)
  71 intros (R L x y z);
  72 apply (le_rewr ??? (0 + μ (x ∨ z)) (zero_neutral ??));
  73 apply (le_rewr ??? (μ (x ∨ z) + 0) (plus_comm ???));
  74 apply (le_rewr ??? (μ (x ∨ z) + (-μ(y ∨ z) + μ(y ∨ z))) (opp_inverse ? ?));
  75
  76
  77