diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:45:34 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:45:34 +0100 |
| commit | 16b875d816a0b62037f4ffd1a0233f516529e5ec (patch) | |
| tree | b26772cac25d7b1d18f1184794a4f3287c0bcd7f /kvx | |
| parent | cae3d77b314778bd6b0dcc679ac7833c38ce7aeb (diff) | |
| download | compcert-kvx-16b875d816a0b62037f4ffd1a0233f516529e5ec.tar.gz compcert-kvx-16b875d816a0b62037f4ffd1a0233f516529e5ec.zip | |
simplify proof
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index d9c108a7..a7ed34fc 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -526,8 +526,6 @@ Proof. (IZR a' * (inv_b_r - 1 / IZR b')))%R by (field ; lra). set(delta := (inv_b_r - 1 / IZR b')%R) in *. cbn. - (* assert(Rabs - (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa. *) unfold approx_inv_thresh in *. assert (Rabs(IZR a' * delta) <= 3/8)%R as R2. { apply Rabs_le. @@ -538,8 +536,8 @@ Proof. pose proof (Rabs_triang (prod' - IZR a' * inv_b_r) (IZR a' * delta))%R. lra. } - pose proof (div_approx_reals_correct (Int.unsigned a) (Int.unsigned b) prod') as DIV_CORRECT. - rewrite <- DIV_CORRECT; cycle 1. lia. exact NEAR. + pose proof (div_approx_reals_correct (Int.unsigned a) (Int.unsigned b) prod' b_nz NEAR) as DIV_CORRECT. + rewrite <- DIV_CORRECT. unfold div_approx_reals in *. fold a' b' prod' prod_r. @@ -601,7 +599,7 @@ Proof. split. 2: cbn; lia. replace (prod_r + (-1)) with (prod_r - 1) by lia. - rewrite (DIV_CORRECT b_nz NEAR). + rewrite DIV_CORRECT. apply Z.div_pos; lia. - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false; cycle 1. |