diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-13 20:40:25 +0100 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-13 20:40:25 +0100 |
commit | 9007714f50a8ba49e2e6188cddada22a9fceed11 (patch) | |
tree | 6d06089baabea55ee10c76288fecf88b906eb31e /kvx/ExtFloats.v | |
parent | a90018e65444bcd7a4c85ddd815d315cd852e120 (diff) | |
download | compcert-kvx-9007714f50a8ba49e2e6188cddada22a9fceed11.tar.gz compcert-kvx-9007714f50a8ba49e2e6188cddada22a9fceed11.zip |
begin div algo
Diffstat (limited to 'kvx/ExtFloats.v')
-rw-r--r-- | kvx/ExtFloats.v | 55 |
1 files changed, 3 insertions, 52 deletions
diff --git a/kvx/ExtFloats.v b/kvx/ExtFloats.v index ea663735..332d3e3d 100644 --- a/kvx/ExtFloats.v +++ b/kvx/ExtFloats.v @@ -15,7 +15,7 @@ From Flocq Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd. -Require Import Floats Integers ZArith IEEE754_extra Zdiv Psatz. +Require Import Floats Integers ZArith. Module ExtFloat. (** TODO check with the actual KVX; @@ -32,6 +32,8 @@ Definition max (x : float) (y : float) : float := | Some Eq | Some Gt => x | Some Lt | None => y end. + +Definition one := Float.of_int (Int.repr (1%Z)). End ExtFloat. Module ExtFloat32. @@ -53,54 +55,3 @@ 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. |