Commit 3f8f6608 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Simplified proofs.

parent a59e0aa8
......@@ -40,12 +40,12 @@ split.
intros ((xm, xe), (Hx1, Hx2)).
rewrite Hx1.
eexists ; repeat split.
now rewrite Hx2.
exact Hx2.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
rewrite Hx1.
eexists ; repeat split.
now rewrite Hx2.
exact Hx2.
Qed.
Theorem FIX_format_satisfies_any :
......
......@@ -93,9 +93,7 @@ apply Zle_max_r.
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
apply generic_format_0.
simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta (Rabs x)) as (ex, Hx5).
......@@ -135,13 +133,8 @@ intros Hx2.
destruct (Req_dec x 0) as [Hx3|Hx3].
(* . . *)
rewrite Hx3.
exists (Float beta 0 emin) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
now apply Zlt_le_weak.
apply Zle_refl.
apply -> FLT_format_generic.
apply generic_format_0.
(* . . *)
destruct (proj2 (FLX_format_generic _ _ Hp x) Hx2) as ((xm, xe), (Hx4, Hx5)).
apply -> FLT_format_generic.
......
......@@ -68,9 +68,7 @@ now apply Zlt_le_weak.
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
rewrite Hx3.
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
apply generic_format_0.
simpl in Hx2.
unfold generic_format, canonic.
destruct (ln_beta beta (Rabs x)) as (ex, Hx4).
......
......@@ -123,10 +123,8 @@ now apply Zge_le.
(* . *)
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
exists (Float beta 0 (FTZ_exp (projT1 (ln_beta beta (Rabs x))))).
repeat split.
unfold F2R. simpl.
now rewrite Hx4, Rmult_0_l.
rewrite Hx4.
apply generic_format_0.
assert (Hx5: xm <> Z0).
intros H.
apply Hx4.
......
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