Commit 43aa5724 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix find and replace for Flocq

parent 08848ccd
...@@ -126,15 +126,15 @@ Definition bpowQ (r:radix) (e: Z) := ...@@ -126,15 +126,15 @@ Definition bpowQ (r:radix) (e: Z) :=
Definition B2Q := Definition B2Q :=
fun prec emax : Z => fun prec emax : Z =>
let emin := (3 - emax - prec)%Z in let emin := (3 - emax - prec)%Z in
let fexpr := Fcore_FLT.FLT_expr emin prec in let fexpr := Fcore_FLT.FLT_exp emin prec in
fun f : binary_float prec emax => fun f : binary_float prec emax =>
match f with match f with
| B754_zero _ _ _ => 0%Q | B754_zero _ _ _ => 0%Q
| B754_infinity _ _ _ => (bpowQ radix2 emax) +1%Q | B754_infinity _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_nan _ _ _ _ => (bpowQ radix2 emax) +1%Q | B754_nan _ _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_finite _ _ s m e _ => | B754_finite _ _ s m e _ =>
let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (' m); Fcore_defs.Fexpr := e |} in let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (' m); Fcore_defs.Fexp := e |} in
(Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexpr f_new) (Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
end. end.
Lemma B2Q_B2R_eq : Lemma B2Q_B2R_eq :
...@@ -393,7 +393,7 @@ Proof. ...@@ -393,7 +393,7 @@ Proof.
Qed. Qed.
Lemma round_0_zero: Lemma round_0_zero:
(Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_expr (3 - 1024 - 53) 53) (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE) 0) = 0%R. (round_mode mode_NE) 0) = 0%R.
Proof. Proof.
unfold Fcore_generic_fmt.round. simpl. unfold Fcore_generic_fmt.round. simpl.
...@@ -408,7 +408,7 @@ Proof. ...@@ -408,7 +408,7 @@ Proof.
assert (Rcompare (0) (/ 2) = Lt). assert (Rcompare (0) (/ 2) = Lt).
{ apply Rcompare_Lt. lra. } { apply Rcompare_Lt. lra. }
rewrite H0. rewrite H0.
unfold Fcore_generic_fmt.canonic_expr. unfold Fcore_generic_fmt.canonic_exp.
unfold Fcore_defs.F2R; simpl. unfold Fcore_defs.F2R; simpl.
rewrite Rmult_0_l. auto. rewrite Rmult_0_l. auto.
Qed. Qed.
...@@ -422,20 +422,20 @@ Lemma validValue_bounded b v_e1 v_e2: ...@@ -422,20 +422,20 @@ Lemma validValue_bounded b v_e1 v_e2:
(Rabs (Rabs
(Fcore_generic_fmt.round (Fcore_generic_fmt.round
radix2 radix2
(Fcore_FLT.FLT_expr (3 - 1024 - 53) 53) (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE) (round_mode mode_NE)
(evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)))) (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2))))
(bpow radix2 1024) = true. (bpow radix2 1024) = true.
Proof. Proof.
simpl. simpl.
pose proof (fexpr_correct 53 1024 eq_refl) as fexpr_corr. pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
assert (forall k : Z, (-1022 < k)%Z -> assert (forall k : Z, (-1022 < k)%Z ->
(53 <= k - Fcore_FLT.FLT_expr (3 - 1024 - 53) 53 k)%Z) (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
as expr_valid. as expr_valid.
{ intros k k_pos. { intros k k_pos.
unfold Fcore_FLT.FLT_expr; simpl. unfold Fcore_FLT.FLT_exp; simpl.
destruct (Z.max_spec_le (k - 53) (-1074)); omega. } destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_expr (3 -1024 - 53) 53) pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
(-1022)%Z 53%Z expr_valid) (-1022)%Z 53%Z expr_valid)
as rel_error_exists. as rel_error_exists.
intros [normal_v | zero_v] validVal; intros [normal_v | zero_v] validVal;
...@@ -477,7 +477,7 @@ Proof. ...@@ -477,7 +477,7 @@ Proof.
Qed. Qed.
(* (fexpr_correct 53 1024 eq_refl) as fexpr_corr. *) (* (fexpr_correct 53 1024 eq_refl) as fexpr_corr. *)
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_expr (3 -1024 - 53) 53) *) (* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
(* (-1022)%Z 53%Z) *) (* (-1022)%Z 53%Z) *)
Lemma eval_expr_gives_IEEE (e:expr fl64) : Lemma eval_expr_gives_IEEE (e:expr fl64) :
forall E1 E2 E2_real Gamma tMap vR A P fVars dVars, forall E1 E2 E2_real Gamma tMap vR A P fVars dVars,
...@@ -672,14 +672,14 @@ Proof. ...@@ -672,14 +672,14 @@ Proof.
clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
usedVars_sound R2 R1 L1 L R6 L0 R3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1 usedVars_sound R2 R1 L1 L R6 L0 R3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
IHe2. IHe2.
pose proof (fexpr_correct 53 1024 eq_refl) as fexpr_corr. pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
assert (forall k : Z, (-1022 < k)%Z -> assert (forall k : Z, (-1022 < k)%Z ->
(53 <= k - Fcore_FLT.FLT_expr (3 - 1024 - 53) 53 k)%Z) (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
as expr_valid. as expr_valid.
{ intros k k_pos. { intros k k_pos.
unfold Fcore_FLT.FLT_expr; simpl. unfold Fcore_FLT.FLT_exp; simpl.
destruct (Z.max_spec_le (k - 53) (-1074)); omega. } destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_expr (3 -1024 - 53) 53) pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
(-1022)%Z 53%Z expr_valid) (-1022)%Z 53%Z expr_valid)
as rel_error_exists. as rel_error_exists.
rewrite eval_float_e1, eval_float_e2 in H1. rewrite eval_float_e1, eval_float_e2 in H1.
......
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