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
|
(**
This example is part of the Flocq formalization of floating-point
arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2015-2018 Sylvie Boldo
#<br />#
Copyright (C) 2015-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
From Coq Require Import ZArith Reals.
From Flocq Require Import Core Bracket Round Operations Div Sqrt.
Section Compute.
Variable beta : radix.
Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Variable prec : Z.
Hypothesis Hprec : (0 < prec)%Z.
Hypothesis fexp_prec :
forall e, (e - prec <= fexp e)%Z.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Variable choice : bool -> Z -> location -> Z.
Hypothesis rnd_choice :
forall x m l,
inbetween_int m (Rabs x) l ->
rnd x = cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l).
Lemma Rsgn_F2R :
forall m e,
Rlt_bool (F2R (Float beta m e)) 0 = Zlt_bool m 0.
Proof.
intros m e.
case Zlt_bool_spec ; intros H.
apply Rlt_bool_true.
now apply F2R_lt_0.
apply Rlt_bool_false.
now apply F2R_ge_0.
Qed.
Definition plus (x y : float beta) :=
let (m, e) := Fplus x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
Theorem plus_correct :
forall x y : float beta,
round beta fexp rnd (F2R x + F2R y) = F2R (plus x y).
Proof.
intros x y.
unfold plus.
rewrite <- F2R_plus.
destruct (Fplus x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
apply Rsgn_F2R.
apply inbetween_Exact.
apply sym_eq, F2R_Zabs.
Qed.
Definition mult (x y : float beta) :=
let (m, e) := Fmult x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
Theorem mult_correct :
forall x y : float beta,
round beta fexp rnd (F2R x * F2R y) = F2R (mult x y).
Proof.
intros x y.
unfold mult.
rewrite <- F2R_mult.
destruct (Fmult x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
apply Rsgn_F2R.
apply inbetween_Exact.
apply sym_eq, F2R_Zabs.
Qed.
Definition sqrt (x : float beta) :=
if Zlt_bool 0 (Fnum x) then
let '(m', e', l) := truncate beta fexp (Fsqrt fexp x) in
Float beta (choice false m' l) e'
else Float beta 0 0.
Theorem sqrt_correct :
forall x : float beta,
round beta fexp rnd (R_sqrt.sqrt (F2R x)) = F2R (sqrt x).
Proof.
intros x.
unfold sqrt.
case Zlt_bool_spec ; intros Hm.
generalize (Fsqrt_correct fexp x (F2R_gt_0 _ _ Hm)).
destruct Fsqrt as [[m' e'] l].
intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l).
destruct truncate as [[m'' e''] l'].
now rewrite Rlt_bool_false by apply sqrt_ge_0.
now rewrite Rabs_pos_eq by apply sqrt_ge_0.
now left.
destruct (Req_dec (F2R x) 0) as [Hz|Hz].
rewrite Hz, sqrt_0, F2R_0.
now apply round_0.
unfold R_sqrt.sqrt.
destruct Rcase_abs as [H|H].
rewrite F2R_0.
now apply round_0.
destruct H as [H|H].
elim Rgt_not_le with (1 := H).
now apply F2R_le_0.
now elim Hz.
Qed.
Lemma Rsgn_div :
forall x y : R,
x <> 0%R -> y <> 0%R ->
Rlt_bool (x / y) 0 = xorb (Rlt_bool x 0) (Rlt_bool y 0).
Proof.
intros x y Hx0 Hy0.
unfold Rdiv.
case (Rlt_bool_spec x) ; intros Hx ;
case (Rlt_bool_spec y) ; intros Hy.
apply Rlt_bool_false.
rewrite <- Rmult_opp_opp.
apply Rlt_le, Rmult_lt_0_compat.
now apply Ropp_gt_lt_0_contravar.
apply Ropp_gt_lt_0_contravar.
now apply Rinv_lt_0_compat.
apply Rlt_bool_true.
apply Ropp_lt_cancel.
rewrite Ropp_0, <- Ropp_mult_distr_l_reverse.
apply Rmult_lt_0_compat.
now apply Ropp_gt_lt_0_contravar.
apply Rinv_0_lt_compat.
destruct Hy as [Hy|Hy].
easy.
now elim Hy0.
apply Rlt_bool_true.
apply Ropp_lt_cancel.
rewrite Ropp_0, <- Ropp_mult_distr_r_reverse.
apply Rmult_lt_0_compat.
destruct Hx as [Hx|Hx].
easy.
now elim Hx0.
apply Ropp_gt_lt_0_contravar.
now apply Rinv_lt_0_compat.
apply Rlt_bool_false.
apply Rlt_le, Rmult_lt_0_compat.
destruct Hx as [Hx|Hx].
easy.
now elim Hx0.
apply Rinv_0_lt_compat.
destruct Hy as [Hy|Hy].
easy.
now elim Hy0.
Qed.
Definition div (x y : float beta) :=
if Zeq_bool (Fnum x) 0 then Float beta 0 0
else
let '(m, e, l) := truncate beta fexp (Fdiv fexp (Fabs x) (Fabs y)) in
let s := xorb (Zlt_bool (Fnum x) 0) (Zlt_bool (Fnum y) 0) in
Float beta (cond_Zopp s (choice s m l)) e.
Theorem div_correct :
forall x y : float beta,
F2R y <> 0%R ->
round beta fexp rnd (F2R x / F2R y) = F2R (div x y).
Proof.
intros x y Hy.
unfold div.
case Zeq_bool_spec ; intros Hm.
destruct x as [mx ex].
simpl in Hm.
rewrite Hm, 2!F2R_0.
unfold Rdiv.
rewrite Rmult_0_l.
now apply round_0.
assert (0 < F2R (Fabs x))%R as Hx.
destruct x as [mx ex].
now apply F2R_gt_0, Z.abs_pos.
assert (0 < F2R (Fabs y))%R as Hy'.
destruct y as [my ey].
apply F2R_gt_0, Z.abs_pos.
contradict Hy.
rewrite Hy.
apply F2R_0.
generalize (Fdiv_correct fexp _ _ Hx Hy').
destruct Fdiv as [[m e] l].
intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l).
- destruct truncate as [[m' e'] l'].
apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
rewrite Rsgn_div.
apply f_equal2 ; apply Rsgn_F2R.
contradict Hm.
apply eq_0_F2R with (1 := Hm).
exact Hy.
- unfold Rdiv.
rewrite Rabs_mult, Rabs_Rinv by exact Hy.
now rewrite <- 2!F2R_abs.
- left.
rewrite <- cexp_abs.
unfold Rdiv.
rewrite Rabs_mult, Rabs_Rinv by exact Hy.
now rewrite <- 2!F2R_abs.
Qed.
End Compute.
|
