diff options
Diffstat (limited to 'theories/QArith/Qcabs.v')
| -rw-r--r-- | theories/QArith/Qcabs.v | 129 |
1 files changed, 129 insertions, 0 deletions
diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v new file mode 100644 index 00000000..c0ababff --- /dev/null +++ b/theories/QArith/Qcabs.v @@ -0,0 +1,129 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * An absolute value for normalized rational numbers. *) + +(** Contributed by Cédric Auger *) + +Require Import Qabs Qcanon. + +Lemma Qred_abs (x : Q) : Qred (Qabs x) = Qabs (Qred x). +Proof. + destruct x as [[|a|a] d]; simpl; auto; + destruct (Pos.ggcd a d) as [x [y z]]; simpl; auto. +Qed. + +Lemma Qcabs_canon (x : Q) : Qred x = x -> Qred (Qabs x) = Qabs x. +Proof. intros H; now rewrite (Qred_abs x), H. Qed. + +Definition Qcabs (x:Qc) : Qc := {| canon := Qcabs_canon x (canon x) |}. +Notation "[ q ]" := (Qcabs q) (q at next level, format "[ q ]") : Qc_scope. + +Ltac Qc_unfolds := + unfold Qcabs, Qcminus, Qcopp, Qcplus, Qcmult, Qcle, Q2Qc, this. + +Lemma Qcabs_case (x:Qc) (P : Qc -> Type) : + (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P [x]. +Proof. + intros A B. + apply (Qabs_case x (fun x => forall Hx, P {|this:=x;canon:=Hx|})). + intros; case (Qc_decomp x {|canon:=Hx|}); auto. + intros; case (Qc_decomp (-x) {|canon:=Hx|}); auto. +Qed. + +Lemma Qcabs_pos x : 0 <= x -> [x] = x. +Proof. + intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x). + set (K := canon [x]); simpl in K; case K; clear K. + set (a := x) at 1; case (canon x); subst a; apply Qred_complete. + now apply Qabs_pos. +Qed. + +Lemma Qcabs_neg x : x <= 0 -> [x] = - x. +Proof. + intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x). + set (K := canon [x]); simpl in K; case K; clear K. + now apply Qred_complete; apply Qabs_neg. +Qed. + +Lemma Qcabs_nonneg x : 0 <= [x]. +Proof. intros; apply Qabs_nonneg. Qed. + +Lemma Qcabs_opp x : [(-x)] = [x]. +Proof. + apply Qc_decomp; Qc_unfolds; fold (this x). + set (K := canon [x]); simpl in K; case K; clear K. + case Qred_abs; apply Qred_complete; apply Qabs_opp. +Qed. + +Lemma Qcabs_triangle x y : [x+y] <= [x] + [y]. +Proof. + Qc_unfolds; case Qred_abs; rewrite !Qred_le; apply Qabs_triangle. +Qed. + +Lemma Qcabs_Qcmult x y : [x*y] = [x]*[y]. +Proof. + apply Qc_decomp; Qc_unfolds; fold (this x) (this y); case Qred_abs. + apply Qred_complete; apply Qabs_Qmult. +Qed. + +Lemma Qcabs_Qcminus x y: [x-y] = [y-x]. +Proof. + apply Qc_decomp; Qc_unfolds; fold (this x) (this y) (this (-x)) (this (-y)). + set (a := x) at 2; case (canon x); subst a. + set (a := y) at 1; case (canon y); subst a. + rewrite !Qred_opp; fold (Qred x - Qred y)%Q (Qred y - Qred x)%Q. + repeat case Qred_abs; f_equal; apply Qabs_Qminus. +Qed. + +Lemma Qcle_Qcabs x : x <= [x]. +Proof. apply Qle_Qabs. Qed. + +Lemma Qcabs_triangle_reverse x y : [x] - [y] <= [x - y]. +Proof. + unfold Qcle, Qcabs, Qcminus, Qcplus, Qcopp, Q2Qc, this; + fold (this x) (this y) (this (-x)) (this (-y)). + case Qred_abs; rewrite !Qred_le, !Qred_opp, Qred_abs. + apply Qabs_triangle_reverse. +Qed. + +Lemma Qcabs_Qcle_condition x y : [x] <= y <-> -y <= x <= y. +Proof. + Qc_unfolds; fold (this x) (this y). + destruct (Qabs_Qle_condition x y) as [A B]. + split; intros H. + + destruct (A H) as [X Y]; split; auto. + now case (canon x); apply Qred_le. + + destruct H as [X Y]; apply B; split; auto. + now case (canon y); case Qred_opp. +Qed. + +Lemma Qcabs_diff_Qcle_condition x y r : [x-y] <= r <-> x - r <= y <= x + r. +Proof. + Qc_unfolds; fold (this x) (this y) (this r). + case Qred_abs; repeat rewrite Qred_opp. + set (a := y) at 1; case (canon y); subst a. + set (a := r) at 2; case (canon r); subst a. + set (a := Qred r) at 2 3; + assert (K := canon (Q2Qc r)); simpl in K; case K; clear K; subst a. + set (a := Qred y) at 1; + assert (K := canon (Q2Qc y)); simpl in K; case K; clear K; subst a. + fold (x - Qred y)%Q (x - Qred r)%Q. + destruct (Qabs_diff_Qle_condition x (Qred y) (Qred r)) as [A B]. + split. + + clear B; rewrite !Qred_le. auto. + + clear A; rewrite !Qred_le. auto. +Qed. + +Lemma Qcabs_null x : [x] = 0 -> x = 0. +Proof. + intros H. + destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B]. + + rewrite H; apply Qcle_refl. + + apply Qcle_antisym; auto. +Qed.
\ No newline at end of file |