Total Order

A total order is a lattice were x <= y or y <= x.

Record TotalOrder : Type :=
{ L :> Lattice
; le_total : forall x y:L, {x <= y}+{y <= x}
}.

Section MinMax.

Variable X : TotalOrder.

meet x y is either x or y.

Definition meet_irred : forall x y : X, {meet x y == x} + {meet x y == y}.
Defined.

Section Monotone.

Variable f : X -> X.
Hypothesis Hf : monotone X f.

Add Morphism f with signature (@st_eq X) ==> (@st_eq X) as monotone_compat.
Qed.

meet distributes over any monotone function.

Lemma monotone_meet_distr : forall x y : X, f (meet x y) == meet (f x) (f y).

End Monotone.

join distributes over meet

Lemma join_meet_distr_r : forall x y z:X, (join x (meet y z))==(meet (join x y) (join x z)).

Lemma join_meet_distr_l : forall x y z:X, (join (meet y z) x)==(meet (join y x) (join z x)).

Section Antitone.

Variable f : X -> X.
Hypothesis Hf : antitone X f.

Lemma antitone_meet_join_distr : forall x y : X, f (meet x y) == join (f x) (f y).

End Antitone.

Lemmas of distributive lattices

Lemma join_meet_modular_r : forall x y z : X, join x (meet y (join x z)) == meet (join x y) (join x z).

Lemma join_meet_modular_l : forall x y z : X, join (meet (join x z) y) z == meet (join x z) (join y z).

Lemma meet_join_disassoc : forall x y z : X, meet (join x y) z <= join x (meet y z).

End MinMax.

Section MaxMin.

Variable X : TotalOrder.

Dual Total Order

The dual of a total order is a total order.

Definition Dual : TotalOrder.
Defined.

The duals of the previous lemmas hold.

Definition join_irred : forall x y : X, {join x y == x} + {join x y == y} :=
meet_irred Dual.

Lemma monotone_join_distr : forall f, monotone X f -> forall x y : X, f (join x y) == join (f x) (f y).

Lemma meet_join_distr_r : forall x y z:X, (meet x (join y z))==(join (meet x y) (meet x z)).

Lemma meet_join_distr_l : forall x y z:X, (meet (join y z) x)==(join (meet y x) (meet z x)).

Lemma antitone_join_meet_distr : forall f, antitone X f -> forall x y : X, f (join x y) == meet (f x) (f y).

Lemma meet_join_modular_r : forall x y z : X, meet x (join y (meet x z)) == join (meet x y) (meet x z).

Lemma meet_join_modular_l : forall x y z : X, meet (join (meet x z) y) z == join (meet x z) (meet y z).

End MaxMin.

Section TotalOrderMinDef.

Variable X : PartialOrder.

Given a total order, meet and join can be characterized in terms of the order.

Variable min : X -> X -> X.
Hypothesis le_total : forall x y:X, {x <= y}+{y <= x}.
Hypothesis min_def1 : forall x y:X, x <= y -> min x y == x.
Hypothesis min_def2 : forall x y:X, y <= x -> min x y == y.

Lemma min_lb_l : forall x y:X, min x y <= x.

Lemma min_lb_r : forall x y:X, min x y <= y.

Lemma min_glb : forall x y z, z <= x -> z <= y -> z <= min x y.

End TotalOrderMinDef.

With a total order has a new characterization.

Definition makeTotalOrder :
forall (A : Type) (equiv : A -> A -> Prop) (le : A -> A -> Prop)
  (monotone antitone : (A -> A) -> Prop)
  (meet join : A -> A -> A),
  (forall x y : A, equiv x y <-> (le x y /\ le y x)) ->
  (forall x : A, le x x) ->
  (forall x y z : A, le x y -> le y z -> le x z) ->
  (forall x y : A, {le x y} + {le y x}) ->
  (forall f, monotone f <-> (forall x y, le x y -> le (f x) (f y))) ->
  (forall f, antitone f <-> (forall x y, le x y -> le (f y) (f x))) ->
  (forall x y : A, le x y -> equiv (meet x y) x) ->
  (forall x y : A, le y x -> equiv (meet x y) y) ->
  (forall x y : A, le y x -> equiv (join x y) x) ->
  (forall x y : A, le x y -> equiv (join x y) y) ->
  TotalOrder.
Defined.

Module Default.

Default meet and join.

Section MinDefault.
Variable A : Type.
Variable equiv: A -> A -> Prop.
Variable le : A -> A -> Prop.
Hypothesis equiv_le_def : forall x y : A, equiv x y <-> (le x y /\ le y x).
Hypothesis le_total : forall x y:A, {le x y}+{le y x}.

Given a total order, meet and join have a default implemenation.

Definition min (x y:A) :=
if (le_total x y) then x else y.

Definition min_case x y (P:A -> Type) (Hx : le x y -> P x) (Hy : le y x -> P y) : P (min x y) :=
match (le_total x y) as s return P (if s then x else y) with
| left p => Hx p
| right p => Hy p
end.

Lemma min_def1 : forall x y, le x y -> equiv (min x y) x.

Lemma min_def2 : forall x y, le y x -> equiv (min x y) y.

End MinDefault.

Section MaxDefault.
Variable A : Type.
Variable equiv: A -> A -> Prop.
Variable le : A -> A -> Prop.
Hypothesis equiv_le_def : forall x y : A, equiv x y <-> (le x y /\ le y x).
Hypothesis le_total : forall x y:A, {le x y}+{le y x}.

Definition max (x y:A) :=
if le_total y x then x else y.

Let flip_le x y := le y x.
Let flip_le_total x y := le_total y x.

Definition max_case :
forall x y (P : A -> Type), (le y x -> P x) -> (le x y -> P y) -> P (max x y) :=
min_case A flip_le flip_le_total.

Lemma max_def1 : forall x y, le y x -> equiv (max x y) x.

Lemma max_def2 : forall x y, le x y -> equiv (max x y) y.

End MaxDefault.

End Default.