diff options
author | 2007-06-21 11:46:13 +0000 | |
---|---|---|
committer | 2007-06-21 11:46:13 +0000 | |
commit | bd5b2a45c2ef00d63fc84f5f1bc577fcb3a3d0d9 (patch) | |
tree | 635e016228fd284c8f4165465b728f0c8cc48aa3 /theories/QArith/Qabs.v | |
parent | f4586d1e8b1116340574d9660117f93e7a1e4e3b (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.v | 103 |
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. |