diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-04-29 09:32:44 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-04-29 09:32:44 +0200 |
commit | 4920f93e4f933c8616a3376da5264d63bd58afdc (patch) | |
tree | f05cdd8084fcbc2098bbad14dc5b3fe38bf34ba4 /flocq/Prop/Mult_error.v | |
parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
parent | e8c312eecf96ae1703f7ba0b65f107233d340238 (diff) | |
download | compcert-4920f93e4f933c8616a3376da5264d63bd58afdc.tar.gz compcert-4920f93e4f933c8616a3376da5264d63bd58afdc.zip |
Merge pull request #368 from silene/flocq-3.4
Upgrade to Flocq 4.1.
Diffstat (limited to 'flocq/Prop/Mult_error.v')
-rw-r--r-- | flocq/Prop/Mult_error.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/flocq/Prop/Mult_error.v b/flocq/Prop/Mult_error.v index f4467025..ce909350 100644 --- a/flocq/Prop/Mult_error.v +++ b/flocq/Prop/Mult_error.v @@ -19,7 +19,8 @@ COPYING file for more details. (** * Error of the multiplication is in the FLX/FLT format *) -From Coq Require Import Lia. +From Coq Require Import ZArith Reals Lia. + Require Import Core Operations Plus_error. Section Fprop_mult_error. @@ -243,8 +244,7 @@ destruct (mag beta x) as (ex,Ex) ; simpl. specialize (Ex Hx0). destruct (mag beta y) as (ey,Ey) ; simpl. specialize (Ey Hy0). -assert (emin + 2 * prec -1 < ex + ey)%Z. -2: lia. +cut (emin + 2 * prec -1 < ex + ey)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1:=Hxy). rewrite Rabs_mult, bpow_plus. @@ -298,7 +298,7 @@ destruct (mag beta x) as (ex,Hx). destruct (mag beta y) as (ey,Hy). simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z. 2: apply Zplus_le_compat; apply Z.le_max_l. -assert (e + 2*prec -1< ex+ey)%Z;[idtac|lia]. +cut (e + 2*prec -1< ex+ey)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=H1). rewrite Rabs_mult, bpow_plus. @@ -329,7 +329,7 @@ apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). -unfold FLT_exp; rewrite Z.max_l; [|lia]; rewrite <- Z.add_max_distr_r. +unfold FLT_exp; rewrite Z.max_l by lia; rewrite <- Z.add_max_distr_r. set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; lia|]. apply Z.le_max_l. Qed. |