Record is_SemiLattice (po : PartialOrder) (meet : po -> po -> po) : Prop :=
{ sl_meet_lb_l : forall x y, meet x y <= x
; sl_meet_lb_r : forall x y, meet x y <= y
; sl_meet_glb : forall x y z, z <= x -> z <= y -> z <= meet x y
}.
Record SemiLattice : Type :=
{ po :> PartialOrder
; meet : po -> po -> po
; sl_proof : is_SemiLattice po meet
}.
Section Meet.
Variable X : SemiLattice.
Definition makeSemiLattice po meet p1 p2 p3 :=
@Build_SemiLattice po meet
(@Build_is_SemiLattice po meet p1 p2 p3).
The axioms and basic properties of a semi lattice
Lemma meet_lb_l : forall x y : X, meet x y <= x.
Lemma meet_lb_r : forall x y : X, meet x y <= y.
Lemma meet_glb : forall x y z : X, z <= x -> z <= y -> z <= meet x y.
Lemma meet_lb_r : forall x y : X, meet x y <= y.
Lemma meet_glb : forall x y z : X, z <= x -> z <= y -> z <= meet x y.
commutativity of meet
associativity of meet
idempotency of meet
Lemma meet_idem : forall x:X, meet x x == x.
Lemma le_meet_l : forall x y : X, x <= y <-> meet x y == x.
Lemma le_meet_r : forall x y : X, y <= x <-> meet x y == y.
Lemma le_meet_l : forall x y : X, x <= y <-> meet x y == x.
Lemma le_meet_r : forall x y : X, y <= x <-> meet x y == y.
monotonicity of meet
Lemma meet_monotone_r : forall a : X, monotone X (meet a).
Lemma meet_monotone_l : forall a : X, monotone X (fun x => meet x a).
Lemma meet_le_compat : forall w x y z : X, w<=y -> x<=z -> meet w x <= meet y z.
End Meet.
Lemma meet_monotone_l : forall a : X, monotone X (fun x => meet x a).
Lemma meet_le_compat : forall w x y z : X, w<=y -> x<=z -> meet w x <= meet y z.
End Meet.