Qcabs : absolute value on normalized rational numbers Qc

 File contributed by Cédric Auger (a long time ago, sorry!)

 Qarith and Qc would probably deserve many more results like this one,
 and a more modern style (for instance qualified names), but this commit
 is better than nothing...

4 files changed, 150 insertions, 12 deletions

diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v
new file mode 100644
index 000000000..c0ababfff
--- /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
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 078926e32..6bfa47bc5 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -81,14 +81,6 @@ Qed.
 Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
 Arguments Q2Qc q%Q.
 
-Lemma Qred_eq_iff (q q' : Q) : Qred q = Qred q' <-> q == q'.
-Proof.
- split.
- - intros E. rewrite <- (Qred_correct q), <- (Qred_correct q').
-   now rewrite E.
- - apply Qred_complete.
-Qed.
-
 Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.
 Proof.
  split; intro H.
@@ -488,7 +480,7 @@ Proof.
   destruct n; simpl.
   destruct 1; auto.
   intros.
-  now apply Qc_is_canon. 
+  now apply Qc_is_canon.
 Qed.
 
 Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index c50c38b28..131214f51 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -93,11 +93,17 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+Lemma Qred_eq_iff q q' : Qred q = Qred q' <-> q == q'.
+Proof.
+ split.
+ - intros E. rewrite <- (Qred_correct q), <- (Qred_correct q').
+   now rewrite E.
+ - apply Qred_complete.
+Qed.
+
 Add Morphism Qred : Qred_comp.
 Proof.
-  intros q q' H.
-  rewrite (Qred_correct q); auto.
-  rewrite (Qred_correct q'); auto.
+  intros. now rewrite !Qred_correct.
 Qed.
 
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
@@ -149,3 +155,13 @@ Theorem Qred_compare: forall x y,
 Proof.
   intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
 Qed.
+
+Lemma Qred_le q q' : Qred q <= Qred q' <-> q <= q'.
+Proof.
+  now rewrite !Qle_alt, <- Qred_compare.
+Qed.
+
+Lemma Qred_lt q q' : Qred q < Qred q' <-> q < q'.
+Proof.
+  now rewrite !Qlt_alt, <- Qred_compare.
+Qed.
diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget
index b3faef881..b550b4712 100644
--- a/theories/QArith/vo.itarget
+++ b/theories/QArith/vo.itarget
@@ -2,6 +2,7 @@ Qabs.vo
 QArith_base.vo
 QArith.vo
 Qcanon.vo
+Qcabs.vo
 Qfield.vo
 Qpower.vo
 Qreals.vo