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/Appli/Fappli_IEEE.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'flocq/Appli/Fappli_IEEE.v') diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index 6400304b..b6ccd84f 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -39,7 +39,7 @@ Inductive full_float := Definition FF2R beta x := match x with | F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e) - | _ => R0 + | _ => 0%R end. End AnyRadix. @@ -104,7 +104,7 @@ Definition B2FF x := Definition B2R f := match f with | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e) - | _ => R0 + | _ => 0%R end. Theorem FF2R_B2FF : @@ -346,11 +346,11 @@ Proof. intros. destruct x, y; try (apply B2R_inj; now eauto). - simpl in H2. congruence. - symmetry in H1. apply Rmult_integral in H1. - destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b0; discriminate H1. + destruct H1. apply (eq_Z2R _ 0) in H1. destruct b0; discriminate H1. simpl in H1. pose proof (bpow_gt_0 radix2 e). rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3. - apply Rmult_integral in H1. - destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b; discriminate H1. + destruct H1. apply (eq_Z2R _ 0) in H1. destruct b; discriminate H1. simpl in H1. pose proof (bpow_gt_0 radix2 e). rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3. Qed. @@ -1714,7 +1714,7 @@ Definition Bdiv div_nan m x y := Theorem Bdiv_correct : forall div_nan m x y, - B2R y <> R0 -> + B2R y <> 0%R -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\ is_finite (Bdiv div_nan m x y) = is_finite x /\ -- cgit