1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/lattice/".
19 record lattice : Type ≝ {
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)
35 interpretation "Lattice meet" 'and a b =
36 (cic:/matita/lattice/meet.con _ a b).
38 interpretation "Lattice join" 'or a b =
39 (cic:/matita/lattice/join.con _ a b).
41 definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
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 ???));
53 cases (ap_cotransitive ??? (x∧z) H1) (H2 H3); [left; assumption]
54 right; apply (strong_extm ? x); apply (ap_rewr ???? (meet_assoc ????));
58 coercion cic:/matita/lattice/excess_of_lattice.con.
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);
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);
70 lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
72 unfold le in H; unfold excess_of_lattice in H;
73 unfold excl in H; simplify in H;
74 unfold eq; assumption;
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;