Commit b6a382bd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Factored proofs a bit.

parent a4ed3d8a
......@@ -120,43 +120,6 @@ apply FLT_format_generic.
exact FLT_exp_correct.
Qed.
Theorem FLT_format_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
( FLT_format x <-> FLX_format beta prec x ).
Proof.
intros x Hx1.
split.
(* . *)
intros ((xm, xe), (Hx2, (Hx3, Hx4))).
rewrite Hx2.
eexists ; split ; easy.
(* . *)
intros Hx2.
destruct (Req_dec x 0) as [Hx3|Hx3].
(* . . *)
rewrite Hx3.
apply <- FLT_format_generic.
apply generic_format_0.
(* . . *)
destruct (proj1 (FLX_format_generic _ _ Hp x) Hx2) as ((xm, xe), (Hx4, Hx5)).
apply <- FLT_format_generic.
rewrite Hx4.
eexists ; repeat split.
rewrite Hx5. clear Hx5.
rewrite <- Hx4.
destruct (ln_beta beta x) as (ex, Hx5).
unfold FLX_exp, FLT_exp.
simpl.
apply sym_eq.
apply Zmax_left.
cut (emin + prec <= ex)%Z. omega.
apply bpow_lt_bpow with beta.
apply Rle_lt_trans with (1 := Hx1).
now apply Hx5.
Qed.
(* TODO: vérifier si ça implique ^^ *)
Theorem FLT_canonic_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
......@@ -182,6 +145,31 @@ rewrite H, Rabs_R0.
apply bpow_gt_0.
Qed.
Theorem FLT_generic_format_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
( generic_format beta FLT_exp x <-> generic_format beta (FLX_exp prec) x ).
Proof.
intros x Hx.
assert (Hc := FLT_canonic_FLX x Hx).
split ; intros (f, Hf) ; exists f.
now apply -> Hc.
now apply <- Hc.
Qed.
Theorem FLT_format_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
( FLT_format x <-> FLX_format beta prec x ).
Proof.
intros x Hx1.
assert (Hc := FLT_canonic_FLX x Hx1).
apply iff_trans with (1 := FLT_format_generic x).
apply iff_trans with (1 := FLT_generic_format_FLX x Hx1).
apply iff_sym.
now apply FLX_format_generic.
Qed.
Theorem FLT_format_FIX :
forall x,
(Rabs x <= bpow (emin + prec))%R ->
......
......@@ -582,9 +582,8 @@ apply DN_UP_parity_FLX_pos with prec x xd xu cd cu ; try easy.
(* .. *)
intros H.
apply Hfx.
apply -> FLT_format_generic. 2: exact Hp.
apply <- FLT_format_FLX. 3: exact Hp.
now apply <- FLX_format_generic.
apply <- FLT_generic_format_FLX.
exact H.
rewrite Rabs_pos_eq.
now apply Rlt_le.
now apply Rlt_le.
......@@ -612,15 +611,11 @@ apply Hxu.
apply Rnd_DN_pt_equiv_format with (a := bpow (emin + prec - 1)) (b := x) (4 := Hxd).
exact Hn.
intros a (Ha, _).
apply iff_trans with (2 := FLX_format_generic beta prec Hp a).
assert (Ha' : (bpow (emin + prec - 1) <= Rabs a)%R).
apply FLT_generic_format_FLX.
rewrite Rabs_pos_eq.
exact Ha.
apply Rle_trans with (2 := Ha).
apply bpow_ge_0.
apply iff_trans with (2 := FLT_format_FLX beta emin prec Hp a Ha').
apply iff_sym.
now apply FLT_format_generic.
split.
now apply Rlt_le.
apply Rle_refl.
......
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