diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 07:42:03 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 07:42:03 +0100 |
| commit | e185e82170dad225355cc4472ab341938e718b79 (patch) | |
| tree | 0f77d9f1db102e908cb5390b909d048ef82f776d /kvx | |
| parent | 03e9c06bc2f53212b596b4c61c047b1116f9408c (diff) | |
| download | compcert-kvx-e185e82170dad225355cc4472ab341938e718b79.tar.gz compcert-kvx-e185e82170dad225355cc4472ab341938e718b79.zip | |
one admit less
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 257e22b9..06d833bd 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -449,7 +449,11 @@ Proof. assert(0 <= prod_r <= 4294967295) as prod_r_range. { unfold prod_r. rewrite <- (Znearest_IZR (fun x => negb (Z.even x)) 0). - replace 4294967295 with (ZnearestE (17179869181 / 4)%R) by admit. + replace 4294967295 with (ZnearestE (17179869181 / 4)%R); cycle 1. + { apply Znearest_imp. + apply Rabs_lt. + lra. + } split; apply Znearest_le; lra. } |