Commit 74feb0d8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Split FIX_format_generic equivalence.

parent 4f1811cc
......@@ -52,16 +52,18 @@ apply Zle_refl.
now intros _ _.
Qed.
Theorem FIX_format_generic :
forall x : R, FIX_format x <-> generic_format beta FIX_exp x.
Theorem generic_format_FIX :
forall x, FIX_format x -> generic_format beta FIX_exp x.
Proof.
split.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
intros x ((xm, xe), (Hx1, Hx2)).
rewrite Hx1.
now apply generic_format_canonic.
(* . *)
intros H.
Qed.
Theorem FIX_format_generic :
forall x, generic_format beta FIX_exp x -> FIX_format x.
Proof.
intros x H.
rewrite H.
eexists ; repeat split.
Qed.
......@@ -71,8 +73,9 @@ Theorem FIX_format_satisfies_any :
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)).
intros x.
apply iff_sym.
split.
apply FIX_format_generic.
apply generic_format_FIX.
Qed.
Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
......
......@@ -246,8 +246,9 @@ Proof.
intros x Hx1.
apply iff_trans with (1 := FLT_format_generic x).
apply iff_trans with (1 := FLT_generic_format_FIX x Hx1).
apply iff_sym.
now apply FIX_format_generic.
split.
apply FIX_format_generic.
apply generic_format_FIX.
Qed.
(** FLT is a nice format: it has a monotone exponent... *)
......
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