Commit 840b5207 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added nearest even property to FIX, FLX, and FLT.

parent 6ef6c1a1
......@@ -493,4 +493,70 @@ Qed.
End Flocq_rnd_NE_generic.
Section Flocq_rnd_NE_FIX.
Variable emin : Z.
Theorem DN_UP_parity_FIX_pos :
DN_UP_parity_pos_prop (FIX_exp emin).
Proof.
apply DN_UP_parity_generic_pos.
apply FIX_exp_correct.
right.
split ; easy.
Qed.
End Flocq_rnd_NE_FIX.
Section Flocq_rnd_NE_FLX.
Variable prec : Z.
Hypothesis Hp : (0 < prec)%Z.
Theorem DN_UP_parity_FLX_pos :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
DN_UP_parity_pos_prop (FLX_exp prec).
Proof.
intros H.
apply DN_UP_parity_generic_pos.
now apply FLX_exp_correct.
destruct H.
now left.
right.
unfold FLX_exp ; split ; omega.
Qed.
End Flocq_rnd_NE_FLX.
Section Flocq_rnd_NE_FLT.
Variable emin : Z.
Variable prec : Z.
Hypothesis Hp : (0 < prec)%Z.
Theorem DN_UP_parity_FLT_pos :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
DN_UP_parity_pos_prop (FLT_exp emin prec).
Proof.
intros H.
apply DN_UP_parity_generic_pos.
now apply FLT_exp_correct.
destruct H.
now left.
right.
intros e.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)].
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
End Flocq_rnd_NE_FLT.
End Flocq_rnd_NE.
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