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