CoRN.order.SemiLattice
Record is_SemiLattice (po : PartialOrder) (meet : po → po → po) : Prop :=
{ sl_meet_lb_l : ∀ x y, meet x y ≤ x
; sl_meet_lb_r : ∀ x y, meet x y ≤ y
; sl_meet_glb : ∀ 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 : ∀ x y : X, meet x y ≤ x.
Proof (sl_meet_lb_l _ _ (sl_proof X)).
Lemma meet_lb_r : ∀ x y : X, meet x y ≤ y.
Proof (sl_meet_lb_r _ _ (sl_proof X)).
Lemma meet_glb : ∀ x y z : X, z ≤ x → z ≤ y → z ≤ meet x y.
Proof (sl_meet_glb _ _ (sl_proof X)).
Proof (sl_meet_lb_l _ _ (sl_proof X)).
Lemma meet_lb_r : ∀ x y : X, meet x y ≤ y.
Proof (sl_meet_lb_r _ _ (sl_proof X)).
Lemma meet_glb : ∀ x y z : X, z ≤ x → z ≤ y → z ≤ meet x y.
Proof (sl_meet_glb _ _ (sl_proof X)).
commutativity of meet
Lemma meet_comm : ∀ x y:X, meet x y == meet y x.
Proof.
assert (∀ x y : X, meet x y ≤ meet y x).
intros.
destruct X.
simpl in ×.
firstorder.
intros; apply le_antisym; firstorder.
Qed.
Proof.
assert (∀ x y : X, meet x y ≤ meet y x).
intros.
destruct X.
simpl in ×.
firstorder.
intros; apply le_antisym; firstorder.
Qed.
associativity of meet
Lemma meet_assoc : ∀ x y z:X, meet x (meet y z) == meet (meet x y) z.
Proof.
assert (∀ x y z : X, meet x (meet y z) ≤ meet (meet x y) z).
intros.
apply meet_glb; [apply meet_glb|]; firstorder using meet_lb_l meet_lb_r le_trans.
intros.
apply le_antisym.
apply H.
rewrite → meet_comm.
rewrite → (meet_comm x (meet y z)).
rewrite → (meet_comm x y).
rewrite → (meet_comm y z).
apply H.
Qed.
Proof.
assert (∀ x y z : X, meet x (meet y z) ≤ meet (meet x y) z).
intros.
apply meet_glb; [apply meet_glb|]; firstorder using meet_lb_l meet_lb_r le_trans.
intros.
apply le_antisym.
apply H.
rewrite → meet_comm.
rewrite → (meet_comm x (meet y z)).
rewrite → (meet_comm x y).
rewrite → (meet_comm y z).
apply H.
Qed.
idempotency of meet
Lemma meet_idem : ∀ x:X, meet x x == x.
Proof.
intros.
apply le_antisym; firstorder using meet_lb_l meet_glb le_refl.
Qed.
Lemma le_meet_l : ∀ x y : X, x ≤ y ↔ meet x y == x.
Proof.
intros.
split; intros.
apply le_antisym.
apply meet_lb_l.
apply meet_glb.
apply le_refl.
assumption.
rewrite <- H.
apply meet_lb_r.
Qed.
Lemma le_meet_r : ∀ x y : X, y ≤ x ↔ meet x y == y.
Proof.
intros.
rewrite → meet_comm.
apply le_meet_l.
Qed.
Proof.
intros.
apply le_antisym; firstorder using meet_lb_l meet_glb le_refl.
Qed.
Lemma le_meet_l : ∀ x y : X, x ≤ y ↔ meet x y == x.
Proof.
intros.
split; intros.
apply le_antisym.
apply meet_lb_l.
apply meet_glb.
apply le_refl.
assumption.
rewrite <- H.
apply meet_lb_r.
Qed.
Lemma le_meet_r : ∀ x y : X, y ≤ x ↔ meet x y == y.
Proof.
intros.
rewrite → meet_comm.
apply le_meet_l.
Qed.
monotonicity of meet
Lemma meet_monotone_r : ∀ a : X, monotone X (meet a).
Proof.
intros.
rewrite → monotone_def.
intros.
revert H;rewrite → le_meet_l, meet_comm; intro.
rewrite <- H.
rewrite → meet_assoc.
apply meet_lb_l.
Qed.
Lemma meet_monotone_l : ∀ a : X, monotone X (fun x ⇒ meet x a).
Proof.
intros.
assert (A:=meet_monotone_r a).
revert A; do 2 rewrite → monotone_def;intros.
rewrite → (meet_comm x), (meet_comm y);auto.
Qed.
Lemma meet_le_compat : ∀ w x y z : X, w≤y → x≤z → meet w x ≤ meet y z.
Proof.
intros.
apply le_trans with (y:=meet y x).
firstorder using meet_monotone_l monotone_def.
firstorder using meet_monotone_r monotone_def.
Qed.
End Meet.
Proof.
intros.
rewrite → monotone_def.
intros.
revert H;rewrite → le_meet_l, meet_comm; intro.
rewrite <- H.
rewrite → meet_assoc.
apply meet_lb_l.
Qed.
Lemma meet_monotone_l : ∀ a : X, monotone X (fun x ⇒ meet x a).
Proof.
intros.
assert (A:=meet_monotone_r a).
revert A; do 2 rewrite → monotone_def;intros.
rewrite → (meet_comm x), (meet_comm y);auto.
Qed.
Lemma meet_le_compat : ∀ w x y z : X, w≤y → x≤z → meet w x ≤ meet y z.
Proof.
intros.
apply le_trans with (y:=meet y x).
firstorder using meet_monotone_l monotone_def.
firstorder using meet_monotone_r monotone_def.
Qed.
End Meet.