helm/software/matita/dama/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 include "excess.ma".
  16
  17 record semi_lattice_base : Type ≝ {
  18   sl_carr:> apartness;
  19   sl_op: sl_carr → sl_carr → sl_carr;
  20   sl_op_refl: ∀x.sl_op x x ≈ x;
  21   sl_op_comm: ∀x,y:sl_carr. sl_op x y ≈ sl_op y x;
  22   sl_op_assoc: ∀x,y,z:sl_carr. sl_op x (sl_op y z) ≈ sl_op (sl_op x y) z;
  23   sl_strong_extop: ∀x.strong_ext ? (sl_op x)
  24 }.
  25
  26 notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }.
  27 interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b).
  28
  29 lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
  30 intro l;
  31 apply mk_excess;
  32 [1: apply mk_excess_;
  33     [1:
  34
  35   apply (mk_excess_base (sl_carr l));
  36     [1: apply (λa,b:sl_carr l.a # (a ✗ b));
  37     |2: unfold; intros 2 (x H); simplify in H;
  38         lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
  39         apply (ap_coreflexive ?? H1);
  40     |3: unfold; simplify; intros (x y z H1);
  41         cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
  42           lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
  43           lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
  44           lapply (sl_strong_extop ???? H22); clear H22;
  45           left; apply ap_symmetric; assumption;]
  46         cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
  47         right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
  48         apply (sl_strong_extop ???? H31);]
  49
  50     |2:
  51     apply apartness_of_excess_base;
  52
  53   apply (mk_excess_base (sl_carr l));
  54     [1: apply (λa,b:sl_carr l.a # (a ✗ b));
  55     |2: unfold; intros 2 (x H); simplify in H;
  56         lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
  57         apply (ap_coreflexive ?? H1);
  58     |3: unfold; simplify; intros (x y z H1);
  59         cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2:
  60           lapply (Ap≪ ? (sl_op_comm ???) H2) as H21;
  61           lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2;
  62           lapply (sl_strong_extop ???? H22); clear H22;
  63           left; apply ap_symmetric; assumption;]
  64         cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption]
  65         right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31;
  66         apply (sl_strong_extop ???? H31);]
  67
  68     |3: apply refl_eq;]
  69 |2,3: intros (x y H); assumption;]
  70 qed.
  71
  72 record semi_lattice : Type ≝ {
  73   sl_exc:> excess;
  74   meet: sl_exc → sl_exc → sl_exc;
  75   meet_refl: ∀x.meet x x ≈ x;
  76   meet_comm: ∀x,y. meet x y ≈ meet y x;
  77   meet_assoc: ∀x,y,z. meet x (meet y z) ≈ meet (meet x y) z;
  78   strong_extm: ∀x.strong_ext ? (meet x);
  79   le_to_eqm: ∀x,y.x ≤ y → x ≈ meet x y;
  80   lem: ∀x,y.(meet x y) ≤ y
  81 }.
  82
  83 interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/meet.con _ a b).
  84
  85 lemma feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
  86 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
  87 intro H1; apply H; clear H; apply (strong_extm ???? H1);
  88 qed.
  89
  90 lemma feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
  91 intros (l a b c H);
  92 apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
  93 apply feq_ml; assumption;
  94 qed.
  95
  96
  97 (*
  98 lemma semi_lattice_of_semi_lattice_base: semi_lattice_base → semi_lattice.
  99 intro slb; apply (mk_semi_lattice (excess_of_semi_lattice_base slb));
 100 [1: apply (sl_op slb);
 101 |2: intro x; apply (eq_trans (excess_of_semi_lattice_base slb)); [2:
 102       apply (sl_op_refl slb);|1:skip] (sl_op slb x x)); ? (sl_op_refl slb x));
 103
 104  unfold excess_of_semi_lattice_base; simplify;
 105     intro H; elim H;
 106     [
 107
 108
 109     lapply (ap_rewl (excess_of_semi_lattice_base slb) x ? (sl_op slb x x)
 110       (eq_sym (excess_of_semi_lattice_base slb) ?? (sl_op_refl slb x)) t);
 111     change in x with (sl_carr slb);
 112     apply (Ap≪ (x ✗ x)); (sl_op_refl slb x));
 113
 114 whd in H; elim H; clear H;
 115     [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t);
 116
 117 prelattice (excess_of_directed l_)); [apply (sl_op l_);]
 118 unfold excess_of_directed; try unfold apart_of_excess; simplify;
 119 unfold excl; simplify;
 120 [intro x; intro H; elim H; clear H;
 121  [apply (sl_op_refl l_ x);
 122   lapply (Ap≫ ? (sl_op_comm ???) t) as H; clear t;
 123   lapply (sl_strong_extop l_ ??? H); apply ap_symmetric; assumption
 124  | lapply (Ap≪ ? (sl_op_refl ?x) t) as H; clear t;
 125    lapply (sl_strong_extop l_ ??? H); apply (sl_op_refl l_ x);
 126    apply ap_symmetric; assumption]
 127 |intros 3 (x y H); cases H (H1 H2); clear H;
 128  [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x y)) H1) as H; clear H1;
 129   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 130   lapply (Ap≪ ? (sl_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
 131  |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ y x)) H2) as H; clear H2;
 132   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 133   lapply (Ap≪ ? (sl_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
 134 |intros 4 (x y z H); cases H (H1 H2); clear H;
 135  [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x (sl_op l_ y z))) H1) as H; clear H1;
 136   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 137   lapply (Ap≪ ? (eq_sym ??? (sl_op_assoc ?x y z)) H1) as H; clear H1;
 138   apply (ap_coreflexive ?? H);
 139  |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ (sl_op l_ x y) z)) H2) as H; clear H2;
 140   lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 141   lapply (Ap≪ ? (sl_op_assoc ?x y z) H1) as H; clear H1;
 142   apply (ap_coreflexive ?? H);]
 143 |intros (x y z H); elim H (H1 H1); clear H;
 144  lapply (Ap≪ ? (sl_op_refl ??) H1) as H; clear H1;
 145  lapply (sl_strong_extop l_ ??? H) as H1; clear H;
 146  lapply (sl_strong_extop l_ ??? H1) as H; clear H1;
 147  cases (ap_cotransitive ??? (sl_op l_ y z) H);[left|right|right|left] try assumption;
 148  [apply ap_symmetric;apply (Ap≪ ? (sl_op_comm ???));
 149  |apply (Ap≫ ? (sl_op_comm ???));
 150  |apply ap_symmetric;] assumption;
 151 |intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
 152  lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
 153  lapply (sl_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
 154  assumption
 155 |intros 3 (x y H);
 156  cut (sl_op l_ x y ≈ sl_op l_ x (sl_op l_ y y)) as H1;[2:
 157    intro; lapply (sl_strong_extop ???? a); apply (sl_op_refl l_ y);
 158    apply ap_symmetric; assumption;]
 159  lapply (Ap≪ ? (eq_sym ??? H1) H); apply (sl_op_assoc l_ x y y);
 160  assumption; ]
 161 qed.
 162 *)
 163
 164
 165 record lattice_ : Type ≝ {
 166   latt_mcarr:> semi_lattice;
 167   latt_jcarr_: semi_lattice;
 168   latt_with:  sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr)
 169 }.
 170
 171 lemma latt_jcarr : lattice_ → semi_lattice.
 172 intro l;
 173 apply (mk_semi_lattice (dual_exc l));
 174 unfold excess_OF_lattice_;
 175 cases (latt_with l); simplify;
 176 [apply meet|apply meet_refl|apply meet_comm|apply meet_assoc|
 177 apply strong_extm| apply le_to_eqm|apply lem]
 178 qed.
 179
 180 coercion cic:/matita/lattice/latt_jcarr.con.
 181
 182 interpretation "Lattice meet" 'and a b =
 183  (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
 184
 185 interpretation "Lattice join" 'or a b =
 186  (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
 187
 188 record lattice : Type ≝ {
 189   latt_carr:> lattice_;
 190   absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
 191   absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
 192 }.
 193
 194 notation "'meet'"        non associative with precedence 50 for @{'meet}.
 195 notation "'meet_refl'"   non associative with precedence 50 for @{'meet_refl}.
 196 notation "'meet_comm'"   non associative with precedence 50 for @{'meet_comm}.
 197 notation "'meet_assoc'"  non associative with precedence 50 for @{'meet_assoc}.
 198 notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
 199 notation "'le_to_eqm'"   non associative with precedence 50 for @{'le_to_eqm}.
 200 notation "'lem'"         non associative with precedence 50 for @{'lem}.
 201 notation "'join'"        non associative with precedence 50 for @{'join}.
 202 notation "'join_refl'"   non associative with precedence 50 for @{'join_refl}.
 203 notation "'join_comm'"   non associative with precedence 50 for @{'join_comm}.
 204 notation "'join_assoc'"  non associative with precedence 50 for @{'join_assoc}.
 205 notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
 206 notation "'le_to_eqj'"   non associative with precedence 50 for @{'le_to_eqj}.
 207 notation "'lej'"         non associative with precedence 50 for @{'lej}.
 208
 209 interpretation "Lattice meet"        'meet = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _)).
 210 interpretation "Lattice meet_refl"   'meet_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
 211 interpretation "Lattice meet_comm"   'meet_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
 212 interpretation "Lattice meet_assoc"  'meet_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
 213 interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
 214 interpretation "Lattice le_to_eqm"   'le_to_eqm = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
 215 interpretation "Lattice lem"         'lem = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_mcarr.con _)).
 216 interpretation "Lattice join"        'join = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _)).
 217 interpretation "Lattice join_refl"   'join_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
 218 interpretation "Lattice join_comm"   'join_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
 219 interpretation "Lattice join_assoc"  'join_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
 220 interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
 221 interpretation "Lattice le_to_eqj"   'le_to_eqj = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
 222 interpretation "Lattice lej"         'lej = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_jcarr.con _)).
 223
 224 notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
 225 notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
 226 interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
 227 interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
 228 notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
 229 notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
 230 interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
 231 interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
 232