Set Firstorder Depth 5.

Require Export PartialOrder.

Open Local Scope po_scope.

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).

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)).

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.

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.

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.

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.