Library Coqtail.Reals.Raxioms.Rcauchy_lemmas

Require Import QArith Qabs.

Open Local Scope Q_scope.

Add Parametric Relation : Q Qle
reflexivity proved by Qle_refl
transitivity proved by Qle_trans
as Qle_order.

Add Parametric Relation : Q Qlt
transitivity proved by Qlt_trans
as Qlt_order.

Instance subrelation_le_eq : subrelation Qeq Qle.
intros x y H.
rewrite H.
apply Qle_refl.
Qed.

Add Morphism Qplus with signature Qlt ++> Qlt ++> Qlt as Qplus_lt_morphism.
intros a b H1 c d H2.
destruct a as [a₁ a₂]; destruct b as [b₁ b₂]; destruct c as [c₁ c₂]; destruct d as [d₁ d₂]; simpl.
unfold Qlt in ×.
simpl in ×.

replace ('(b₂ × d₂))%Z with ('b₂ × 'd₂)%Z; [|auto with zarith].
replace ('(a₂ × c₂))%Z with ('a₂ × 'c₂)%Z; [|auto with zarith].

replace ((a₁ × 'c₂ + c₁ × 'a₂) × ('b₂ × 'd₂))%Z with
((a₁ × 'b₂) × ('d₂ × 'c₂) + (c₁ × 'd₂) × ('a₂ × 'b₂))%Z; [|ring].
replace ((b₁ × 'd₂ + d₁ × 'b₂) × ('a₂ × 'c₂))%Z with
((b₁ × 'a₂) × ('d₂ × 'c₂) + (d₁ × 'c₂) × ('a₂ × 'b₂))%Z;[|ring].
apply Zplus_le_lt_compat.
apply Zmult_le_compat_r; auto with zarith.
apply Zmult_lt_compat_r; auto with zarith.
constructor.
Qed.

Add Morphism Qplus with signature Qle ++> Qle ++> Qle as Qplus_le_morphism.
intros; apply Qplus_le_compat; assumption.
Qed.

Definition Qeq_pos x y := 0 x x == y.

Definition Qle_pos x y := 0 x x y.

Instance Qle_pos_transitive : Transitive Qle_pos.
intros ? ? ? [? ?] [? ?]; split; auto.
eapply transitivity; eassumption.
Qed.

Instance subrelation_le_pos : subrelation Qle_pos Qle.
intros ? ? [? ?]; assumption.
Qed.

Instance Qeq_pos_transitive : Transitive Qeq_pos.
intros ? ? ? [? ?] [? ?]; split; auto.
eapply transitivity; eassumption.
Qed.

Instance subrelation_eq_pos : subrelation Qeq_pos Qeq.
intros ? ? [? ?]; assumption.
Qed.

Instance Qeq_pos_symmetric : Symmetric Qeq_pos.
intros ? ? [H1 H2]; split.
rewrite<- H2; assumption.
apply symmetry; assumption.
Qed.

Add Morphism Qmult with signature Qle ++> Qeq_pos ++> Qle as Qmult_le_morphism.
intros x y H1 a b [H2 H3].
rewrite H3.
apply Qmult_le_compat_r; auto.
rewrite<- H3.
assumption.
Qed.

Definition Qmax (p q : Q) : Q :=
if Qlt_le_dec p q then q else p.
Lemma Qmax_comm : p q, (Qmax p q == Qmax q p)%Q.
intros p q.
unfold Qmax; destruct (Qlt_le_dec p q); destruct (Qlt_le_dec q p);
auto with qarith.
Qed.
Lemma le_Qmax : p q r:Q, (p q)%Q → (p Qmax q r)%Q.
Proof.
intros p q r H.
unfold Qmax. destruct (Qlt_le_dec q r).
transitivity q. apply H. auto with qarith.
apply H.
Qed.

Lemma lt_Qmax : p q r:Q, (p < q)%Q → (p < Qmax q r)%Q.
Proof.
intros p q r H.
unfold Qmax ; destruct (Qlt_le_dec q r).
transitivity q ; auto with qarith.
apply H.
Qed.

Lemma Qmult_pos_le_compat :
a b c d:Q, 0 a b → 0 c da×c b×d.
intros.
apply transitivity with (b×c).
apply Qmult_le_compat_r; intuition.
setoid_rewrite Qmult_comm.
apply Qmult_le_compat_r; intuition.
apply transitivity with a; intuition.
Qed.

Lemma Qmult_pos_compat :
x y, 0 < x → 0 < y → 0 < x × y.
intros.
setoid_replace 0 with (0 × y).
apply Qmult_lt_compat_r; assumption.
ring.
Qed.

Lemma Qdiv_pos :
n, x :Q, 0 < x → 0 < x × (1 # n).
intros; apply Qmult_pos_compat.
assumption.
auto with qarith.
Qed.

Lemma Qplus_le_lt_compat :
a b c d, a bc < da+c < b + d.