CoRN.order.TotalOrder
Record TotalOrder : Type :=
{ L :> Lattice
; le_total : ∀ x y:L, {x ≤ y}+{y ≤ x}
}.
Section MinMax.
Variable X : TotalOrder.
{ L :> Lattice
; le_total : ∀ x y:L, {x ≤ y}+{y ≤ x}
}.
Section MinMax.
Variable X : TotalOrder.
meet x y is either x or y.
Definition meet_irred : ∀ x y : X, {meet x y == x} + {meet x y == y}.
Proof.
intros.
destruct (le_total _ x y) as [H|H].
left.
firstorder using le_meet_l.
right.
firstorder using le_meet_r.
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.
Proof.
revert Hf;rewrite → monotone_def;intros.
revert H0; do 2 rewrite → equiv_le_def.
firstorder.
Qed.
Proof.
intros.
destruct (le_total _ x y) as [H|H].
left.
firstorder using le_meet_l.
right.
firstorder using le_meet_r.
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.
Proof.
revert Hf;rewrite → monotone_def;intros.
revert H0; do 2 rewrite → equiv_le_def.
firstorder.
Qed.
meet distributes over any monotone function.
Lemma monotone_meet_distr : ∀ x y : X, f (meet x y) == meet (f x) (f y).
Proof.
revert Hf; rewrite → monotone_def. intro Hf.
assert (∀ x y : X, x ≤ y → f (meet x y) == meet (f x) (f y)).
intros x y Hxy.
assert (Hfxfy:=Hf _ _ Hxy).
rewrite → le_meet_l in Hxy.
rewrite → Hxy.
rewrite → le_meet_l in Hfxfy.
rewrite → Hfxfy.
reflexivity.
intros.
destruct (le_total _ x y).
auto.
rewrite → (meet_comm X).
rewrite → (meet_comm _ (f x)).
auto.
Qed.
End Monotone.
Proof.
revert Hf; rewrite → monotone_def. intro Hf.
assert (∀ x y : X, x ≤ y → f (meet x y) == meet (f x) (f y)).
intros x y Hxy.
assert (Hfxfy:=Hf _ _ Hxy).
rewrite → le_meet_l in Hxy.
rewrite → Hxy.
rewrite → le_meet_l in Hfxfy.
rewrite → Hfxfy.
reflexivity.
intros.
destruct (le_total _ x y).
auto.
rewrite → (meet_comm X).
rewrite → (meet_comm _ (f x)).
auto.
Qed.
End Monotone.
join distributes over meet
Lemma join_meet_distr_r : ∀ x y z:X, (join x (meet y z))==(meet (join x y) (join x z)).
Proof (fun a ⇒ monotone_meet_distr _ (join_monotone_r X a)).
Lemma join_meet_distr_l : ∀ x y z:X, (join (meet y z) x)==(meet (join y x) (join z x)).
Proof (fun a ⇒ monotone_meet_distr _ (join_monotone_l X a)).
Section Antitone.
Variable f : X → X.
Hypothesis Hf : antitone X f.
Lemma antitone_meet_join_distr : ∀ x y : X, f (meet x y) == join (f x) (f y).
Proof.
revert Hf;rewrite → antitone_def; intro Hf.
assert (∀ x y : X, x ≤ y → f (meet x y) == join (f x) (f y)).
intros x y Hxy.
assert (Hfxfy:=Hf _ _ Hxy).
rewrite → le_meet_l in Hxy.
rewrite → Hxy.
rewrite → le_join_l in Hfxfy.
rewrite → Hfxfy.
reflexivity.
intros.
destruct (le_total _ x y).
auto.
rewrite → (meet_comm X).
rewrite → (join_comm X).
auto.
Qed.
End Antitone.
Proof (fun a ⇒ monotone_meet_distr _ (join_monotone_r X a)).
Lemma join_meet_distr_l : ∀ x y z:X, (join (meet y z) x)==(meet (join y x) (join z x)).
Proof (fun a ⇒ monotone_meet_distr _ (join_monotone_l X a)).
Section Antitone.
Variable f : X → X.
Hypothesis Hf : antitone X f.
Lemma antitone_meet_join_distr : ∀ x y : X, f (meet x y) == join (f x) (f y).
Proof.
revert Hf;rewrite → antitone_def; intro Hf.
assert (∀ x y : X, x ≤ y → f (meet x y) == join (f x) (f y)).
intros x y Hxy.
assert (Hfxfy:=Hf _ _ Hxy).
rewrite → le_meet_l in Hxy.
rewrite → Hxy.
rewrite → le_join_l in Hfxfy.
rewrite → Hfxfy.
reflexivity.
intros.
destruct (le_total _ x y).
auto.
rewrite → (meet_comm X).
rewrite → (join_comm X).
auto.
Qed.
End Antitone.
Lemmas of distributive lattices
Lemma join_meet_modular_r : ∀ x y z : X, join x (meet y (join x z)) == meet (join x y) (join x z).
Proof.
intros.
rewrite → join_meet_distr_r.
rewrite → (join_assoc X).
rewrite → (join_idem X).
reflexivity.
Qed.
Lemma join_meet_modular_l : ∀ x y z : X, join (meet (join x z) y) z == meet (join x z) (join y z).
Proof.
intros.
rewrite → (join_comm X (meet (join x z) y) z).
rewrite → (meet_comm X (join x z) y).
rewrite → (meet_comm X (join x z) (join y z)).
rewrite → (join_comm X x z).
rewrite → (join_comm X y z).
apply join_meet_modular_r.
Qed.
Lemma meet_join_disassoc : ∀ x y z : X, meet (join x y) z ≤ join x (meet y z).
Proof.
intros.
rewrite → join_meet_distr_r.
apply meet_le_compat.
apply le_refl.
apply join_ub_r.
Qed.
End MinMax.
Section MaxMin.
Variable X : TotalOrder.
Proof.
intros.
rewrite → join_meet_distr_r.
rewrite → (join_assoc X).
rewrite → (join_idem X).
reflexivity.
Qed.
Lemma join_meet_modular_l : ∀ x y z : X, join (meet (join x z) y) z == meet (join x z) (join y z).
Proof.
intros.
rewrite → (join_comm X (meet (join x z) y) z).
rewrite → (meet_comm X (join x z) y).
rewrite → (meet_comm X (join x z) (join y z)).
rewrite → (join_comm X x z).
rewrite → (join_comm X y z).
apply join_meet_modular_r.
Qed.
Lemma meet_join_disassoc : ∀ x y z : X, meet (join x y) z ≤ join x (meet y z).
Proof.
intros.
rewrite → join_meet_distr_r.
apply meet_le_compat.
apply le_refl.
apply join_ub_r.
Qed.
End MinMax.
Section MaxMin.
Variable X : TotalOrder.
Definition Dual : TotalOrder.
eapply Build_TotalOrder with (L:= Dual X).
Proof.
intros.
destruct (le_total _ x y); auto.
Defined.
eapply Build_TotalOrder with (L:= Dual X).
Proof.
intros.
destruct (le_total _ x y); auto.
Defined.
The duals of the previous lemmas hold.
Definition join_irred : ∀ x y : X, {join x y == x} + {join x y == y} :=
meet_irred Dual.
Lemma monotone_join_distr : ∀ f, monotone X f → ∀ x y : X, f (join x y) == join (f x) (f y).
Proof monotone_meet_distr Dual.
Lemma meet_join_distr_r : ∀ x y z:X, (meet x (join y z))==(join (meet x y) (meet x z)).
Proof join_meet_distr_r Dual.
Lemma meet_join_distr_l : ∀ x y z:X, (meet (join y z) x)==(join (meet y x) (meet z x)).
Proof join_meet_distr_l Dual.
Lemma antitone_join_meet_distr : ∀ f, antitone X f → ∀ x y : X, f (join x y) == meet (f x) (f y).
Proof antitone_meet_join_distr Dual.
Lemma meet_join_modular_r : ∀ x y z : X, meet x (join y (meet x z)) == join (meet x y) (meet x z).
Proof join_meet_modular_r Dual.
Lemma meet_join_modular_l : ∀ x y z : X, meet (join (meet x z) y) z == join (meet x z) (meet y z).
Proof join_meet_modular_l Dual.
End MaxMin.
Section TotalOrderMinDef.
Variable X : PartialOrder.
meet_irred Dual.
Lemma monotone_join_distr : ∀ f, monotone X f → ∀ x y : X, f (join x y) == join (f x) (f y).
Proof monotone_meet_distr Dual.
Lemma meet_join_distr_r : ∀ x y z:X, (meet x (join y z))==(join (meet x y) (meet x z)).
Proof join_meet_distr_r Dual.
Lemma meet_join_distr_l : ∀ x y z:X, (meet (join y z) x)==(join (meet y x) (meet z x)).
Proof join_meet_distr_l Dual.
Lemma antitone_join_meet_distr : ∀ f, antitone X f → ∀ x y : X, f (join x y) == meet (f x) (f y).
Proof antitone_meet_join_distr Dual.
Lemma meet_join_modular_r : ∀ x y z : X, meet x (join y (meet x z)) == join (meet x y) (meet x z).
Proof join_meet_modular_r Dual.
Lemma meet_join_modular_l : ∀ x y z : X, meet (join (meet x z) y) z == join (meet x z) (meet y z).
Proof join_meet_modular_l Dual.
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 : ∀ x y:X, {x ≤ y}+{y ≤ x}.
Hypothesis min_def1 : ∀ x y:X, x ≤ y → min x y == x.
Hypothesis min_def2 : ∀ x y:X, y ≤ x → min x y == y.
Lemma min_lb_l : ∀ x y:X, min x y ≤ x.
Proof.
intros.
destruct (le_total x y).
rewrite → min_def1; auto.
apply le_refl.
rewrite → min_def2; auto.
Qed.
Lemma min_lb_r : ∀ x y:X, min x y ≤ y.
Proof.
intros.
destruct (le_total x y).
rewrite → min_def1; auto.
rewrite → min_def2; auto.
apply le_refl.
Qed.
Lemma min_glb : ∀ x y z, z ≤ x → z ≤ y → z ≤ min x y.
Proof.
intros.
destruct (le_total x y).
rewrite → min_def1; assumption.
rewrite → min_def2; assumption.
Qed.
End TotalOrderMinDef.
Hypothesis le_total : ∀ x y:X, {x ≤ y}+{y ≤ x}.
Hypothesis min_def1 : ∀ x y:X, x ≤ y → min x y == x.
Hypothesis min_def2 : ∀ x y:X, y ≤ x → min x y == y.
Lemma min_lb_l : ∀ x y:X, min x y ≤ x.
Proof.
intros.
destruct (le_total x y).
rewrite → min_def1; auto.
apply le_refl.
rewrite → min_def2; auto.
Qed.
Lemma min_lb_r : ∀ x y:X, min x y ≤ y.
Proof.
intros.
destruct (le_total x y).
rewrite → min_def1; auto.
rewrite → min_def2; auto.
apply le_refl.
Qed.
Lemma min_glb : ∀ x y z, z ≤ x → z ≤ y → z ≤ min x y.
Proof.
intros.
destruct (le_total x y).
rewrite → min_def1; assumption.
rewrite → min_def2; assumption.
Qed.
End TotalOrderMinDef.
With a total order has a new characterization.
Definition makeTotalOrder :
∀ (A : Type) (equiv : A → A → Prop) (le : A → A → Prop)
(monotone antitone : (A → A) → Prop)
(meet join : A → A → A),
(∀ x y : A, equiv x y ↔ (le x y ∧ le y x)) →
(∀ x : A, le x x) →
(∀ x y z : A, le x y → le y z → le x z) →
(∀ x y : A, {le x y} + {le y x}) →
(∀ f, monotone f ↔ (∀ x y, le x y → le (f x) (f y))) →
(∀ f, antitone f ↔ (∀ x y, le x y → le (f y) (f x))) →
(∀ x y : A, le x y → equiv (meet x y) x) →
(∀ x y : A, le y x → equiv (meet x y) y) →
(∀ x y : A, le y x → equiv (join x y) x) →
(∀ x y : A, le x y → equiv (join x y) y) →
TotalOrder.
Proof.
intros A0 eq0 le0 monotone0 antitone0 min max eq0_def refl trans total monotone0_def antitone0_def min_def1 min_def2 max_def1 max_def2.
pose (PO:=makePartialOrder eq0 le0 monotone0 antitone0 eq0_def refl trans monotone0_def antitone0_def).
pose (DPO := (PartialOrder.Dual PO)).
pose (flip_total := fun x y ⇒ total y x).
pose (L0:=makeLattice PO min max (min_lb_l PO min total min_def1 min_def2)
(min_lb_r PO min total min_def1 min_def2) (min_glb PO min total min_def1 min_def2)
(min_lb_l DPO max flip_total max_def1 max_def2) (min_lb_r DPO max flip_total max_def1 max_def2)
(min_glb DPO max flip_total max_def1 max_def2)).
exact (Build_TotalOrder L0 total).
Defined.
Module Default.
∀ (A : Type) (equiv : A → A → Prop) (le : A → A → Prop)
(monotone antitone : (A → A) → Prop)
(meet join : A → A → A),
(∀ x y : A, equiv x y ↔ (le x y ∧ le y x)) →
(∀ x : A, le x x) →
(∀ x y z : A, le x y → le y z → le x z) →
(∀ x y : A, {le x y} + {le y x}) →
(∀ f, monotone f ↔ (∀ x y, le x y → le (f x) (f y))) →
(∀ f, antitone f ↔ (∀ x y, le x y → le (f y) (f x))) →
(∀ x y : A, le x y → equiv (meet x y) x) →
(∀ x y : A, le y x → equiv (meet x y) y) →
(∀ x y : A, le y x → equiv (join x y) x) →
(∀ x y : A, le x y → equiv (join x y) y) →
TotalOrder.
Proof.
intros A0 eq0 le0 monotone0 antitone0 min max eq0_def refl trans total monotone0_def antitone0_def min_def1 min_def2 max_def1 max_def2.
pose (PO:=makePartialOrder eq0 le0 monotone0 antitone0 eq0_def refl trans monotone0_def antitone0_def).
pose (DPO := (PartialOrder.Dual PO)).
pose (flip_total := fun x y ⇒ total y x).
pose (L0:=makeLattice PO min max (min_lb_l PO min total min_def1 min_def2)
(min_lb_r PO min total min_def1 min_def2) (min_glb PO min total min_def1 min_def2)
(min_lb_l DPO max flip_total max_def1 max_def2) (min_lb_r DPO max flip_total max_def1 max_def2)
(min_glb DPO max flip_total max_def1 max_def2)).
exact (Build_TotalOrder L0 total).
Defined.
Module Default.
Section MinDefault.
Variable A : Type.
Variable equiv: A → A → Prop.
Variable le : A → A → Prop.
Hypothesis equiv_le_def : ∀ x y : A, equiv x y ↔ (le x y ∧ le y x).
Hypothesis le_total : ∀ x y:A, {le x y}+{le y x}.
Variable A : Type.
Variable equiv: A → A → Prop.
Variable le : A → A → Prop.
Hypothesis equiv_le_def : ∀ x y : A, equiv x y ↔ (le x y ∧ le y x).
Hypothesis le_total : ∀ 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 : ∀ x y, le x y → equiv (min x y) x.
Proof.
intros.
apply min_case; firstorder.
Qed.
Lemma min_def2 : ∀ x y, le y x → equiv (min x y) y.
Proof.
intros.
apply min_case; firstorder.
Qed.
End MinDefault.
Section MaxDefault.
Variable A : Type.
Variable equiv: A → A → Prop.
Variable le : A → A → Prop.
Hypothesis equiv_le_def : ∀ x y : A, equiv x y ↔ (le x y ∧ le y x).
Hypothesis le_total : ∀ 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 :
∀ 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 : ∀ x y, le y x → equiv (max x y) x.
Proof.
refine (min_def1 A equiv flip_le _ flip_le_total).
firstorder.
Qed.
Lemma max_def2 : ∀ x y, le x y → equiv (max x y) y.
Proof.
refine (min_def2 A equiv flip_le _ flip_le_total).
firstorder.
Qed.
End MaxDefault.
End Default.
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 : ∀ x y, le x y → equiv (min x y) x.
Proof.
intros.
apply min_case; firstorder.
Qed.
Lemma min_def2 : ∀ x y, le y x → equiv (min x y) y.
Proof.
intros.
apply min_case; firstorder.
Qed.
End MinDefault.
Section MaxDefault.
Variable A : Type.
Variable equiv: A → A → Prop.
Variable le : A → A → Prop.
Hypothesis equiv_le_def : ∀ x y : A, equiv x y ↔ (le x y ∧ le y x).
Hypothesis le_total : ∀ 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 :
∀ 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 : ∀ x y, le y x → equiv (max x y) x.
Proof.
refine (min_def1 A equiv flip_le _ flip_le_total).
firstorder.
Qed.
Lemma max_def2 : ∀ x y, le x y → equiv (max x y) y.
Proof.
refine (min_def2 A equiv flip_le _ flip_le_total).
firstorder.
Qed.
End MaxDefault.
End Default.