Qabs.v

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)         *)
(************************************************************************)

Require Export QArith.
Require Export Qreduction.

Hint Resolve Qlt_le_weak : qarith.

Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d).

Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x).forall (x : Q) (P : Q -> Type),
(0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x)
Proof.forall (x : Q) (P : Q -> Type),
(0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x)
intros x P H1 H2.x:Q
P:Q -> Type
H1:0 <= x -> P x
H2:x <= 0 -> P (- x)
P (Qabs x)
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.forall x y : Q, x == y -> Qabs x == Qabs y
intros [xn xd] [yn yd] H.xn:Z
xd:positive
yn:Z
yd:positive
H:xn # xd == yn # yd
Qabs (xn # xd) == Qabs (yn # yd)
simpl.xn:Z
xd:positive
yn:Z
yd:positive
H:xn # xd == yn # yd
Z.abs xn # xd == Z.abs yn # yd
unfold Qeq in *.xn:Z
xd:positive
yn:Z
yd:positive
H:(Qnum (xn # xd) * QDen (yn # yd))%Z =
(Qnum (yn # yd) * QDen (xn # xd))%Z
(Qnum (Z.abs xn # xd) * QDen (Z.abs yn # yd))%Z =
(Qnum (Z.abs yn # yd) * QDen (Z.abs xn # xd))%Z
simpl in *.xn:Z
xd:positive
yn:Z
yd:positive
H:(xn * Z.pos yd)%Z = (yn * Z.pos xd)%Z
(Z.abs xn * Z.pos yd)%Z = (Z.abs yn * Z.pos xd)%Z
change (Zpos yd)%Z with (Z.abs (Zpos yd)).xn:Z
xd:positive
yn:Z
yd:positive
H:(xn * Z.pos yd)%Z = (yn * Z.pos xd)%Z
(Z.abs xn * Z.abs (Z.pos yd))%Z =
(Z.abs yn * Z.pos xd)%Z
change (Zpos xd)%Z with (Z.abs (Zpos xd)).xn:Z
xd:positive
yn:Z
yd:positive
H:(xn * Z.pos yd)%Z = (yn * Z.pos xd)%Z
(Z.abs xn * Z.abs (Z.pos yd))%Z =
(Z.abs yn * Z.abs (Z.pos xd))%Z
repeat rewrite <- Z.abs_mul.xn:Z
xd:positive
yn:Z
yd:positive
H:(xn * Z.pos yd)%Z = (yn * Z.pos xd)%Z
Z.abs (xn * Z.pos yd) = Z.abs (yn * Z.pos xd)
congruence.
Qed.

Lemma Qabs_pos : forall x, 0 <= x -> Qabs x == x.forall x : Q, 0 <= x -> Qabs x == x
Proof.forall x : Q, 0 <= x -> Qabs x == x
intros x H.x:Q
H:0 <= x
Qabs x == x
apply Qabs_case.x:Q
H:0 <= x
0 <= x -> x == x
x:Q
H:0 <= x
x <= 0 -> - x == x
reflexivity.x:Q
H:0 <= x
x <= 0 -> - x == x
intros H0.x:Q
H:0 <= x
H0:x <= 0
- x == x
setoid_replace x with 0.x:Q
H:0 <= x
H0:x <= 0
- 0 == 0
x:Q
H:0 <= x
H0:x <= 0
x == 0
reflexivity.x:Q
H:0 <= x
H0:x <= 0
x == 0
apply Qle_antisym; assumption.
Qed.

Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x.forall x : Q, x <= 0 -> Qabs x == - x
Proof.forall x : Q, x <= 0 -> Qabs x == - x
intros x H.x:Q
H:x <= 0
Qabs x == - x
apply Qabs_case.x:Q
H:x <= 0
0 <= x -> x == - x
x:Q
H:x <= 0
x <= 0 -> - x == - x
intros H0.x:Q
H:x <= 0
H0:0 <= x
x == - x
x:Q
H:x <= 0
x <= 0 -> - x == - x
setoid_replace x with 0.x:Q
H:x <= 0
H0:0 <= x
0 == - 0
x:Q
H:x <= 0
H0:0 <= x
x == 0
x:Q
H:x <= 0
x <= 0 -> - x == - x
reflexivity.x:Q
H:x <= 0
H0:0 <= x
x == 0
x:Q
H:x <= 0
x <= 0 -> - x == - x
apply Qle_antisym; assumption.x:Q
H:x <= 0
x <= 0 -> - x == - x
reflexivity.
Qed.

Lemma Qabs_nonneg : forall x, 0 <= (Qabs x).forall x : Q, 0 <= Qabs x
intros x.x:Q
0 <= Qabs x
apply Qabs_case.x:Q
0 <= x -> 0 <= x
x:Q
x <= 0 -> 0 <= - x
auto.x:Q
x <= 0 -> 0 <= - x
apply (Qopp_le_compat x 0).
Qed.

Lemma Zabs_Qabs : forall n d, (Z.abs n#d)==Qabs (n#d).forall (n : Z) (d : positive),
Z.abs n # d == Qabs (n # d)
Proof.forall (n : Z) (d : positive),
Z.abs n # d == Qabs (n # d)
intros [|n|n]; reflexivity.
Qed.

Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x.forall x : Q, Qabs (- x) == Qabs x
Proof.forall x : Q, Qabs (- x) == Qabs x
intros x.x:Q
Qabs (- x) == Qabs 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.forall x y : Q, Qabs (x + y) <= Qabs x + Qabs y
Proof.forall x y : Q, Qabs (x + y) <= Qabs x + Qabs y
intros [xn xd] [yn yd].xn:Z
xd:positive
yn:Z
yd:positive
Qabs ((xn # xd) + (yn # yd)) <=
Qabs (xn # xd) + Qabs (yn # yd)
unfold Qplus.xn:Z
xd:positive
yn:Z
yd:positive
Qabs
  (Qnum (xn # xd) * QDen (yn # yd) +
   Qnum (yn # yd) * QDen (xn # xd)
   # Qden (xn # xd) * Qden (yn # yd)) <=
Qnum (Qabs (xn # xd)) * QDen (Qabs (yn # yd)) +
Qnum (Qabs (yn # yd)) * QDen (Qabs (xn # xd))
# Qden (Qabs (xn # xd)) * Qden (Qabs (yn # yd))
unfold Qle.xn:Z
xd:positive
yn:Z
yd:positive
(Qnum
   (Qabs
      (Qnum (xn # xd) * QDen (yn # yd) +
       Qnum (yn # yd) * QDen (xn # xd)
       # Qden (xn # xd) * Qden (yn # yd))) *
 QDen
   (Qnum (Qabs (xn # xd)) * QDen (Qabs (yn # yd)) +
    Qnum (Qabs (yn # yd)) * QDen (Qabs (xn # xd))
    # Qden (Qabs (xn # xd)) * Qden (Qabs (yn # yd))) <=
 Qnum
   (Qnum (Qabs (xn # xd)) * QDen (Qabs (yn # yd)) +
    Qnum (Qabs (yn # yd)) * QDen (Qabs (xn # xd))
    # Qden (Qabs (xn # xd)) * Qden (Qabs (yn # yd))) *
 QDen
   (Qabs
      (Qnum (xn # xd) * QDen (yn # yd) +
       Qnum (yn # yd) * QDen (xn # xd)
       # Qden (xn # xd) * Qden (yn # yd))))%Z
simpl.xn:Z
xd:positive
yn:Z
yd:positive
(Z.abs (xn * Z.pos yd + yn * Z.pos xd) *
 Z.pos (xd * yd) <=
 (Z.abs xn * Z.pos yd + Z.abs yn * Z.pos xd) *
 Z.pos (xd * yd))%Z
apply Z.mul_le_mono_nonneg_r;auto with *.xn:Z
xd:positive
yn:Z
yd:positive
(Z.abs (xn * Z.pos yd + yn * Z.pos xd) <=
 Z.abs xn * Z.pos yd + Z.abs yn * Z.pos xd)%Z
change (Zpos yd)%Z with (Z.abs (Zpos yd)).xn:Z
xd:positive
yn:Z
yd:positive
(Z.abs (xn * Z.abs (Z.pos yd) + yn * Z.pos xd) <=
 Z.abs xn * Z.abs (Z.pos yd) + Z.abs yn * Z.pos xd)%Z
change (Zpos xd)%Z with (Z.abs (Zpos xd)).xn:Z
xd:positive
yn:Z
yd:positive
(Z.abs (xn * Z.abs (Z.pos yd) + yn * Z.abs (Z.pos xd)) <=
 Z.abs xn * Z.abs (Z.pos yd) +
 Z.abs yn * Z.abs (Z.pos xd))%Z
repeat rewrite <- Z.abs_mul.xn:Z
xd:positive
yn:Z
yd:positive
(Z.abs (xn * Z.abs (Z.pos yd) + yn * Z.abs (Z.pos xd)) <=
 Z.abs (xn * Z.pos yd) + Z.abs (yn * Z.pos xd))%Z
apply Z.abs_triangle.
Qed.

Lemma Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).forall a b : Q, Qabs (a * b) == Qabs a * Qabs b
Proof.forall a b : Q, Qabs (a * b) == Qabs a * Qabs b
intros [an ad] [bn bd].an:Z
ad:positive
bn:Z
bd:positive
Qabs ((an # ad) * (bn # bd)) ==
Qabs (an # ad) * Qabs (bn # bd)
simpl.an:Z
ad:positive
bn:Z
bd:positive
Z.abs (an * bn) # ad * bd ==
(Z.abs an # ad) * (Z.abs bn # bd)
rewrite Z.abs_mul.an:Z
ad:positive
bn:Z
bd:positive
Z.abs an * Z.abs bn # ad * bd ==
(Z.abs an # ad) * (Z.abs bn # bd)
reflexivity.
Qed.

Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q).forall q : Q, Qabs (/ q) == / Qabs q
Proof.forall q : Q, Qabs (/ q) == / Qabs q
  intros [n d]; simpl.n:Z
d:positive
Qabs (/ (n # d)) == / (Z.abs n # d)
  unfold Qinv.n:Z
d:positive
Qabs
  match Qnum (n # d) with
  | 0%Z => 0
  | Z.pos p => QDen (n # d) # p
  | Z.neg p => Z.neg (Qden (n # d)) # p
  end ==
match Qnum (Z.abs n # d) with
| 0%Z => 0
| Z.pos p => QDen (Z.abs n # d) # p
| Z.neg p => Z.neg (Qden (Z.abs n # d)) # p
end
  case_eq n; intros; simpl in *; apply Qeq_refl.
Qed.
  
Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x).x, y:Q
Qabs (x - y) = Qabs (y - x)
Proof.x, y:Q
Qabs (x - y) = Qabs (y - x)
 unfold Qminus, Qopp.x, y:Q
Qabs (x + (- Qnum y # Qden y)) =
Qabs (y + (- Qnum x # Qden x)) simpl.x, y:Q
Z.abs (Qnum x * QDen y + - Qnum y * QDen x)
# Qden x * Qden y =
Z.abs (Qnum y * QDen x + - Qnum x * QDen y)
# Qden y * Qden x
 rewrite Pos.mul_comm, <- Z.abs_opp.x, y:Q
Z.abs (- (Qnum x * QDen y + - Qnum y * QDen x))
# Qden y * Qden x =
Z.abs (Qnum y * QDen x + - Qnum x * QDen y)
# Qden y * Qden x
 do 2 f_equal.x, y:Q
(- (Qnum x * QDen y + - Qnum y * QDen x))%Z =
(Qnum y * QDen x + - Qnum x * QDen y)%Z ring.
Qed.

Lemma Qle_Qabs : forall a, a <= Qabs a.forall a : Q, a <= Qabs a
Proof.forall a : Q, a <= Qabs a
intros a.a:Q
a <= Qabs a
apply Qabs_case; auto with *.a:Q
a <= 0 -> a <= - a
intros H.a:Q
H:a <= 0
a <= - a
apply Qle_trans with 0; try assumption.a:Q
H:a <= 0
0 <= - a
change 0 with (-0).a:Q
H:a <= 0
- 0 <= - a
apply Qopp_le_compat.a:Q
H:a <= 0
a <= 0
assumption.
Qed.

Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y).forall x y : Q, Qabs x - Qabs y <= Qabs (x - y)
Proof.forall x y : Q, Qabs x - Qabs y <= Qabs (x - y)
intros x y.x, y:Q
Qabs x - Qabs y <= Qabs (x - y)
rewrite Qle_minus_iff.x, y:Q
0 <= Qabs (x - y) + - (Qabs x - Qabs y)
setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring.x, y:Q
0 <= Qabs (x - y) + Qabs y + - Qabs x
rewrite <- Qle_minus_iff.x, y:Q
Qabs x <= Qabs (x - y) + Qabs y
setoid_replace (Qabs x) with (Qabs (x-y+y)).x, y:Q
Qabs (x - y + y) <= Qabs (x - y) + Qabs y
x, y:Q
Qabs x == Qabs (x - y + y)
apply Qabs_triangle.x, y:Q
Qabs x == Qabs (x - y + y)
apply Qabs_wd.x, y:Q
x == x - y + y
ring.
Qed.

Lemma Qabs_Qle_condition x y: Qabs x <= y <-> -y <= x <= y.x, y:Q
Qabs x <= y <-> - y <= x <= y
Proof.x, y:Q
Qabs x <= y <-> - y <= x <= y
 split.x, y:Q
Qabs x <= y -> - y <= x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
  split.x, y:Q
H:Qabs x <= y
- y <= x
x, y:Q
H:Qabs x <= y
x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
   rewrite <- (Qopp_opp x).x, y:Q
H:Qabs x <= y
- y <= - - x
x, y:Q
H:Qabs x <= y
x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
   apply Qopp_le_compat.x, y:Q
H:Qabs x <= y
- x <= y
x, y:Q
H:Qabs x <= y
x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
   apply Qle_trans with (Qabs (-x)).x, y:Q
H:Qabs x <= y
- x <= Qabs (- x)
x, y:Q
H:Qabs x <= y
Qabs (- x) <= y
x, y:Q
H:Qabs x <= y
x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
   apply Qle_Qabs.x, y:Q
H:Qabs x <= y
Qabs (- x) <= y
x, y:Q
H:Qabs x <= y
x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
   now rewrite Qabs_opp.x, y:Q
H:Qabs x <= y
x <= y
x, y:Q
- y <= x <= y -> Qabs x <= y
  apply Qle_trans with (Qabs x); auto using Qle_Qabs.x, y:Q
- y <= x <= y -> Qabs x <= y
 intros (H,H').x, y:Q
H:- y <= x
H':x <= y
Qabs x <= y
 apply Qabs_case; trivial.x, y:Q
H:- y <= x
H':x <= y
x <= 0 -> - x <= y
 intros.x, y:Q
H:- y <= x
H':x <= y
H0:x <= 0
- x <= y rewrite <- (Qopp_opp y).x, y:Q
H:- y <= x
H':x <= y
H0:x <= 0
- x <= - - y now apply Qopp_le_compat.
Qed.

Lemma Qabs_diff_Qle_condition x y r: Qabs (x - y) <= r <-> x - r <= y <= x + r.x, y, r:Q
Qabs (x - y) <= r <-> x - r <= y <= x + r
Proof.x, y, r:Q
Qabs (x - y) <= r <-> x - r <= y <= x + r
 intros.x, y, r:Q
Qabs (x - y) <= r <-> x - r <= y <= x + r unfold Qminus.x, y, r:Q
Qabs (x + - y) <= r <-> x + - r <= y <= x + r
 rewrite Qabs_Qle_condition.x, y, r:Q
- r <= x + - y <= r <-> x + - r <= y <= x + r
 rewrite <- (Qplus_le_l (-r) (x+-y) (y+r)).x, y, r:Q
- r + (y + r) <= x + - y + (y + r) /\ x + - y <= r <->
x + - r <= y <= x + r
 rewrite <- (Qplus_le_l (x+-y) r (y-r)).x, y, r:Q
- r + (y + r) <= x + - y + (y + r) /\
x + - y + (y - r) <= r + (y - r) <->
x + - r <= y <= x + r
 setoid_replace (-r + (y + r)) with y by ring.x, y, r:Q
y <= x + - y + (y + r) /\
x + - y + (y - r) <= r + (y - r) <->
x + - r <= y <= x + r
 setoid_replace (r + (y - r)) with y by ring.x, y, r:Q
y <= x + - y + (y + r) /\ x + - y + (y - r) <= y <->
x + - r <= y <= x + r
 setoid_replace (x + - y + (y + r)) with (x + r) by ring.x, y, r:Q
y <= x + r /\ x + - y + (y - r) <= y <->
x + - r <= y <= x + r
 setoid_replace (x + - y + (y - r)) with (x - r) by ring.x, y, r:Q
y <= x + r /\ x - r <= y <-> x + - r <= y <= x + r
 intuition.
Qed.