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.
|
