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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Square Root Function *)
Require Import NZAxioms NZMulOrder.
(** Interface of a sqrt function, then its specification on naturals *)
Module Type Sqrt (Import A : Typ).
Parameters Inline sqrt : t -> t.
End Sqrt.
Module Type SqrtNotation (A : Typ)(Import B : Sqrt A).
Notation "√ x" := (sqrt x) (at level 25).
End SqrtNotation.
Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.
Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a).
Axiom sqrt_neg : forall a, a<0 -> √a == 0.
End NZSqrtSpec.
Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A.
Module Type NZSqrt' (A : NZOrdAxiomsSig) := Sqrt' A <+ NZSqrtSpec A.
(** Derived properties of power *)
Module Type NZSqrtProp
(Import A : NZOrdAxiomsSig')
(Import B : NZSqrt' A)
(Import C : NZMulOrderProp A).
(** First, sqrt is non-negative *)
Lemma sqrt_spec_nonneg : forall a b,
b*b <= a < S b * S b -> 0 <= b.
Proof.
intros a b (LE,LT).
destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso.
assert (S b * S b < b * b).
rewrite mul_succ_l, <- (add_0_r (b*b)).
apply add_lt_le_mono.
apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r.
now apply le_succ_l.
order.
Qed.
Lemma sqrt_nonneg : forall a, 0<=√a.
Proof.
intros. destruct (lt_ge_cases a 0) as [Ha|Ha].
now rewrite (sqrt_neg _ Ha).
now apply (sqrt_spec_nonneg a), sqrt_spec.
Qed.
(** The spec of sqrt indeed determines it *)
Lemma sqrt_unique : forall a b, b*b <= a < S b * S b -> √a == b.
Proof.
intros a b (LEb,LTb).
assert (Ha : 0<=a) by (transitivity (b*b); trivial using square_nonneg).
assert (Hb : 0<=b) by (apply (sqrt_spec_nonneg a); now split).
assert (Ha': 0<=√a) by now apply sqrt_nonneg.
destruct (sqrt_spec a Ha) as (LEa,LTa).
assert (b <= √a).
apply lt_succ_r, square_lt_simpl_nonneg; [|order].
now apply lt_le_incl, lt_succ_r.
assert (√a <= b).
apply lt_succ_r, square_lt_simpl_nonneg; [|order].
now apply lt_le_incl, lt_succ_r.
order.
Qed.
(** Hence sqrt is a morphism *)
Instance sqrt_wd : Proper (eq==>eq) sqrt.
Proof.
intros x x' Hx.
destruct (lt_ge_cases x 0) as [H|H].
rewrite 2 sqrt_neg; trivial. reflexivity.
now rewrite <- Hx.
apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec.
Qed.
(** An alternate specification *)
Lemma sqrt_spec_alt : forall a, 0<=a -> exists r,
a == √a * √a + r /\ 0 <= r <= 2*√a.
Proof.
intros a Ha.
destruct (sqrt_spec _ Ha) as (LE,LT).
destruct (le_exists_sub _ _ LE) as (r & Hr & Hr').
exists r.
split. now rewrite add_comm.
split. trivial.
apply (add_le_mono_r _ _ (√a * √a)).
rewrite <- Hr, add_comm.
generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc.
Qed.
Lemma sqrt_unique' : forall a b c, 0<=c<=2*b ->
a == b*b + c -> sqrt a == b.
Proof.
intros a b c (Hc,H) EQ.
apply sqrt_unique.
rewrite EQ.
split.
rewrite <- add_0_r at 1. now apply add_le_mono_l.
nzsimpl. apply lt_succ_r.
rewrite <- add_assoc. apply add_le_mono_l.
generalize H; now nzsimpl'.
Qed.
(** Sqrt is exact on squares *)
Lemma sqrt_square : forall a, 0<=a -> √(a*a) == a.
Proof.
intros a Ha.
apply sqrt_unique' with 0.
split. order. apply mul_nonneg_nonneg; order'. now nzsimpl.
Qed.
(** Sqrt is a monotone function (but not a strict one) *)
Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b.
Proof.
intros a b Hab.
destruct (lt_ge_cases a 0) as [Ha|Ha].
rewrite (sqrt_neg _ Ha). apply sqrt_nonneg.
assert (Hb : 0 <= b) by order.
destruct (sqrt_spec a Ha) as (LE,_).
destruct (sqrt_spec b Hb) as (_,LT).
apply lt_succ_r.
apply square_lt_simpl_nonneg; try order.
now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
Qed.
(** No reverse result for <=, consider for instance √2 <= √1 *)
Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
Proof.
intros a b H.
destruct (lt_ge_cases b 0) as [Hb|Hb].
rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order.
destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|].
destruct (sqrt_spec a Ha) as (_,LT).
destruct (sqrt_spec b Hb) as (LE,_).
apply le_succ_l in H.
assert (S (√a) * S (√a) <= √b * √b).
apply mul_le_mono_nonneg; trivial.
now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
order.
Qed.
(** When left side is a square, we have an equivalence for <= *)
Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b*b<=a <-> b <= √a).
Proof.
intros a b Ha Hb. split; intros H.
rewrite <- (sqrt_square b); trivial.
now apply sqrt_le_mono.
destruct (sqrt_spec a Ha) as (LE,LT).
transitivity (√a * √a); trivial.
now apply mul_le_mono_nonneg.
Qed.
(** When right side is a square, we have an equivalence for < *)
Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b*b <-> √a < b).
Proof.
intros a b Ha Hb. split; intros H.
destruct (sqrt_spec a Ha) as (LE,_).
apply square_lt_simpl_nonneg; try order.
rewrite <- (sqrt_square b Hb) in H.
now apply sqrt_lt_cancel.
Qed.
(** Sqrt and basic constants *)
Lemma sqrt_0 : √0 == 0.
Proof.
rewrite <- (mul_0_l 0) at 1. now apply sqrt_square.
Qed.
Lemma sqrt_1 : √1 == 1.
Proof.
rewrite <- (mul_1_l 1) at 1. apply sqrt_square. order'.
Qed.
Lemma sqrt_2 : √2 == 1.
Proof.
apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'.
Qed.
Lemma sqrt_lt_lin : forall a, 1<a -> √a<a.
Proof.
intros a Ha. rewrite <- sqrt_lt_square; try order'.
rewrite <- (mul_1_r a) at 1.
rewrite <- mul_lt_mono_pos_l; order'.
Qed.
Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
Proof.
intros a Ha.
destruct (le_gt_cases a 0) as [H|H].
setoid_replace a with 0 by order. now rewrite sqrt_0.
destruct (le_gt_cases a 1) as [H'|H'].
rewrite <- le_succ_l, <- one_succ in H.
setoid_replace a with 1 by order. now rewrite sqrt_1.
now apply lt_le_incl, sqrt_lt_lin.
Qed.
(** Sqrt and multiplication. *)
(** Due to rounding error, we don't have the usual √(a*b) = √a*√b
but only lower and upper bounds. *)
Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
Proof.
intros a b.
destruct (lt_ge_cases a 0) as [Ha|Ha].
rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg.
destruct (lt_ge_cases b 0) as [Hb|Hb].
rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg.
assert (Ha':=sqrt_nonneg a).
assert (Hb':=sqrt_nonneg b).
apply sqrt_le_square; try now apply mul_nonneg_nonneg.
rewrite mul_shuffle1.
apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg.
now apply sqrt_spec.
now apply sqrt_spec.
Qed.
Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b).
Proof.
intros a b Ha Hb.
apply sqrt_lt_square.
now apply mul_nonneg_nonneg.
apply mul_nonneg_nonneg.
now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
rewrite mul_shuffle1.
apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec.
Qed.
(** And we can't find better approximations in general.
- The lower bound is exact for squares
- Concerning the upper bound, for any c>0, take a=b=c*c-1,
then √(a*b) = c*c -1 while S √a = S √b = c
*)
(** Sqrt and addition *)
Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
Proof.
assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b).
intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl.
apply sqrt_le_mono.
rewrite <- (add_0_l b) at 2.
apply add_le_mono_r; order.
intros a b.
destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX.
destruct (lt_ge_cases b 0) as [Hb|Hb].
rewrite (add_comm a), (add_comm (√a)); now apply AUX.
assert (Ha':=sqrt_nonneg a).
assert (Hb':=sqrt_nonneg b).
rewrite <- lt_succ_r.
apply sqrt_lt_square.
now apply add_nonneg_nonneg.
now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg.
destruct (sqrt_spec a Ha) as (_,LTa).
destruct (sqrt_spec b Hb) as (_,LTb).
revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r.
intros LTa LTb.
assert (H:=add_le_mono _ _ _ _ LTa LTb).
etransitivity; [eexact H|]. clear LTa LTb H.
rewrite <- (add_assoc _ (√a) (√a)).
rewrite <- (add_assoc _ (√b) (√b)).
rewrite add_shuffle1.
rewrite <- (add_assoc _ (√a + √b)).
rewrite (add_shuffle1 (√a) (√b)).
apply add_le_mono_r.
now apply add_square_le.
Qed.
(** convexity inequality for sqrt: sqrt of middle is above middle
of square roots. *)
Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)).
Proof.
intros a b Ha Hb.
assert (Ha':=sqrt_nonneg a).
assert (Hb':=sqrt_nonneg b).
apply sqrt_le_square.
apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg.
now apply add_nonneg_nonneg.
transitivity (2*(√a*√a + √b*√b)).
now apply square_add_le.
apply mul_le_mono_nonneg_l. order'.
apply add_le_mono; now apply sqrt_spec.
Qed.
End NZSqrtProp.
|
