blob: ea6637353872d918b3126d62f5ee318fd6dfd088 (
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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
Binary Round_odd.
Require Import Floats Integers ZArith IEEE754_extra Zdiv Psatz.
Module ExtFloat.
(** TODO check with the actual KVX;
this is what happens on x86 and may be inappropriate. *)
Definition min (x : float) (y : float) : float :=
match Float.compare x y with
| Some Eq | Some Lt => x
| Some Gt | None => y
end.
Definition max (x : float) (y : float) : float :=
match Float.compare x y with
| Some Eq | Some Gt => x
| Some Lt | None => y
end.
End ExtFloat.
Module ExtFloat32.
(** TODO check with the actual KVX *)
Definition min (x : float32) (y : float32) : float32 :=
match Float32.compare x y with
| Some Eq | Some Lt => x
| Some Gt | None => y
end.
Definition max (x : float32) (y : float32) : float32 :=
match Float32.compare x y with
| Some Eq | Some Gt => x
| Some Lt | None => y
end.
Definition one := Float32.of_int (Int.repr (1%Z)).
Definition inv (x : float32) : float32 :=
Float32.div one x.
End ExtFloat32.
Definition div_approx_reals (a b : Z) (x : R) :=
let q:=ZnearestE x in
let r:=a-q*b in
if r <? 0
then q-1
else q.
Lemma floor_ball1:
forall x : R, forall y : Z,
(Rabs (x - IZR y) < 1)%R -> Zfloor x = (y-1)%Z \/ Zfloor x = y.
Proof.
intros x y BALL.
apply Rabs_lt_inv in BALL.
case (Rcompare_spec x (IZR y)); intro CMP.
- left. apply Zfloor_imp.
ring_simplify (y-1+1).
rewrite minus_IZR. lra.
- subst.
rewrite Zfloor_IZR. right. reflexivity.
- right. apply Zfloor_imp.
rewrite plus_IZR. lra.
Qed.
Theorem div_approx_reals_correct:
forall a b : Z, forall x : R,
b > 0 ->
(Rabs (x - IZR a/ IZR b) < 1/2)%R ->
div_approx_reals a b x = (a/b)%Z.
Proof.
intros a b x bPOS GAP.
assert (0 < IZR b)%R by (apply IZR_lt ; lia).
unfold div_approx_reals.
pose proof (Znearest_imp2 (fun x => negb (Z.even x)) x) as NEAR.
assert (Rabs (IZR (ZnearestE x) - IZR a/ IZR b) < 1)%R as BALL.
{ pose proof (Rabs_triang (IZR (ZnearestE x) - x)
(x - IZR a/ IZR b)) as TRI.
ring_simplify (IZR (ZnearestE x) - x + (x - IZR a / IZR b))%R in TRI.
lra.
}
clear GAP NEAR.
rewrite Rabs_minus_sym in BALL.
pose proof (floor_ball1 _ _ BALL) as FLOOR.
clear BALL.
rewrite Zfloor_div in FLOOR by lia.
pose proof (Z_div_mod_eq_full a b) as DIV_MOD.
assert (0 < b) as bPOS' by lia.
pose proof (Z.mod_pos_bound a b bPOS') as MOD_BOUNDS.
case Z.ltb_spec; intro; destruct FLOOR; lia.
Qed.
|
