Commit e58683ac authored by BOLDO Sylvie's avatar BOLDO Sylvie

canonic_0 and canonic_abs

parent f0bb7902
......@@ -196,16 +196,6 @@ apply canonic_exp_opp.
Qed.
Theorem canonic_0: canonic (Float beta 0 (fexp (ln_beta beta 0%R))).
unfold Fcore_generic_fmt.canonic; simpl.
unfold canonic_exp.
apply f_equal.
replace (F2R {| Fnum := 0; Fexp := fexp (ln_beta beta 0) |}) with 0%R.
reflexivity.
unfold F2R; simpl; ring.
Qed.
Theorem round_odd_pt :
forall x,
......@@ -280,6 +270,33 @@ rewrite <- round_0 with beta fexp Zfloor...
apply round_le...
now left.
intros Y.
generalize (DN_UP_parity_generic beta fexp)...
unfold DN_UP_parity_prop.
intros T; apply T with x; clear T.
unfold generic_format.
rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1.
unfold F2R; simpl.
apply Rmult_neq_compat_r.
apply Rgt_not_eq, bpow_gt_0.
rewrite Ztrunc_floor.
assumption.
apply Rmult_le_pos.
now left.
apply bpow_ge_0.
unfold Fcore_generic_fmt.canonic.
simpl.
apply sym_eq, canonic_exp_DN...
unfold Fcore_generic_fmt.canonic.
rewrite <- H0; reflexivity.
reflexivity.
apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)).
reflexivity.
apply round_generic...
intros Y.
replace (Fnum {| Fnum := Zfloor (scaled_mantissa beta fexp x); Fexp := cexp x |})
generalize (DN_UP_parity_generic beta fexp)...
unfold DN_UP_parity_prop.
intros T; apply T with x; clear T.
......@@ -310,6 +327,8 @@ rewrite Zfloor_Z2R; simpl.
SearchAbout Fnum.
......
......@@ -175,6 +175,26 @@ unfold canonic.
now rewrite F2R_Zopp, canonic_exp_opp.
Qed.
Theorem canonic_abs :
forall m e,
canonic (Float beta m e) ->
canonic (Float beta (Zabs m) e).
Proof.
intros m e H.
unfold canonic.
now rewrite F2R_Zabs, canonic_exp_abs.
Qed.
Theorem canonic_0: canonic (Float beta 0 (fexp (ln_beta beta 0%R))).
Proof.
unfold canonic; simpl; unfold canonic_exp.
replace (F2R {| Fnum := 0; Fexp := fexp (ln_beta beta 0) |}) with 0%R.
reflexivity.
unfold F2R; simpl; ring.
Qed.
Theorem canonic_unicity :
forall f1 f2,
canonic f1 ->
......
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