aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith/Qabs.v
diff options
context:
space:
mode:
authorGravatar roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-06-21 11:46:13 +0000
committerGravatar roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-06-21 11:46:13 +0000
commitbd5b2a45c2ef00d63fc84f5f1bc577fcb3a3d0d9 (patch)
tree635e016228fd284c8f4165465b728f0c8cc48aa3 /theories/QArith/Qabs.v
parentf4586d1e8b1116340574d9660117f93e7a1e4e3b (diff)
Adding: Field instance for Q.
: Power function from Q -> Z -> Q. : Absolute value function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith/Qabs.v')
-rw-r--r--theories/QArith/Qabs.v103
1 files changed, 103 insertions, 0 deletions
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
new file mode 100644
index 000000000..511463ee7
--- /dev/null
+++ b/theories/QArith/Qabs.v
@@ -0,0 +1,103 @@
+Require Export QArith.
+Require Export Qreduction.
+
+Hint Resolve Qlt_le_weak : qarith.
+
+Definition Qabs (x:Q) := let (n,d):=x in (Zabs n#d).
+
+Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x).
+Proof.
+intros x P H1 H2.
+destruct x as [[|xn|xn] xd];
+[apply H1|apply H1|apply H2];
+abstract (compute; discriminate).
+Defined.
+
+Add Morphism Qabs with signature Qeq ==> Qeq as Qabs_wd.
+intros [xn xd] [yn yd] H.
+simpl.
+unfold Qeq in *.
+simpl in *.
+change (' yd)%Z with (Zabs (' yd)).
+change (' xd)%Z with (Zabs (' xd)).
+repeat rewrite <- Zabs_Zmult.
+congruence.
+Qed.
+
+Lemma Qabs_pos : forall x, 0 <= x -> Qabs x == x.
+Proof.
+intros x H.
+apply Qabs_case.
+reflexivity.
+intros H0.
+setoid_replace x with 0.
+reflexivity.
+apply Qle_antisym; assumption.
+Qed.
+
+Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x.
+Proof.
+intros x H.
+apply Qabs_case.
+intros H0.
+setoid_replace x with 0.
+reflexivity.
+apply Qle_antisym; assumption.
+reflexivity.
+Qed.
+
+Lemma Qabs_nonneg : forall x, 0 <= (Qabs x).
+intros x.
+apply Qabs_case.
+auto.
+apply (Qopp_le_compat x 0).
+Qed.
+
+Lemma Zabs_Qabs : forall n d, (Zabs n#d)==Qabs (n#d).
+Proof.
+intros [|n|n]; reflexivity.
+Qed.
+
+Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x.
+Proof.
+intros x.
+do 2 apply Qabs_case; try (intros; ring);
+(intros H0 H1;
+setoid_replace x with 0;[reflexivity|];
+apply Qle_antisym);try assumption;
+rewrite Qle_minus_iff in *;
+ring_simplify;
+ring_simplify in H1;
+assumption.
+Qed.
+
+Lemma Qabs_triangle : forall x y, Qabs (x+y) <= Qabs x + Qabs y.
+Proof.
+intros [xn xd] [yn yd].
+unfold Qplus.
+unfold Qle.
+simpl.
+apply Zmult_le_compat_r;auto with *.
+change (' yd)%Z with (Zabs (' yd)).
+change (' xd)%Z with (Zabs (' xd)).
+repeat rewrite <- Zabs_Zmult.
+apply Zabs_triangle.
+Qed.
+
+Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y).
+Proof.
+intros x y.
+rewrite Qle_minus_iff.
+setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring.
+rewrite <- Qle_minus_iff.
+setoid_replace (Qabs x) with (Qabs (x-y+y)).
+apply Qabs_triangle.
+apply Qabs_wd.
+ring.
+Qed.
+
+Definition Qminus' x y := Qred (Qminus x y).
+Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).
+Proof.
+ intros; unfold Qminus' in |- *; apply Qred_correct; auto.
+Qed.