diff options
| -rw-r--r-- | kvx/ExtFloats.v | 55 | ||||
| -rw-r--r-- | kvx/ExtValues.v | 65 |
2 files changed, 68 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. diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index b4e14898..c478f70b 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -754,3 +754,68 @@ Definition fmaddfs := triple_op_single (fun f1 f2 f3 => Float32.fma f2 f3 f1). Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma (Float.neg f2) f3 f1). Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma (Float32.neg f2) f3 f1). + +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd. +Require Import IEEE754_extra Zdiv Psatz Floats ExtFloats. + +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. + +Definition my_div (a b : val) := + let b_d := Val.maketotal (Val.floatofintu b) in + let invb_d := Val.floatofsingle (invfs (Val.maketotal (Val.singleofintu b))) in + let alpha := fmsubf (Vfloat ExtFloat.one) invb_d b_d in + let x := fmaddf invb_d alpha invb_d in + Val.mulf (Val.maketotal (Val.floatofintu a)) x. + +(* +Compute (my_div (Vint (Int.repr 3)) (Vint (Int.repr 5))). +*) |