aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith/Qcabs.v
blob: c0ababfff58752ed7cd86a876c0f151973ce2ef0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
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.