-
Notifications
You must be signed in to change notification settings - Fork 1
/
Zsqrt_complements.v
95 lines (79 loc) · 1.86 KB
/
Zsqrt_complements.v
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
(* This code is copyrighted by its authors; it is distributed under *)
(* the terms of the LGPL license (see LICENSE and description files) *)
Require Import ZArith.
Require Import Reals.
Require Import Tactiques.
Require Import Zarith_operations.
Lemma Zsqrt_nul : forall z : Z, z = 0%Z -> Z.sqrt z = 0%Z.
Proof.
intros.
rewrite H.
simpl in |- *.
auto.
Qed.
Hint Resolve Zsqrt_nul: zarith.
Lemma Zsqrt_0 : Z.sqrt 0 = 0%Z.
Proof.
auto.
Qed.
Hint Resolve Zsqrt_0: zarith.
Lemma Zsqrt_pos : forall z : Z, (0 <= Z.sqrt z)%Z.
Proof.
intros.
unfold Z.sqrt in |- *.
case z; auto with zarith.
Qed.
Hint Resolve Zsqrt_pos: reals.
Lemma Zsqrt_sqrt :
forall z : Z, (0 <= z)%Z -> (IZR (Z.sqrt z) <= sqrt (IZR z))%R.
Proof.
intros.
apply Rsqr_incr_0_var.
rewrite Rsqr_sqrt.
unfold Rsqr in |- *.
rewrite <- mult_IZR.
apply IZR_le.
cut
(Z.sqrt z * Z.sqrt z <= z <
(Z.sqrt z + 1) * (Z.sqrt z + 1))%Z.
auto with zarith.
apply Z.sqrt_spec.
auto.
RingReplace 0%R (IZR 0).
apply IZR_le; auto.
apply sqrt_positivity.
RingReplace 0%R (IZR 0).
apply IZR_le; auto.
Qed.
Hint Resolve Zsqrt_sqrt: reals.
Lemma Zsqrt_sqrt_bis :
forall z : Z, (0 <= z)%Z -> (sqrt (IZR z) < IZR (Z.sqrt z) + 1)%R.
Proof.
intros.
apply Rsqr_incrst_0.
rewrite Rsqr_sqrt.
unfold Rsqr in |- *.
replace (IZR (Z.sqrt z) + 1)%R with (IZR (Z.sqrt z + Z.succ 0)).
rewrite <- mult_IZR.
apply IZR_lt.
cut
(Z.sqrt z * Z.sqrt z <= z <
(Z.sqrt z + 1) * (Z.sqrt z + 1))%Z.
intuition.
apply Z.sqrt_spec.
auto.
change 1%R with (IZR (Z.succ 0)).
rewrite <- plus_IZR.
trivial.
change 0%R with (IZR 0).
apply IZR_le; auto.
apply sqrt_positivity.
change 0%R with (IZR 0).
apply IZR_le; auto.
change 0%R with (IZR 0); change 1%R with (IZR (Z.succ 0)).
rewrite <- plus_IZR; apply IZR_le.
replace (Z.sqrt z + Z.succ 0)%Z with (Z.succ (Z.sqrt z));
[ idtac | omega ].
apply Zle_le_succ; apply Zsqrt_pos.
Qed.
Hint Resolve Zsqrt_sqrt_bis: reals.