Commit 315c78ae authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Proved properties on cond_Zopp and cond_Ropp.

parent abcfddd5
......@@ -53,7 +53,6 @@ apply bpow_gt_0.
now rewrite scaled_mantissa_bpow.
Qed.
Definition cond_Zopp (b : bool) m := if b then Zopp m else m.
Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.
Theorem inbetween_float_round_sign :
......
......@@ -2230,3 +2230,60 @@ now intros [|] [|].
Qed.
End Bool.
Section cond_opp.
Definition cond_Zopp (b : bool) m := if b then Zopp m else m.
Definition cond_Ropp (b : bool) m := if b then Ropp m else m.
Theorem Z2R_cond_Zopp :
forall b m,
Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m).
Proof.
intros [|] m.
apply Z2R_opp.
apply refl_equal.
Qed.
Theorem abs_cond_Zopp :
forall b m,
Zabs (cond_Zopp b m) = Zabs m.
Proof.
intros [|] m.
apply Zabs_Zopp.
apply refl_equal.
Qed.
Theorem abs_cond_Ropp :
forall b m,
Rabs (cond_Ropp b m) = Rabs m.
Proof.
intros [|] m.
apply Rabs_Ropp.
apply refl_equal.
Qed.
Theorem cond_Zopp_Zlt_bool :
forall m,
cond_Zopp (Zlt_bool m 0) m = Zabs m.
Proof.
intros m.
apply sym_eq.
case Zlt_bool_spec ; intros Hm.
apply Zabs_non_eq.
now apply Zlt_le_weak.
now apply Zabs_eq.
Qed.
Theorem cond_Ropp_Rlt_bool :
forall m,
cond_Ropp (Rlt_bool m 0) m = Rabs m.
Proof.
intros m.
apply sym_eq.
case Rlt_bool_spec ; intros Hm.
now apply Rabs_left.
now apply Rabs_pos_eq.
Qed.
End cond_opp.
......@@ -490,4 +490,13 @@ apply sym_not_eq.
now apply Zlt_not_eq.
Qed.
Theorem F2R_cond_Zopp :
forall b m e,
F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).
Proof.
intros [|] m e ; unfold F2R ; simpl.
now rewrite Z2R_opp, Ropp_mult_distr_l_reverse.
apply refl_equal.
Qed.
End Float_prop.
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