diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-03-08 14:07:33 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-03-08 14:07:33 +0100 |
commit | a968152051941a0fc50a86c3fc15e90e22ed7c47 (patch) | |
tree | 70f2590a8ea026c2f8596220e60b829d21b6398c /lib | |
parent | de24549f572deb6519be2216ef364b7c80bfdece (diff) | |
parent | 177c8fbc523a171e8c8470fa675f9a69ef7f99de (diff) | |
download | compcert-a968152051941a0fc50a86c3fc15e90e22ed7c47.tar.gz compcert-a968152051941a0fc50a86c3fc15e90e22ed7c47.zip |
Merge pull request #175 from silene/IZR
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 'lib')
-rw-r--r-- | lib/Fappli_IEEE_extra.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v index f5ccec2a..c134a3b6 100644 --- a/lib/Fappli_IEEE_extra.v +++ b/lib/Fappli_IEEE_extra.v @@ -746,7 +746,7 @@ Proof. + apply Rlt_le_trans with 0%R; auto. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply Rlt_0_1. + replace 1%R with (Z2R (Zfloor x) + 1)%R. apply Zfloor_ub. rewrite H. simpl. apply Rplus_0_l. - rewrite Ztrunc_ceil in H by (apply Rlt_le; auto). split. - + apply Ropp_lt_cancel. rewrite Ropp_involutive. + + apply (Ropp_lt_cancel (-(1))). rewrite Ropp_involutive. replace 1%R with (Z2R (Zfloor (-x)) + 1)%R. apply Zfloor_ub. unfold Zceil in H. replace (Zfloor (-x)) with 0 by omega. simpl. apply Rplus_0_l. + apply Rlt_le_trans with 0%R; auto. apply Rle_0_1. @@ -1234,10 +1234,7 @@ Proof. { unfold eps. rewrite <- bpow_plus. replace (emin - 1 + -emin) with (-1) by omega. auto. } rewrite P. unfold Znearest. assert (F: Zfloor (/ 2)%R = 0). - { apply Zfloor_imp. - split. apply Rlt_le. apply Rinv_0_lt_compat. apply (Z2R_lt 0 2). omega. - change (Z2R (0 + 1)) with 1%R. rewrite <- Rinv_1 at 3. apply Rinv_1_lt_contravar. apply Rle_refl. apply (Z2R_lt 1 2). omega. - } + { apply Zfloor_imp. simpl. lra. } rewrite F. change (Z2R 0) with 0%R. rewrite Rminus_0_r. rewrite Rcompare_Eq by auto. simpl. unfold F2R; simpl. apply Rmult_0_l. } |