Commit d91303db authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added proofs that common formats are not FTZ.

parent 07c8584d
......@@ -66,4 +66,11 @@ right.
split ; easy.
Qed.
Theorem FIX_not_FTZ :
not_FTZ_prop FIX_exp.
Proof.
intros e.
apply Zle_refl.
Qed.
End RND_FIX.
......@@ -215,6 +215,19 @@ apply iff_sym.
now apply FIX_format_generic.
Qed.
Theorem FLT_not_FTZ :
not_FTZ_prop FLT_exp.
Proof.
intros e.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2.
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
Hypothesis NE_prop : Zeven (radix_val beta) = false \/ (1 < prec)%Z.
Theorem NE_ex_prop_FLT :
......
......@@ -222,6 +222,14 @@ now apply <- FLX_format_FLXN.
exact FLX_exp_correct.
Qed.
Theorem FLX_not_FTZ :
not_FTZ_prop FLX_exp.
Proof.
intros e.
unfold FLX_exp.
omega.
Qed.
Hypothesis NE_prop : Zeven (radix_val beta) = false \/ (1 < prec)%Z.
Theorem NE_ex_prop_FLX :
......
......@@ -876,7 +876,8 @@ apply Rnd_UP_pt_unicity with (1 := H).
apply generic_UP_pt.
Qed.
Hypothesis not_FTZ : forall e, (fexp (fexp e + 1) <= fexp e)%Z.
Definition not_FTZ_prop := forall e, (fexp (fexp e + 1) <= fexp e)%Z.
Hypothesis not_FTZ : not_FTZ_prop.
Theorem subnormal_exponent :
forall e x,
......
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