CoRN.model.lattice.CRlattice

Require Export CRpartialorder.
Require Import Lattice.

Definition CRLattice : Lattice :=
makeLattice CRPartialOrder (ucFun2 CRmin) (ucFun2 CRmax)
 CRmin_lb_l CRmin_lb_r CRmin_glb CRmax_ub_l CRmax_ub_r CRmax_lub.

Section CRLattice.

Let CRlat := CRLattice.

Open Local Scope CR_scope.

Definition CRmin_comm : ∀ x y : CR, CRmin x y == CRmin y x := @meet_comm CRlat.
Definition CRmin_assoc : ∀ x y z : CR, CRmin x (CRmin y z) == CRmin (CRmin x y) z:=
 @meet_assoc CRlat.
Definition CRmin_idem : ∀ x : CR, CRmin x x == x := @meet_idem CRlat.
Definition CRle_min_l : ∀ x y : CR, x ≤ y ↔ CRmin x y == x := @le_meet_l CRlat.
Definition CRle_min_r : ∀ x y : CR, y ≤ x ↔ CRmin x y == y := @le_meet_r CRlat.
Definition CRmin_monotone_r : ∀ a : CR, CRmonotone (CRmin a) :=
 @meet_monotone_r CRlat.
Definition CRmin_monotone_l : ∀ a : CR, CRmonotone (fun x ⇒ CRmin x a) :=
 @meet_monotone_l CRlat.
Definition CRmin_le_compat :
 ∀ w x y z : CR, w ≤ y → x ≤ z → CRmin w x ≤ CRmin y z :=
 @meet_le_compat CRlat.

Definition CRmax_comm : ∀ x y : CR, CRmax x y == CRmax y x := @join_comm CRlat.
Definition CRmax_assoc : ∀ x y z : CR, CRmax x (CRmax y z) == CRmax (CRmax x y) z:=
 @join_assoc CRlat.
Definition CRmax_idem : ∀ x : CR, CRmax x x == x := @join_idem CRlat.
Definition CRle_max_l : ∀ x y : CR, y ≤ x ↔ CRmax x y == x := @le_join_l CRlat.
Definition CRle_max_r : ∀ x y : CR, x ≤ y ↔ CRmax x y == y := @le_join_r CRlat.
Definition CRmax_monotone_r : ∀ a : CR, CRmonotone (CRmax a) :=
 @join_monotone_r CRlat.
Definition CRmax_monotone_l : ∀ a : CR, CRmonotone (fun x ⇒ CRmax x a) :=
 @join_monotone_l CRlat.
Definition CRmax_le_compat :
 ∀ w x y z : CR, w≤y → x≤z → CRmax w x ≤ CRmax y z :=
 @join_le_compat CRlat.

Definition CRmin_max_absorb_l_l : ∀ x y : CR, CRmin x (CRmax x y) == x :=
 @meet_join_absorb_l_l CRlat.
Definition CRmax_min_absorb_l_l : ∀ x y : CR, CRmax x (CRmin x y) == x :=
 @join_meet_absorb_l_l CRlat.
Definition CRmin_max_absorb_l_r : ∀ x y : CR, CRmin x (CRmax y x) == x :=
 @meet_join_absorb_l_r CRlat.
Definition CRmax_min_absorb_l_r : ∀ x y : CR, CRmax x (CRmin y x) == x :=
 @join_meet_absorb_l_r CRlat.
Definition CRmin_max_absorb_r_l : ∀ x y : CR, CRmin (CRmax x y) x == x :=
 @meet_join_absorb_r_l CRlat.
Definition CRmax_min_absorb_r_l : ∀ x y : CR, CRmax (CRmin x y) x == x :=
 @join_meet_absorb_r_l CRlat.
Definition CRmin_max_absorb_r_r : ∀ x y : CR, CRmin (CRmax y x) x == x :=
 @meet_join_absorb_r_r CRlat.
Definition CRmax_min_absorb_r_r : ∀ x y : CR, CRmax (CRmin y x) x == x :=
 @join_meet_absorb_r_r CRlat.

Definition CRmin_max_eq : ∀ x y : CR, CRmin x y == CRmax x y → x == y :=
 @meet_join_eq CRlat.


End CRLattice.