CoRN.model.totalorder.QposMinMax
Definition Qpos_le_total (x y : Qpos) : {x ≤ y} + {y ≤ x} :=
match Qlt_le_dec_fast x y with
| left p ⇒ left _ (Qlt_le_weak _ _ p)
| right p ⇒ right _ p
end.
Lemma Qpos_eq_le_def : ∀ (x y: Qpos), x == y ↔ x ≤ y ∧ y ≤ x.
Proof.
intros.
split.
intros H; rewrite → H.
firstorder using Qle_refl.
firstorder using Qle_antisym.
Qed.
Definition Qpos_monotone : (Qpos → Qpos) → Prop := Default.monotone (fun (x y:Qpos) ⇒ x ≤ y).
Definition Qpos_antitone : (Qpos → Qpos) → Prop := Default.antitone (fun (x y:Qpos) ⇒ x ≤ y).
Definition Qpos_min : Qpos → Qpos → Qpos := Default.min _ _ Qpos_le_total.
Definition Qpos_max : Qpos → Qpos → Qpos := Default.max _ _ Qpos_le_total.
Definition Qpos_min_case :
∀ (x y:Qpos) (P : Qpos → Type), (x ≤ y → P x) → (y ≤ x → P y) → P (Qpos_min x y) :=
Default.min_case _ _ Qpos_le_total.
Definition Qpos_max_case :
∀ (x y:Qpos) (P : Qpos → Type), (y ≤ x → P x) → (x ≤ y → P y) → P (Qpos_max x y) :=
Default.max_case _ _ Qpos_le_total.
Definition QposTotalOrder : TotalOrder.
Proof.
apply makeTotalOrder with
Qpos QposEq (fun (x y:Qpos) ⇒ x ≤ y) Qpos_monotone Qpos_antitone Qpos_min Qpos_max.
exact Qpos_eq_le_def.
exact Qle_refl.
exact Qle_trans.
exact Qpos_le_total.
firstorder using PartialOrder.Default.monotone_def.
firstorder using PartialOrder.Default.antitone_def.
apply (TotalOrder.Default.min_def1 _ _ _ Qpos_eq_le_def Qpos_le_total).
apply (TotalOrder.Default.min_def2 _ _ _ Qpos_eq_le_def Qpos_le_total).
apply (TotalOrder.Default.max_def1 _ _ _ Qpos_eq_le_def Qpos_le_total).
apply (TotalOrder.Default.max_def2 _ _ _ Qpos_eq_le_def Qpos_le_total).
Defined.
Section QTotalOrder.
Let Qto := QposTotalOrder.
Definition Qpos_min_lb_l : ∀ x y : Qpos, Qpos_min x y ≤ x := @meet_lb_l Qto.
Definition Qpos_min_lb_r : ∀ x y : Qpos, Qpos_min x y ≤ y := @meet_lb_r Qto.
Definition Qpos_min_glb : ∀ x y z : Qpos, z ≤ x → z ≤ y → z ≤ (Qpos_min x y) :=
@meet_glb Qto.
Definition Qpos_min_comm : ∀ x y : Qpos, Qpos_min x y == Qpos_min y x := @meet_comm Qto.
Definition Qpos_min_assoc : ∀ x y z : Qpos, Qpos_min x (Qpos_min y z) == Qpos_min (Qpos_min x y) z:=
@meet_assoc Qto.
Definition Qpos_min_idem : ∀ x : Qpos, Qpos_min x x == x := @meet_idem Qto.
Definition Qpos_le_min_l : ∀ x y : Qpos, x ≤ y ↔ Qpos_min x y == x := @le_meet_l Qto.
Definition Qpos_le_min_r : ∀ x y : Qpos, y ≤ x ↔ Qpos_min x y == y := @le_meet_r Qto.
Definition Qpos_min_irred : ∀ x y: Qpos, {Qpos_min x y == x} + {Qpos_min x y == y} := @meet_irred Qto.
Definition Qpos_min_monotone_r : ∀ a : Qpos, Qpos_monotone (Qpos_min a) :=
@meet_monotone_r Qto.
Definition Qpos_min_monotone_l : ∀ a : Qpos, Qpos_monotone (fun x ⇒ Qpos_min x a) :=
@meet_monotone_l Qto.
Definition Qpos_min_le_compat :
∀ w x y z : Qpos, w ≤ y → x ≤ z → Qpos_min w x ≤ Qpos_min y z :=
@meet_le_compat Qto.
Definition Qpos_max_ub_l : ∀ x y : Qpos, x ≤ Qpos_max x y := @join_ub_l Qto.
Definition Qpos_max_ub_r : ∀ x y : Qpos, y ≤ Qpos_max x y := @join_ub_r Qto.
Definition Qpos_max_glb : ∀ x y z : Qpos, x ≤ z → y ≤ z → (Qpos_max x y) ≤ z :=
@join_lub Qto.
Definition Qpos_max_comm : ∀ x y : Qpos, Qpos_max x y == Qpos_max y x := @join_comm Qto.
Definition Qpos_max_assoc : ∀ x y z : Qpos, Qpos_max x (Qpos_max y z) == Qpos_max (Qpos_max x y) z:=
@join_assoc Qto.
Definition Qpos_max_idem : ∀ x : Qpos, Qpos_max x x == x := @join_idem Qto.
Definition Qpos_le_max_l : ∀ x y : Qpos, y ≤ x ↔ Qpos_max x y == x := @le_join_l Qto.
Definition Qpos_le_max_r : ∀ x y : Qpos, x ≤ y ↔ Qpos_max x y == y := @le_join_r Qto.
Definition Qpos_max_irred : ∀ x y: Qpos, {Qpos_max x y == x} + {Qpos_max x y == y} := @join_irred Qto.
Definition Qpos_max_monotone_r : ∀ a : Qpos, Qpos_monotone (Qpos_max a) :=
@join_monotone_r Qto.
Definition Qpos_max_monotone_l : ∀ a : Qpos, Qpos_monotone (fun x ⇒ Qpos_max x a) :=
@join_monotone_l Qto.
Definition Qpos_max_le_compat :
∀ w x y z : Qpos, w≤y → x≤z → Qpos_max w x ≤ Qpos_max y z :=
@join_le_compat Qto.
Definition Qpos_min_max_absorb_l_l : ∀ x y : Qpos, Qpos_min x (Qpos_max x y) == x :=
@meet_join_absorb_l_l Qto.
Definition Qpos_max_min_absorb_l_l : ∀ x y : Qpos, Qpos_max x (Qpos_min x y) == x :=
@join_meet_absorb_l_l Qto.
Definition Qpos_min_max_absorb_l_r : ∀ x y : Qpos, Qpos_min x (Qpos_max y x) == x :=
@meet_join_absorb_l_r Qto.
Definition Qpos_max_min_absorb_l_r : ∀ x y : Qpos, Qpos_max x (Qpos_min y x) == x :=
@join_meet_absorb_l_r Qto.
Definition Qpos_min_max_absorb_r_l : ∀ x y : Qpos, Qpos_min (Qpos_max x y) x == x :=
@meet_join_absorb_r_l Qto.
Definition Qpos_max_min_absorb_r_l : ∀ x y : Qpos, Qpos_max (Qpos_min x y) x == x :=
@join_meet_absorb_r_l Qto.
Definition Qpos_min_max_absorb_r_r : ∀ x y : Qpos, Qpos_min (Qpos_max y x) x == x :=
@meet_join_absorb_r_r Qto.
Definition Qpos_max_min_absorb_r_r : ∀ x y : Qpos, Qpos_max (Qpos_min y x) x == x :=
@join_meet_absorb_r_r Qto.
Definition Qpos_min_max_eq : ∀ x y : Qpos, Qpos_min x y == Qpos_max x y → x == y :=
@meet_join_eq Qto.
Definition Qpos_max_min_distr_r : ∀ x y z : Qpos,
Qpos_max x (Qpos_min y z) == Qpos_min (Qpos_max x y) (Qpos_max x z) :=
@join_meet_distr_r Qto.
Definition Qpos_max_min_distr_l : ∀ x y z : Qpos,
Qpos_max (Qpos_min y z) x == Qpos_min (Qpos_max y x) (Qpos_max z x) :=
@join_meet_distr_l Qto.
Definition Qpos_min_max_distr_r : ∀ x y z : Qpos,
Qpos_min x (Qpos_max y z) == Qpos_max (Qpos_min x y) (Qpos_min x z) :=
@meet_join_distr_r Qto.
Definition Qpos_min_max_distr_l : ∀ x y z : Qpos,
Qpos_min (Qpos_max y z) x == Qpos_max (Qpos_min y x) (Qpos_min z x) :=
@meet_join_distr_l Qto.
Definition Qpos_max_min_modular_r : ∀ x y z : Qpos,
Qpos_max x (Qpos_min y (Qpos_max x z)) == Qpos_min (Qpos_max x y) (Qpos_max x z) :=
@join_meet_modular_r Qto.
Definition Qpos_max_min_modular_l : ∀ x y z : Qpos,
Qpos_max (Qpos_min (Qpos_max x z) y) z == Qpos_min (Qpos_max x z) (Qpos_max y z) :=
@join_meet_modular_l Qto.
Definition Qpos_min_max_modular_r : ∀ x y z : Qpos,
Qpos_min x (Qpos_max y (Qpos_min x z)) == Qpos_max (Qpos_min x y) (Qpos_min x z) :=
@meet_join_modular_r Qto.
Definition Qpos_min_max_modular_l : ∀ x y z : Qpos,
Qpos_min (Qpos_max (Qpos_min x z) y) z == Qpos_max (Qpos_min x z) (Qpos_min y z) :=
@meet_join_modular_l Qto.
Definition Qpos_min_max_disassoc : ∀ x y z : Qpos, Qpos_min (Qpos_max x y) z ≤ Qpos_max x (Qpos_min y z) :=
@meet_join_disassoc Qto.
Lemma Qplus_monotone_r : ∀ a, Qpos_monotone (Qpos_plus a).
Proof.
intros a x y Hxy.
repeat rewrite → Q_Qpos_plus.
apply Qplus_le_compat. apply Qle_refl. assumption.
Qed.
Lemma Qplus_monotone_l : ∀ a, Qpos_monotone (fun x ⇒ Qpos_plus x a).
Proof.
intros a x y Hxy.
repeat rewrite Q_Qpos_plus.
apply Qplus_le_compat. assumption. apply Qle_refl.
Qed.
Open Local Scope Qpos_scope.
Definition Qpos_min_plus_distr_r : (∀ x y z : Qpos, Qpos_plus x (Qpos_min y z) == Qpos_min (Qpos_plus x y) (Qpos_plus x z)) :=
fun a ⇒ @monotone_meet_distr Qto _ (Qplus_monotone_r a).
Definition Qpos_min_plus_distr_l : ∀ x y z : Qpos, Qpos_plus (Qpos_min y z) x == Qpos_min (Qpos_plus y x) (Qpos_plus z x) :=
fun a ⇒ @monotone_meet_distr Qto _ (Qplus_monotone_l a).
Definition Qpos_max_plus_distr_r : ∀ x y z : Qpos, Qpos_plus x (Qpos_max y z) == Qpos_max (Qpos_plus x y) (Qpos_plus x z) :=
fun a ⇒ @monotone_join_distr Qto _ (Qplus_monotone_r a).
Definition Qpos_max_plus_distr_l : ∀ x y z : Qpos, Qpos_plus (Qpos_max y z) x == Qpos_max (Qpos_plus y x) (Qpos_plus z x) :=
fun a ⇒ @monotone_join_distr Qto _ (Qplus_monotone_l a).
End QTotalOrder.
Lemma Q_Qpos_min : ∀ (x y:Qpos), ((Qpos_min x y)%Qpos:Q)==Qmin (x:Q) (y:Q).
Proof.
intros x y.
unfold Qpos_min.
unfold Qmin.
unfold Default.min.
destruct (Qpos_le_total x y) as [H|H]; destruct (Qle_total x y) as [H0|H0]; try reflexivity;
apply Qle_antisym; auto.
Qed.
Lemma Q_Qpos_max : ∀ (x y:Qpos), ((Qpos_max x y)%Qpos:Q)==Qmax (x:Q) (y:Q).
Proof.
intros x y.
unfold Qpos_max.
unfold Qmax.
unfold Default.max.
destruct (Qpos_le_total y x) as [H|H]; destruct (Qle_total y x) as [H0|H0]; try reflexivity;
apply Qle_antisym; auto.
Qed.
Lemma Qpos_min_mult_distr_r : ∀ x y z : Qpos, Qpos_mult x (Qpos_min y z) == Qpos_min (Qpos_mult x y) (Qpos_mult x z).
Proof. intros x y z. autorewrite with QposElim. apply Qmin_mult_pos_distr_r. auto. Qed.
Lemma Qpos_min_mult_distr_l : ∀ x y z : Qpos, Qpos_mult (Qpos_min y z) x == Qpos_min (Qpos_mult y x) (Qpos_mult z x).
Proof. intros x y z. autorewrite with QposElim. apply Qmin_mult_pos_distr_l. auto. Qed.
Lemma Qpos_max_mult_distr_r : ∀ x y z : Qpos, Qpos_mult x (Qpos_max y z) == Qpos_max (Qpos_mult x y) (Qpos_mult x z).
Proof. intros x y z. autorewrite with QposElim. apply Qmax_mult_pos_distr_r. auto. Qed.
Lemma Qpos_max_mult_distr_l : ∀ x y z : Qpos, Qpos_mult (Qpos_max y z) x == Qpos_max (Qpos_mult y x) (Qpos_mult z x).
Proof. intros x y z. autorewrite with QposElim. apply Qmax_mult_pos_distr_l. auto. Qed.