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 set "baseuri" "cic:/matita/lattice/".
  16
  17 include "excess.ma".
  18
  19 record lattice : Type ≝ {
  20   l_carr:> apartness;
  21   join: l_carr → l_carr → l_carr;
  22   meet: l_carr → l_carr → l_carr;
  23   join_refl: ∀x.join x x ≈ x;
  24   meet_refl: ∀x.meet x x ≈ x;
  25   join_comm: ∀x,y:l_carr. join x y ≈ join y x;
  26   meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
  27   join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z;
  28   meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z;
  29   absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
  30   absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f;
  31   strong_extj: ∀x.strong_ext ? (join x);
  32   strong_extm: ∀x.strong_ext ? (meet x)
  33 }.
  34
  35 interpretation "Lattice meet" 'and a b =
  36  (cic:/matita/lattice/meet.con _ a b).
  37
  38 interpretation "Lattice join" 'or a b =
  39  (cic:/matita/lattice/join.con _ a b).
  40
  41 definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
  42
  43 lemma excess_of_lattice: lattice → excess.
  44 intro l; apply (mk_excess l (excl l));
  45 [ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
  46   apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
  47 | intros 3 (x y z); unfold excl; intro H;
  48   cases (ap_cotransitive ??? (x∧z∧y) H) (H1 H2); [2:
  49     left; apply ap_symmetric; apply (strong_extm ? y);
  50     apply (ap_rewl ???? (meet_comm ???));
  51     apply (ap_rewr ???? (meet_comm ???));
  52     assumption]
  53   cases (ap_cotransitive ??? (x∧z) H1) (H2 H3); [left; assumption]
  54   right; apply (strong_extm ? x); apply (ap_rewr ???? (meet_assoc ????));
  55   assumption]
  56 qed.
  57
  58 coercion cic:/matita/lattice/excess_of_lattice.con.
  59
  60 lemma feq_ml: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
  61 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
  62 intro H1; apply H; clear H; apply (strong_extm ???? H1);
  63 qed.
  64
  65 lemma feq_jl: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∨ a) ≈ (c ∨ b).
  66 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
  67 intro H1; apply H; clear H; apply (strong_extj ???? H1);
  68 qed.
  69
  70 lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
  71 intros (l a b H);
  72   unfold le in H; unfold excess_of_lattice in H;
  73   unfold excl in H; simplify in H;
  74 unfold eq; assumption;
  75 qed.
  76
  77 lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
  78 intros (l a b H); lapply (le_to_eqm ??? H) as H1;
  79 lapply (feq_jl ??? b H1) as H2;
  80 apply (Eq≈ ?? (join_comm ???));
  81 apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
  82 apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
  83 apply eq_sym; apply absorbjm;
  84 qed.
  85
  86
  87