Adding a few lemmas for reasoning about inequalities over the

rationals.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10101 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 62 insertions, 1 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 6e18490108..0dccf64aa3 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -130,6 +130,12 @@ Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
 Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
 Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
 
+Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. 
+Proof.
+ auto with qarith.
+Qed.
+
+Hint Resolve Qnot_eq_sym : qarith.
 
 (** * Addition, multiplication and opposite *)
 
@@ -564,6 +570,9 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
 Qed.
 
+Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le 
+ Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih.
+
 (** Some decidability results about orders. *)
 
 Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}.
@@ -666,6 +675,46 @@ Proof.
 intros [[|n|n] d] Ha; assumption.
 Qed.
 
+Lemma Qle_shift_div_l : forall a b c, 
+ 0 < c -> a*c <= b -> a <= b/c.
+Proof.
+intros a b c Hc H.
+apply Qmult_lt_0_le_reg_r with (c).
+ assumption.
+setoid_replace (b/c*c) with (c*(b/c)) by apply Qmult_comm.
+rewrite Qmult_div_r; try assumption.
+auto with *.
+Qed.
+
+Lemma Qle_shift_recip_l : forall a c, 
+ 0 < c -> a*c <= 1 -> a <= /c.
+Proof.
+intros a c Hc H.
+setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l).
+change (a <= 1/c).
+apply Qle_shift_div_l; assumption.
+Qed.
+
+Lemma Qle_shift_div_r : forall a b c, 
+ 0 < b -> a <= c*b -> a/b <= c.
+Proof.
+intros a b c Hc H.
+apply Qmult_lt_0_le_reg_r with b.
+ assumption.
+setoid_replace (a/b*b) with (b*(a/b)) by apply Qmult_comm.
+rewrite Qmult_div_r; try assumption.
+auto with *.
+Qed.
+
+Lemma Qle_shift_recip_r : forall b c, 
+ 0 < b -> 1 <= c*b -> /b <= c.
+Proof.
+intros b c Hc H.
+setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l).
+change (1/b <= c).
+apply Qle_shift_div_r; assumption.
+Qed.
+
 (** * Rational to the n-th power *)
 
 Definition Qpower_positive (q:Q)(p:positive) : Q := 
@@ -694,4 +743,4 @@ Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp.
 Proof.
 intros x1 x2 Hx [|y|y]; try reflexivity;
 simpl; rewrite Hx; reflexivity.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 97b6e21875..f837de4222 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -190,3 +190,15 @@ replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring.
 ring_simplify.
 reflexivity.
 Qed.
+
+Lemma Qsqr_nonneg : forall a, 0 <= a^2.
+Proof.
+intros a.
+destruct (Qlt_le_dec 0 a) as [A|A].
+apply (Qmult_le_0_compat a a);
+ (apply Qlt_le_weak; assumption).
+setoid_replace (a^2) with ((-a)*(-a)) by ring.
+rewrite Qle_minus_iff in A.
+setoid_replace (0+ - a) with (-a) in A by ring.
+apply Qmult_le_0_compat; assumption.
+Qed.
\ No newline at end of file