diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 09:29:48 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 09:29:48 +0100 |
| commit | 6d75ed4e081bab3eb08b517a1a1a14131c22bcf1 (patch) | |
| tree | ee203b9f2daa8092e90ff73956fc07e2c3509f2a /kvx | |
| parent | 94dff310377cf75e9457dbf67fbc39fc2ab82c7b (diff) | |
| download | compcert-kvx-6d75ed4e081bab3eb08b517a1a1a14131c22bcf1.tar.gz compcert-kvx-6d75ed4e081bab3eb08b517a1a1a14131c22bcf1.zip | |
some admit less
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 573a8e18..9866ff13 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -505,11 +505,25 @@ Proof. rewrite Int64.unsigned_repr by (cbn; lia). rewrite Int64.unsigned_repr by (cbn; nia). case Z.ltb_spec; intro CMP. - - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true by admit. + - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true; cycle 1. + { unfold Int64.lt. + change (Int64.signed Int64.zero) with 0. + rewrite Int64.signed_repr; cycle 1. + admit. + rewrite zlt_true by lia. + reflexivity. + } cbn. f_equal. admit. - - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false by admit. + - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false; cycle 1. + { unfold Int64.lt. + change (Int64.signed Int64.zero) with 0. + rewrite Int64.signed_repr; cycle 1. + admit. + rewrite zlt_false by lia. + reflexivity. + } cbn. f_equal. admit. |