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 directed : Type ≝ {
  18   dir_carr: apartness;
  19   dir_op: dir_carr → dir_carr → dir_carr;
  20   dir_op_refl: ∀x.dir_op x x ≈ x;
  21   dir_op_comm: ∀x,y:dir_carr. dir_op x y ≈ dir_op y x;
  22   dir_op_assoc: ∀x,y,z:dir_carr. dir_op x (dir_op y z) ≈ dir_op (dir_op x y) z;
  23   dir_strong_extop: ∀x.strong_ext ? (dir_op x)
  24 }.
  25
  26 definition excl ≝
  27   λl:directed.λa,b:dir_carr l.ap_apart (dir_carr l) a (dir_op l a b).
  28
  29 lemma excess_of_directed: directed → excess.
  30 intro l; apply (mk_excess (dir_carr l) (excl l));
  31 [ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive (dir_carr l) x);
  32   apply (ap_rewr ??? (dir_op l x x) (dir_op_refl ? x)); assumption;
  33 | intros 3 (x y z); unfold excl; intro H;
  34   cases (ap_cotransitive ??? (dir_op l (dir_op l x z) y) H) (H1 H2); [2:
  35     left; apply ap_symmetric; apply (dir_strong_extop ? y);
  36     apply (ap_rewl ???? (dir_op_comm ???));
  37     apply (ap_rewr ???? (dir_op_comm ???));
  38     assumption]
  39   cases (ap_cotransitive ??? (dir_op l x z) H1) (H2 H3); [left; assumption]
  40   right; apply (dir_strong_extop ? x); apply (ap_rewr ???? (dir_op_assoc ????));
  41   assumption]
  42 qed.
  43
  44 record prelattice : Type ≝ {
  45   pl_carr:> excess;
  46   meet: pl_carr → pl_carr → pl_carr;
  47   meet_refl: ∀x.meet x x ≈ x;
  48   meet_comm: ∀x,y:pl_carr. meet x y ≈ meet y x;
  49   meet_assoc: ∀x,y,z:pl_carr. meet x (meet y z) ≈ meet (meet x y) z;
  50   strong_extm: ∀x.strong_ext ? (meet x);
  51   le_to_eqm: ∀x,y.x ≤ y → x ≈ meet x y;
  52   lem: ∀x,y.(meet x y) ≤ y
  53 }.
  54
  55 interpretation "prelattice meet" 'and a b =
  56   (cic:/matita/lattice/meet.con _ a b).
  57
  58 lemma feq_ml: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
  59 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
  60 intro H1; apply H; clear H; apply (strong_extm ???? H1);
  61 qed.
  62
  63 lemma feq_mr: ∀ml:prelattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
  64 intros (l a b c H);
  65 apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
  66 apply feq_ml; assumption;
  67 qed.
  68
  69 lemma prelattice_of_directed: directed → prelattice.
  70 intro l_; apply (mk_prelattice (excess_of_directed l_)); [apply (dir_op l_);]
  71 unfold excess_of_directed; try unfold apart_of_excess; simplify;
  72 unfold excl; simplify;
  73 [intro x; intro H; elim H; clear H;
  74  [apply (dir_op_refl l_ x);
  75   lapply (Ap≫ ? (dir_op_comm ???) t) as H; clear t;
  76   lapply (dir_strong_extop l_ ??? H); apply ap_symmetric; assumption
  77  | lapply (Ap≪ ? (dir_op_refl ?x) t) as H; clear t;
  78    lapply (dir_strong_extop l_ ??? H); apply (dir_op_refl l_ x);
  79    apply ap_symmetric; assumption]
  80 |intros 3 (x y H); cases H (H1 H2); clear H;
  81  [lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ x y)) H1) as H; clear H1;
  82   lapply (dir_strong_extop l_ ??? H) as H1; clear H;
  83   lapply (Ap≪ ? (dir_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
  84  |lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ y x)) H2) as H; clear H2;
  85   lapply (dir_strong_extop l_ ??? H) as H1; clear H;
  86   lapply (Ap≪ ? (dir_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
  87 |intros 4 (x y z H); cases H (H1 H2); clear H;
  88  [lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ x (dir_op l_ y z))) H1) as H; clear H1;
  89   lapply (dir_strong_extop l_ ??? H) as H1; clear H;
  90   lapply (Ap≪ ? (eq_sym ??? (dir_op_assoc ?x y z)) H1) as H; clear H1;
  91   apply (ap_coreflexive ?? H);
  92  |lapply (Ap≪ ? (dir_op_refl ? (dir_op l_ (dir_op l_ x y) z)) H2) as H; clear H2;
  93   lapply (dir_strong_extop l_ ??? H) as H1; clear H;
  94   lapply (Ap≪ ? (dir_op_assoc ?x y z) H1) as H; clear H1;
  95   apply (ap_coreflexive ?? H);]
  96 |intros (x y z H); elim H (H1 H1); clear H;
  97  lapply (Ap≪ ? (dir_op_refl ??) H1) as H; clear H1;
  98  lapply (dir_strong_extop l_ ??? H) as H1; clear H;
  99  lapply (dir_strong_extop l_ ??? H1) as H; clear H1;
 100  cases (ap_cotransitive ??? (dir_op l_ y z) H);[left|right|right|left] try assumption;
 101  [apply ap_symmetric;apply (Ap≪ ? (dir_op_comm ???));
 102  |apply (Ap≫ ? (dir_op_comm ???));
 103  |apply ap_symmetric;] assumption;
 104 |intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
 105  lapply (Ap≪ ? (dir_op_refl ??) H) as H1; clear H;
 106  lapply (dir_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
 107  assumption
 108 |intros 3 (x y H);
 109  cut (dir_op l_ x y ≈ dir_op l_ x (dir_op l_ y y)) as H1;[2:
 110    intro; lapply (dir_strong_extop ???? a); apply (dir_op_refl l_ y);
 111    apply ap_symmetric; assumption;]
 112  lapply (Ap≪ ? (eq_sym ??? H1) H); apply (dir_op_assoc l_ x y y);
 113  assumption; ]
 114 qed.
 115
 116 record lattice_ : Type ≝ {
 117   latt_mcarr:> prelattice;
 118   latt_jcarr_: prelattice;
 119   latt_with: pl_carr latt_jcarr_ = dual_exc (pl_carr latt_mcarr)
 120 }.
 121
 122 lemma latt_jcarr : lattice_ → prelattice.
 123 intro l;
 124 apply (mk_prelattice (dual_exc l)); unfold excess_OF_lattice_;
 125 cases (latt_with l); simplify;
 126 [apply meet|apply meet_refl|apply meet_comm|apply meet_assoc|
 127 apply strong_extm| apply le_to_eqm|apply lem]
 128 qed.
 129
 130 coercion cic:/matita/lattice/latt_jcarr.con.
 131
 132 interpretation "Lattice meet" 'and a b =
 133  (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
 134
 135 interpretation "Lattice join" 'or a b =
 136  (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
 137
 138 record lattice : Type ≝ {
 139   latt_carr:> lattice_;
 140   absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
 141   absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
 142 }.
 143
 144 notation "'meet'"        non associative with precedence 50 for @{'meet}.
 145 notation "'meet_refl'"   non associative with precedence 50 for @{'meet_refl}.
 146 notation "'meet_comm'"   non associative with precedence 50 for @{'meet_comm}.
 147 notation "'meet_assoc'"  non associative with precedence 50 for @{'meet_assoc}.
 148 notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
 149 notation "'le_to_eqm'"   non associative with precedence 50 for @{'le_to_eqm}.
 150 notation "'lem'"         non associative with precedence 50 for @{'lem}.
 151 notation "'join'"        non associative with precedence 50 for @{'join}.
 152 notation "'join_refl'"   non associative with precedence 50 for @{'join_refl}.
 153 notation "'join_comm'"   non associative with precedence 50 for @{'join_comm}.
 154 notation "'join_assoc'"  non associative with precedence 50 for @{'join_assoc}.
 155 notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
 156 notation "'le_to_eqj'"   non associative with precedence 50 for @{'le_to_eqj}.
 157 notation "'lej'"         non associative with precedence 50 for @{'lej}.
 158
 159 interpretation "Lattice meet"        'meet = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _)).
 160 interpretation "Lattice meet_refl"   'meet_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
 161 interpretation "Lattice meet_comm"   'meet_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
 162 interpretation "Lattice meet_assoc"  'meet_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
 163 interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
 164 interpretation "Lattice le_to_eqm"   'le_to_eqm = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
 165 interpretation "Lattice lem"         'lem = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_mcarr.con _)).
 166 interpretation "Lattice join"        'join = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _)).
 167 interpretation "Lattice join_refl"   'join_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
 168 interpretation "Lattice join_comm"   'join_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
 169 interpretation "Lattice join_assoc"  'join_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
 170 interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
 171 interpretation "Lattice le_to_eqj"   'le_to_eqj = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
 172 interpretation "Lattice lej"         'lej = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_jcarr.con _)).
 173
 174 notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
 175 notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
 176 interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
 177 interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
 178 notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
 179 notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
 180 interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
 181 interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
 182