diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 21:59:10 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 21:59:10 +0100 |
| commit | 9d4528e4edaa2b968d52628e6b5c10e6640f5e03 (patch) | |
| tree | 106710fea467acb15b5de56110c13a935bfc171a /lib | |
| parent | 0be6b3d13d2e8920653dde8cf8f7e27af608d812 (diff) | |
| download | compcert-kvx-9d4528e4edaa2b968d52628e6b5c10e6640f5e03.tar.gz compcert-kvx-9d4528e4edaa2b968d52628e6b5c10e6640f5e03.zip | |
factorize proof
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 50 |
1 files changed, 22 insertions, 28 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 2806e572..b8397210 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -899,19 +899,25 @@ Definition ZofB_ne (f: binary_float): option Z := | _ => None end. -Lemma ZnearestE_IZR: - forall n, (ZnearestE (IZR n)) = n. +Lemma Znearest_IZR : + forall choice n, (Znearest choice (IZR n)) = n. Proof. - intro n. - unfold ZnearestE. + intros. + unfold Znearest. case Rcompare_spec ; intro ORDER. - apply Zfloor_IZR. - - destruct negb. + - destruct choice. + apply Zceil_IZR. + apply Zfloor_IZR. - apply Zceil_IZR. Qed. +Lemma ZnearestE_IZR: + forall n, (ZnearestE (IZR n)) = n. +Proof. + apply Znearest_IZR. +Qed. + Lemma Zfloor_opp : forall x : R, (Zfloor (- x)) = - (Zceil x). Proof. @@ -1018,6 +1024,9 @@ Qed. Ltac field_simplify_den := field_simplify ; [idtac | lra]. Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra]. +Hint Rewrite <- plus_IZR minus_IZR opp_IZR mult_IZR : l_IZR. +Ltac l_IZR := autorewrite with l_IZR. + Theorem ZofB_ne_correct: forall f, ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. @@ -1053,28 +1062,22 @@ Proof. 2: lra. field_simplify_den. Rdiv_lt_0_den. - rewrite <- mult_IZR. - rewrite <- minus_IZR. + l_IZR. apply IZR_lt. lia. ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R. 2: lra. field_simplify_den. Rdiv_lt_0_den. - rewrite <- mult_IZR. - rewrite <- minus_IZR. + l_IZR. apply IZR_lt. lia. ** apply Rcompare_Eq. assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra]. field_simplify_den. - rewrite <- mult_IZR. - rewrite <- mult_IZR. - rewrite <- mult_IZR. - rewrite <- plus_IZR. - rewrite <- minus_IZR. + l_IZR. replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia. - field. lra. + field. apply IZR_neq. lia. * symmetry. apply Znearest_imp with (n := zm / p2p). apply Rabs_lt. split. @@ -1083,8 +1086,7 @@ Proof. 2: lra. field_simplify_den. apply Rmult_le_pos. - { rewrite <- mult_IZR. - rewrite <- minus_IZR. + { l_IZR. apply IZR_le. lia. } @@ -1092,10 +1094,7 @@ Proof. 2: lra. apply Rinv_0_lt_compat. assumption. ** assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT. - { rewrite <- mult_IZR. - rewrite <- minus_IZR. - rewrite <- mult_IZR. - rewrite <- plus_IZR. + { l_IZR. apply IZR_lt. lia. } assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT. @@ -1108,11 +1107,7 @@ Proof. apply Rabs_lt. split. ** assert (0 < (IZR zm - IZR p2p * IZR (zm / p2p)) - (IZR p2p * (IZR (zm / p2p) + 1) - IZR zm))%R. { ring_simplify. - rewrite <- mult_IZR. - rewrite <- mult_IZR. - rewrite <- mult_IZR. - rewrite <- minus_IZR. - rewrite <- minus_IZR. + l_IZR. apply IZR_lt. lia. } @@ -1126,8 +1121,7 @@ Proof. 2: lra. field_simplify_den. Rdiv_lt_0_den. - rewrite <- mult_IZR. - rewrite <- minus_IZR. + l_IZR. apply IZR_lt. pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. ring_simplify. |