Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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).x:Q
Qred (Qabs x) = Qabs (Qred x)
Proof.x:Q
Qred (Qabs x) = Qabs (Qred x)
  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.x:Q
Qred x = x -> Qred (Qabs x) = Qabs x
Proof.x:Q
Qred x = x -> Qred (Qabs x) = Qabs x intros H; now rewrite (Qred_abs x), H. Qed.

Definition Qcabs (x:Qc) : Qc := {| canon := Qcabs_canon x (canon x) |}.
Notation "[ q ]" := (Qcabs 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].x:Qc
P:Qc -> Type
(0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P [x]
Proof.x:Qc
P:Qc -> Type
(0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P [x]
  intros A B.x:Qc
P:Qc -> Type
A:0 <= x -> P x
B:x <= 0 -> P (- x)
P [x]
  apply (Qabs_case x (fun x => forall Hx, P {|this:=x;canon:=Hx|})).x:Qc
P:Qc -> Type
A:0 <= x -> P x
B:x <= 0 -> P (- x)
(0 <= x)%Q ->
forall Hx : Qred x = x, P {| this := x; canon := Hx |}
x:Qc
P:Qc -> Type
A:0 <= x -> P x
B:x <= 0 -> P (- x)
(x <= 0)%Q ->
forall Hx : Qred (- x) = (- x)%Q,
P {| this := - x; canon := Hx |}
  intros; case (Qc_decomp x {|canon:=Hx|}); auto.x:Qc
P:Qc -> Type
A:0 <= x -> P x
B:x <= 0 -> P (- x)
(x <= 0)%Q ->
forall Hx : Qred (- x) = (- x)%Q,
P {| this := - x; canon := Hx |}
  intros; case (Qc_decomp (-x) {|canon:=Hx|}); auto.
Qed.

Lemma Qcabs_pos x : 0 <= x -> [x] = x.x:Qc
0 <= x -> [x] = x
Proof.x:Qc
0 <= x -> [x] = x
  intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x).x:Qc
Hx:0 <= x
Qabs x = x
  set (K := canon [x]); simpl in K; case K; clear K.x:Qc
Hx:0 <= x
Qred (Qabs x) = x
  set (a := x) at 1; case (canon x); subst a; apply Qred_complete.x:Qc
Hx:0 <= x
Qabs x == x
  now apply Qabs_pos.
Qed.

Lemma Qcabs_neg x : x <= 0 -> [x] = - x.x:Qc
x <= 0 -> [x] = - x
Proof.x:Qc
x <= 0 -> [x] = - x
  intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x).x:Qc
Hx:x <= 0
Qabs x = Qred (- x)
  set (K := canon [x]); simpl in K; case K; clear K.x:Qc
Hx:x <= 0
Qred (Qabs x) = Qred (- x)
  now apply Qred_complete; apply Qabs_neg.
Qed.

Lemma Qcabs_nonneg x : 0 <= [x].x:Qc
0 <= [x]
Proof.x:Qc
0 <= [x] intros; apply Qabs_nonneg. Qed.

Lemma Qcabs_opp x : [(-x)] = [x].x:Qc
[- x] = [x]
Proof.x:Qc
[- x] = [x]
  apply Qc_decomp; Qc_unfolds; fold (this x).x:Qc
Qabs (Qred (- x)) = Qabs x
  set (K := canon [x]); simpl in K; case K; clear K.x:Qc
Qabs (Qred (- x)) = Qred (Qabs x)
  case Qred_abs; apply Qred_complete; apply Qabs_opp.
Qed.

Lemma Qcabs_triangle x y : [x+y] <= [x] + [y].x, y:Qc
[x + y] <= [x] + [y]
Proof.x, y:Qc
[x + y] <= [x] + [y]
  Qc_unfolds; case Qred_abs; rewrite !Qred_le; apply Qabs_triangle.
Qed.

Lemma Qcabs_Qcmult x y : [x*y] = [x]*[y].x, y:Qc
[x * y] = [x] * [y]
Proof.x, y:Qc
[x * y] = [x] * [y]
  apply Qc_decomp; Qc_unfolds; fold (this x) (this y); case Qred_abs.x, y:Qc
Qred (Qabs (x * y)) = Qred (Qabs x * Qabs y)
  apply Qred_complete; apply Qabs_Qmult.
Qed.

Lemma Qcabs_Qcminus x y: [x-y] = [y-x].x, y:Qc
[x - y] = [y - x]
Proof.x, y:Qc
[x - y] = [y - x]
  apply Qc_decomp; Qc_unfolds; fold (this x) (this y) (this (-x)) (this (-y)).x, y:Qc
Qabs (Qred (x + Qred (- y))) =
Qabs (Qred (y + Qred (- x)))
  set (a := x) at 2; case (canon x); subst a.x, y:Qc
Qabs (Qred (Qred x + Qred (- y))) =
Qabs (Qred (y + Qred (- x)))
  set (a := y) at 1; case (canon y); subst a.x, y:Qc
Qabs (Qred (Qred x + Qred (- y))) =
Qabs (Qred (Qred y + Qred (- x)))
  rewrite !Qred_opp; fold (Qred x - Qred y)%Q (Qred y - Qred x)%Q.x, y:Qc
Qabs (Qred (Qred x - Qred y)) =
Qabs (Qred (Qred y - Qred x))
  repeat case Qred_abs; f_equal; apply Qabs_Qminus.
Qed.

Lemma Qcle_Qcabs x : x <= [x].x:Qc
x <= [x]
Proof.x:Qc
x <= [x] apply Qle_Qabs. Qed.

Lemma Qcabs_triangle_reverse x y : [x] - [y] <= [x - y].x, y:Qc
[x] - [y] <= [x - y]
Proof.x, y:Qc
[x] - [y] <= [x - y]
  unfold Qcle, Qcabs, Qcminus, Qcplus, Qcopp, Q2Qc, this;
  fold (this x) (this y) (this (-x)) (this (-y)).x, y:Qc
(Qred (Qabs x + Qred (- Qabs y)) <=
 Qabs (Qred (x + Qred (- y))))%Q
  case Qred_abs; rewrite !Qred_le, !Qred_opp, Qred_abs.x, y:Qc
(Qabs x + - Qabs (Qred y) <= Qabs (x + - Qred y))%Q
  apply Qabs_triangle_reverse.
Qed.

Lemma Qcabs_Qcle_condition x y : [x] <= y <-> -y <= x <= y.x, y:Qc
[x] <= y <-> - y <= x <= y
Proof.x, y:Qc
[x] <= y <-> - y <= x <= y
  Qc_unfolds; fold (this x) (this y).x, y:Qc
(Qabs x <= y)%Q <-> (Qred (- y) <= x <= y)%Q
  destruct (Qabs_Qle_condition x y) as [A B].x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
(Qabs x <= y)%Q <-> (Qred (- y) <= x <= y)%Q
  split; intros H.x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
H:(Qabs x <= y)%Q
(Qred (- y) <= x <= y)%Q
x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
H:(Qred (- y) <= x <= y)%Q
(Qabs x <= y)%Q
  +x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
H:(Qabs x <= y)%Q
(Qred (- y) <= x <= y)%Q destruct (A H) as [X Y]; split; auto.x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
H:(Qabs x <= y)%Q
X:(- y <= x)%Q
Y:(x <= y)%Q
(Qred (- y) <= x)%Q
    now case (canon x); apply Qred_le.
  +x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
H:(Qred (- y) <= x <= y)%Q
(Qabs x <= y)%Q destruct H as [X Y]; apply B; split; auto.x, y:Qc
A:(Qabs x <= y)%Q -> (- y <= x <= y)%Q
B:(- y <= x <= y)%Q -> (Qabs x <= y)%Q
X:(Qred (- y) <= x)%Q
Y:(x <= y)%Q
(- y <= x)%Q
    now case (canon y); case Qred_opp.
Qed.

Lemma Qcabs_diff_Qcle_condition x y r : [x-y] <= r <-> x - r <= y <= x + r.x, y, r:Qc
[x - y] <= r <-> x - r <= y <= x + r
Proof.x, y, r:Qc
[x - y] <= r <-> x - r <= y <= x + r
  Qc_unfolds; fold (this x) (this y) (this r).x, y, r:Qc
(Qabs (Qred (x + Qred (- y))) <= r)%Q <->
(Qred (x + Qred (- r)) <= y <= Qred (x + r))%Q
  case Qred_abs; repeat rewrite Qred_opp.x, y, r:Qc
(Qred (Qabs (x + - Qred y)) <= r)%Q <->
(Qred (x + - Qred r) <= y <= Qred (x + r))%Q
  set (a := y) at 1; case (canon y); subst a.x, y, r:Qc
(Qred (Qabs (x + - Qred y)) <= r)%Q <->
(Qred (x + - Qred r) <= Qred y <= Qred (x + r))%Q
  set (a := r) at 2; case (canon r); subst a.x, y, r:Qc
(Qred (Qabs (x + - Qred y)) <= Qred r)%Q <->
(Qred (x + - Qred r) <= Qred y <= Qred (x + Qred r))%Q
  set (a := Qred r) at 2 3;
  assert (K := canon (Q2Qc r)); simpl in K; case K; clear K; subst a.x, y, r:Qc
(Qred (Qabs (x + - Qred y)) <= Qred (Qred r))%Q <->
(Qred (x + - Qred r) <= Qred y <= Qred (x + Qred r))%Q
  set (a := Qred y) at 1;
  assert (K := canon (Q2Qc y)); simpl in K; case K; clear K; subst a.x, y, r:Qc
(Qred (Qabs (x + - Qred y)) <= Qred (Qred r))%Q <->
(Qred (x + - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q
  fold (x - Qred y)%Q (x - Qred r)%Q.x, y, r:Qc
(Qred (Qabs (x - Qred y)) <= Qred (Qred r))%Q <->
(Qred (x - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q
  destruct (Qabs_diff_Qle_condition x (Qred y) (Qred r)) as [A B].x, y, r:Qc
A:(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q
B:(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q
(Qred (Qabs (x - Qred y)) <= Qred (Qred r))%Q <->
(Qred (x - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q
  split.x, y, r:Qc
A:(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q
B:(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q
(Qred (Qabs (x - Qred y)) <= Qred (Qred r))%Q ->
(Qred (x - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q
x, y, r:Qc
A:(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q
B:(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q
(Qred (x - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q ->
(Qred (Qabs (x - Qred y)) <= Qred (Qred r))%Q
  +x, y, r:Qc
A:(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q
B:(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q
(Qred (Qabs (x - Qred y)) <= Qred (Qred r))%Q ->
(Qred (x - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q clear B; rewrite !Qred_le.x, y, r:Qc
A:(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q
(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q auto.
  +x, y, r:Qc
A:(Qabs (x - Qred y) <= Qred r)%Q ->
(x - Qred r <= Qred y <= x + Qred r)%Q
B:(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q
(Qred (x - Qred r) <= Qred (Qred y) <=
 Qred (x + Qred r))%Q ->
(Qred (Qabs (x - Qred y)) <= Qred (Qred r))%Q clear A; rewrite !Qred_le.x, y, r:Qc
B:(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q
(x - Qred r <= Qred y <= x + Qred r)%Q ->
(Qabs (x - Qred y) <= Qred r)%Q auto.
Qed.

Lemma Qcabs_null x : [x] = 0 -> x = 0.x:Qc
[x] = 0 -> x = 0
Proof.x:Qc
[x] = 0 -> x = 0
  intros H.x:Qc
H:[x] = 0
x = 0
  destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B].x:Qc
H:[x] = 0
[x] <= 0
x:Qc
H:[x] = 0
A:- 0 <= x
B:x <= 0
x = 0
  +x:Qc
H:[x] = 0
[x] <= 0 rewrite H; apply Qcle_refl.
  +x:Qc
H:[x] = 0
A:- 0 <= x
B:x <= 0
x = 0 apply Qcle_antisym; auto.
Qed.