From 177c8fbc523a171e8c8470fa675f9a69ef7f99de Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 8 Mar 2017 08:35:29 +0100 Subject: Adapt proofs to future handling of literal constants in Coq. This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented. --- flocq/Core/Fcore_FTZ.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'flocq/Core/Fcore_FTZ.v') diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v index 2ebc7851..a2fab00b 100644 --- a/flocq/Core/Fcore_FTZ.v +++ b/flocq/Core/Fcore_FTZ.v @@ -217,7 +217,7 @@ Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Definition Zrnd_FTZ x := - if Rle_bool R1 (Rabs x) then rnd x else Z0. + if Rle_bool 1 (Rabs x) then rnd x else Z0. Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ. Proof with auto with typeclass_instances. @@ -270,7 +270,7 @@ Proof. intros x Hx. unfold round, scaled_mantissa, canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. -assert (Hx0: x <> R0). +assert (Hx0: x <> 0%R). intros Hx0. apply Rle_not_lt with (1 := Hx). rewrite Hx0, Rabs_R0. @@ -286,7 +286,7 @@ rewrite Rle_bool_true. apply refl_equal. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))). -change R1 with (bpow 0). +change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FLX_exp prec ex)). rewrite bpow_plus. apply Rmult_le_compat_r. @@ -320,7 +320,7 @@ rewrite Rle_bool_false. apply F2R_0. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))). -change R1 with (bpow 0). +change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FTZ_exp ex)). rewrite bpow_plus. apply Rmult_lt_compat_r. -- cgit