Lattice
A lattice is a semilattice with a join operation such that it forms a semilattice with in the dual partial order.
Record Lattice : Type :=
{ sl :> SemiLattice
; join : sl -> sl -> sl
; l_proof : is_SemiLattice (Dual sl) join
}.
Section Join.
Variable X : Lattice.
Definition makeLattice (po:PartialOrder) (meet join : po -> po -> po) p1 p2 p3 p4 p5 p6 :=
@Build_Lattice (@makeSemiLattice po meet p1 p2 p3) join
(@Build_is_SemiLattice (Dual po) join p4 p5 p6).
{ sl :> SemiLattice
; join : sl -> sl -> sl
; l_proof : is_SemiLattice (Dual sl) join
}.
Section Join.
Variable X : Lattice.
Definition makeLattice (po:PartialOrder) (meet join : po -> po -> po) p1 p2 p3 p4 p5 p6 :=
@Build_Lattice (@makeSemiLattice po meet p1 p2 p3) join
(@Build_is_SemiLattice (Dual po) join p4 p5 p6).
The axioms of a join lattice.
Lemma join_ub_l : forall x y : X, x <= join x y.
Lemma join_ub_r : forall x y : X, y <= join x y.
Lemma join_lub : forall x y z : X, x <= z -> y <= z -> join x y <= z.
Lemma join_ub_r : forall x y : X, y <= join x y.
Lemma join_lub : forall x y z : X, x <= z -> y <= z -> join x y <= z.
Definition Dual : Lattice :=
@makeLattice (Dual X) (@join X) (@meet X)
join_ub_l
join_ub_r
join_lub
(@meet_lb_l X)
(@meet_lb_r X)
(@meet_glb X).
@makeLattice (Dual X) (@join X) (@meet X)
join_ub_l
join_ub_r
join_lub
(@meet_lb_l X)
(@meet_lb_r X)
(@meet_glb X).
All the lemmas about meet semilattices hold for join.
Lemma join_comm : forall x y:X, join x y == join y x.
Lemma join_assoc : forall x y z:X, join x (join y z) == join (join x y) z.
Lemma join_idem : forall x:X, join x x == x.
Lemma le_join_l : forall x y : X, y <= x <-> join x y == x.
Lemma le_join_r : forall x y : X, x <= y <-> join x y == y.
Lemma join_monotone_r : forall a : X, monotone X (join a).
Lemma join_monotone_l : forall a : X, monotone X (fun x => join x a).
Lemma join_le_compat : forall w x y z : X, w<=y -> x<=z -> join w x <= join y z.
End Join.
Section MeetJoin.
Variable X : Lattice.
Lemma join_assoc : forall x y z:X, join x (join y z) == join (join x y) z.
Lemma join_idem : forall x:X, join x x == x.
Lemma le_join_l : forall x y : X, y <= x <-> join x y == x.
Lemma le_join_r : forall x y : X, x <= y <-> join x y == y.
Lemma join_monotone_r : forall a : X, monotone X (join a).
Lemma join_monotone_l : forall a : X, monotone X (fun x => join x a).
Lemma join_le_compat : forall w x y z : X, w<=y -> x<=z -> join w x <= join y z.
End Join.
Section MeetJoin.
Variable X : Lattice.
Lemma about how meet and join interact.
Lemma meet_join_absorb_l_l : forall x y:X, meet x (join x y) == x.
Lemma meet_join_absorb_l_r : forall x y:X, meet x (join y x) == x.
Lemma meet_join_absorb_r_l : forall x y:X, meet (join x y) x == x.
Lemma meet_join_absorb_r_r : forall x y:X, meet (join y x) x == x.
Lemma meet_join_eq : forall x y : X, meet x y == join x y -> x == y.
End MeetJoin.
Section JoinMeet.
Variable X : Lattice.
Lemma meet_join_absorb_l_r : forall x y:X, meet x (join y x) == x.
Lemma meet_join_absorb_r_l : forall x y:X, meet (join x y) x == x.
Lemma meet_join_absorb_r_r : forall x y:X, meet (join y x) x == x.
Lemma meet_join_eq : forall x y : X, meet x y == join x y -> x == y.
End MeetJoin.
Section JoinMeet.
Variable X : Lattice.
The dual of the previous laws holds.
Lemma join_meet_absorb_l_l : forall x y:X, join x (meet x y) == x.
Lemma join_meet_absorb_l_r : forall x y:X, join x (meet y x) == x.
Lemma join_meet_absorb_r_l : forall x y:X, join (meet x y) x == x.
Lemma join_meet_absorb_r_r : forall x y:X, join (meet y x) x == x.
End JoinMeet.
Lemma join_meet_absorb_l_r : forall x y:X, join x (meet y x) == x.
Lemma join_meet_absorb_r_l : forall x y:X, join (meet x y) x == x.
Lemma join_meet_absorb_r_r : forall x y:X, join (meet y x) x == x.
End JoinMeet.