diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-08 08:35:29 +0100 |
commit | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (patch) | |
tree | f54d8315891bec2f741545991f420dd4407bccc0 /flocq/Appli | |
parent | 44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758 (diff) | |
download | compcert-177c8fbc523a171e8c8470fa675f9a69ef7f99de.tar.gz compcert-177c8fbc523a171e8c8470fa675f9a69ef7f99de.zip |
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.
Diffstat (limited to 'flocq/Appli')
-rw-r--r-- | flocq/Appli/Fappli_IEEE.v | 10 | ||||
-rw-r--r-- | flocq/Appli/Fappli_double_round.v | 30 | ||||
-rw-r--r-- | flocq/Appli/Fappli_rnd_odd.v | 67 |
3 files changed, 46 insertions, 61 deletions
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 /\ diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v index 3ff6c31a..2c4937ab 100644 --- a/flocq/Appli/Fappli_double_round.v +++ b/flocq/Appli/Fappli_double_round.v @@ -183,8 +183,8 @@ destruct (Req_dec x' 0) as [Zx'|Nzx']. apply Rplus_le_compat_r. apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|]. unfold ulp, canonic_exp; bpow_simplify. - rewrite <- (Rinv_r 2) at 3; [|lra]. - rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|]. + apply Rmult_le_reg_l with (1 := Rlt_0_2). + replace (2 * (/ 2 * _)) with (bpow (fexp1 (ln_beta x) - ln_beta x)) by field. apply Rle_trans with 1; [|lra]. change 1 with (bpow 0); apply bpow_le. omega. @@ -1037,10 +1037,11 @@ destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); [now apply Hexp4; omega|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). -{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite <- Rinv_mult_distr; [|lra|lra]. +{ replace (/2 * /2) with (/4) by field. + rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. - change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r. + apply (Z2R_le (2 * 2) (beta * (beta * 1))). + rewrite Zmult_1_r. now apply Zmult_le_compat; omega. } assert (P2 : (0 < 2)%Z) by omega. unfold double_round_eq. @@ -1384,10 +1385,11 @@ assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). -{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite <- Rinv_mult_distr; [|lra|lra]. +{ replace (/2 * /2) with (/4) by field. + rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. - change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r. + apply (Z2R_le (2 * 2) (beta * (beta * 1))). + rewrite Zmult_1_r. now apply Zmult_le_compat; omega. } assert (Ly : y < bpow (ln_beta y)). { apply Rabs_lt_inv. @@ -1449,7 +1451,7 @@ apply double_round_gt_mid. unfold canonic_exp. apply (Rplus_le_reg_r (bpow (fexp2 (ln_beta (x - y))))); ring_simplify. apply Rle_trans with (2 * bpow (fexp1 (ln_beta (x - y)) - 1)). - * rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. + * replace (2 * bpow (fexp1 (ln_beta (x - y)) - 1)) with (bpow (fexp1 (ln_beta (x - y)) - 1) + bpow (fexp1 (ln_beta (x - y)) - 1)) by ring. apply Rplus_le_compat_l. now apply bpow_le. * unfold Zminus; rewrite bpow_plus. @@ -1458,10 +1460,10 @@ apply double_round_gt_mid. apply Rmult_le_compat_l; [now apply bpow_ge_0|]. unfold Fcore_Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. - rewrite <- (Rinv_r 2) at 3; [|lra]. - rewrite Rmult_comm; apply Rmult_le_compat_l; [lra|]. - apply Rinv_le; [lra|]. - now change 2 with (Z2R 2); apply Z2R_le. + apply Z2R_le, Rinv_le in Hbeta. + simpl in Hbeta. + lra. + apply Rlt_0_2. Qed. (* double_round_minus_aux{0,1,2} together *) @@ -4220,7 +4222,7 @@ destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - fexp1 (ln_beta (x / y)) bpow_simplify. rewrite (Rmult_comm _ y). do 2 rewrite Rmult_assoc. - change (Z2R _ * _) with x'. + change (Z2R (Zfloor _) * _) with x'. change (bpow _) with u1. apply (Rmult_lt_reg_l (/ 2)); [lra|]. rewrite Rmult_plus_distr_l. diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v index 4741047f..b6d985ac 100644 --- a/flocq/Appli/Fappli_rnd_odd.v +++ b/flocq/Appli/Fappli_rnd_odd.v @@ -20,7 +20,7 @@ COPYING file for more details. (** * Rounding to odd and its properties, including the equivalence between rnd_NE and double rounding with rnd_odd and then rnd_NE *) - +Require Import Reals Psatz. Require Import Fcore. Require Import Fcalc_ops. @@ -577,29 +577,23 @@ Qed. Lemma d_le_m: (F2R d <= m)%R. -apply Rmult_le_reg_l with 2%R. -auto with real. -apply Rplus_le_reg_l with (-F2R d)%R. -apply Rle_trans with (F2R d). -right; ring. -apply Rle_trans with (F2R u). -apply Rle_trans with x. -apply Hd. -apply Hu. -right; unfold m; field. +Proof. +assert (F2R d <= F2R u)%R. + apply Rle_trans with x. + apply Hd. + apply Hu. +unfold m. +lra. Qed. Lemma m_le_u: (m <= F2R u)%R. -apply Rmult_le_reg_l with 2%R. -auto with real. -apply Rplus_le_reg_l with (-F2R u)%R. -apply Rle_trans with (F2R d). -right; unfold m; field. -apply Rle_trans with (F2R u). -apply Rle_trans with x. -apply Hd. -apply Hu. -right; ring. +Proof. +assert (F2R d <= F2R u)%R. + apply Rle_trans with x. + apply Hd. + apply Hu. +unfold m. +lra. Qed. Lemma ln_beta_m: (0 < F2R d)%R -> (ln_beta beta m =ln_beta beta (F2R d) :>Z). @@ -641,20 +635,13 @@ now apply Rgt_not_eq. now apply generic_format_canonic. now left. replace m with (F2R d). -destruct (ln_beta beta (F2R d)) as (e,He). +destruct (ln_beta beta (F2R d)) as (e,He). simpl in *; rewrite Rabs_right in He. apply He. now apply Rgt_not_eq. apply Rle_ge; now left. -assert (F2R d = F2R u). -apply Rmult_eq_reg_l with (/2)%R. -apply Rplus_eq_reg_l with (/2*F2R u)%R. -apply trans_eq with m. -unfold m, Rdiv; ring. -rewrite H; field. -auto with real. -apply Rgt_not_eq, Rlt_gt; auto with real. -unfold m; rewrite <- H0; field. +unfold m in H |- *. +lra. Qed. @@ -666,7 +653,7 @@ apply ln_beta_unique_pos. unfold m; rewrite <- Y, Rplus_0_l. rewrite u_eq. destruct (ln_beta beta x) as (e,He). -rewrite Rabs_right in He. +rewrite Rabs_pos_eq in He by now apply Rlt_le. rewrite round_UP_small_pos with (ex:=e). rewrite ln_beta_bpow. ring_simplify (fexp e + 1 - 1)%Z. @@ -676,7 +663,7 @@ unfold Rdiv; apply Rmult_le_compat_l. apply bpow_ge_0. simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le. -auto with real. +exact Rlt_0_2. apply (Z2R_le 2). specialize (radix_gt_1 beta). omega. @@ -684,13 +671,11 @@ apply Rlt_le_trans with (bpow (fexp e)*1)%R. 2: right; ring. unfold Rdiv; apply Rmult_lt_compat_l. apply bpow_gt_0. -rewrite <- Rinv_1 at 3. -apply Rinv_lt; auto with real. +lra. now apply He, Rgt_not_eq. apply exp_small_round_0_pos with beta (Zfloor) x... now apply He, Rgt_not_eq. now rewrite <- d_eq, Y. -now left. Qed. @@ -723,9 +708,8 @@ unfold Rdiv; apply f_equal. unfold F2R; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, Hb, Z2R_mult. simpl; field. -apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2). -simpl; auto with real. -rewrite Rmult_0_r, <-Z2R_mult, <-Hb. +apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). +rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb. apply radix_pos. apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z. unfold Fmult. @@ -752,9 +736,8 @@ unfold Rdiv; apply f_equal. unfold F2R; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, Hb, Z2R_mult. simpl; field. -apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2). -simpl; auto with real. -rewrite Rmult_0_r, <-Z2R_mult, <-Hb. +apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). +rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb. apply radix_pos. apply trans_eq with (-1+Fexp u)%Z. unfold Fmult. |