Commit a3f54c8c authored by Heiko Becker's avatar Heiko Becker

Port to Coq 8.7.2

parent 8f094df0
......@@ -325,7 +325,7 @@ Proof.
eapply Rmult_le_compat_l; auto.
apply Rabs_pos.
Qed.
Lemma err_prop_inversion_pos_real nF nR err elo ehi
(float_iv_pos : (0 < elo - err)%R)
......@@ -503,7 +503,6 @@ Proof.
rewrite <- Q2R_plus ; auto.
apply valid_bounds_e.
auto.
rewrite Q2R0_is_0; auto.
Qed.
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
......
......@@ -151,15 +151,15 @@ Proof.
- unfold Z2R, Q2R.
simpl. rewrite RMicromega.Rinv_1.
destruct (cond_Zopp b (' m)); unfold IZR;
try rewrite P2R_INR; try lra.
try rewrite P2R_INR, INR_IPR; lra.
- unfold Q2R; simpl.
unfold bpow, bpowQ.
destruct e; simpl; try lra.
+ rewrite RMicromega.Rinv_1.
unfold Z2R, IZR.
destruct (Z.pow_pos 2 p); try rewrite P2R_INR; auto.
destruct (Z.pow_pos 2 p); try rewrite P2R_INR, INR_IPR; auto.
+ unfold Z2R, IZR. unfold Qinv; simpl.
destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR; simpl; try lra.
destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR, INR_IPR; simpl; try lra.
* unfold bounded in e0. simpl in e0. unfold canonic_mantissa in e0.
simpl in e0.
pose proof (Is_true_eq_left _ e0).
......@@ -167,8 +167,11 @@ Proof.
assert (0 < Z.pow_pos 2 p)%Z.
{ apply Zpower_pos_gt_0. cbv; auto. }
rewrite Heqz in H0. inversion H0.
* rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute; try lra.
hnf; intros. pose proof (pos_INR_nat_of_P p0).
* unfold IPR at 1. rewrite Rmult_1_l; auto.
* rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute;
[ unfold IPR at 1; lra | ].
hnf; intros. pose proof (pos_INR_nat_of_P p0).
rewrite INR_IPR in *.
rewrite H0 in H1; lra.
Qed.
......@@ -456,19 +459,21 @@ Proof.
* unfold Normal in *. destruct normal_v.
eapply Rle_lt_trans; eauto.
unfold maxValue, bpow. unfold maxExponent. unfold Q2R.
unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR. simpl; lra.
unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR.
repeat rewrite <- INR_IPR. simpl. lra.
* unfold Denormal in *. destruct denormal_v.
eapply Rlt_trans; eauto.
unfold minValue, minExponentPos, bpow.
rewrite Q2R_inv.
{ unfold Q2R, Qnum, Qden.
rewrite <- Z2R_IZR; unfold IZR; simpl; lra. }
rewrite <- Z2R_IZR; unfold IZR.
repeat rewrite <- INR_IPR; simpl; lra. }
{ vm_compute; congruence. }
* rewrite zero_v. unfold bpow; simpl. rewrite Rabs_R0. lra.
* rewrite zero_v. simpl. rewrite Rabs_R0. lra.
- rewrite zero_v.
pose proof round_0_zero. simpl in H. rewrite H.
rewrite Rabs_R0.
unfold bpow. lra.
lra.
Qed.
(* (fexp_correct 53 1024 eq_refl) as fexp_corr. *)
......@@ -609,7 +614,6 @@ Proof.
apply Is_true_eq_true.
inversion Heqo1; inversion Heqo2; subst.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
(** MARKER **)
assert (validFloatValue (Q2R (B2Q v_e1)) M64).
{ eapply (FPRangeValidator_sound (B2Qexp e1)); try eauto; try set_tac.
eapply eval_eq_env; eauto. }
......@@ -701,10 +705,9 @@ Proof.
assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
by (vm_compute; auto).
rewrite H2 in H1. rewrite <- Z2R_IZR in H1. unfold IZR in H1.
simpl in H1. lra. }
simpl in H1. rewrite <- INR_IPR in H1. simpl in H1. lra. }
pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
destruct b; revert H1; intros case_eval.
(* Addition *)
+ unfold evalBinop in *. unfold b64_plus.
pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
......@@ -746,8 +749,6 @@ Proof.
assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
by (vm_compute; auto).
rewrite H12. rewrite Q2R_inv; try lra.
unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
simpl; lra.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- add_round; auto. }
......@@ -792,8 +793,6 @@ Proof.
assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
by (vm_compute; auto).
rewrite H12. rewrite Q2R_inv; try lra.
unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
simpl; lra.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- add_round; auto. }
......@@ -840,8 +839,6 @@ Proof.
assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
by (vm_compute; auto).
rewrite H12. rewrite Q2R_inv; try lra.
unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
simpl; lra.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- mult_round; auto.
......@@ -889,8 +886,6 @@ Proof.
assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
by (vm_compute; auto).
rewrite H12. rewrite Q2R_inv; try lra.
unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
simpl; lra.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- div_round; auto.
......
......@@ -29,7 +29,7 @@ fi
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
8.6)
8.7.2)
;;
*)
echo "Error: Need 8.6"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment