From d8f1751b88d0013166412677c965079700e36557 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 24 Jan 2022 15:51:41 +0100 Subject: done for small a --- kvx/FPDivision64.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'kvx/FPDivision64.v') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 0d11c3cb..a53169b8 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1366,7 +1366,9 @@ Proof. with (-(a' - a' / b' * b')+b')%Z by ring. rewrite <- MOD. rewrite Int64.signed_repr; cycle 1. - { admit. + { change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + lia. } rewrite zlt_true by lia. ring. @@ -1376,8 +1378,10 @@ Proof. replace (a' / b' * b' - a')%Z with (-(a' - a' / b' * b'))%Z by ring. rewrite <- MOD. rewrite Int64.signed_repr ; cycle 1. - { admit. + { change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + lia. } rewrite zlt_false by lia. reflexivity. -Admitted. +Qed. -- cgit