Commit bbd4745d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added a boolean version of Zeven.

parent f8248a86
......@@ -596,7 +596,7 @@ Definition new_location_even k l :=
end.
Theorem new_location_even_correct :
Zeven nb_steps ->
Zeven nb_steps = true ->
forall x k l, (0 <= k < nb_steps)%Z ->
inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
inbetween start (start + Z2R nb_steps * step) x (new_location_even k l).
......@@ -624,7 +624,8 @@ easy.
intros H.
rewrite <- H in Hk0.
now elim Hk0.
destruct (Zeven_ex _ He).
destruct (Zeven_ex nb_steps).
rewrite He in H.
omega.
(* . 2 * k = nb_steps *)
set (l' := match l with loc_Eq => loc_Mi | _ => loc_Hi end).
......@@ -651,7 +652,7 @@ Definition new_location_odd k l :=
end.
Theorem new_location_odd_correct :
Zodd nb_steps ->
Zeven nb_steps = false ->
forall x k l, (0 <= k < nb_steps)%Z ->
inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
inbetween start (start + Z2R nb_steps * step) x (new_location_odd k l).
......@@ -689,17 +690,14 @@ apply inbetween_step_Mi_Mi_odd with (1 := Hx) (2 := Hk1).
apply inbetween_step_Hi_Mi_odd with (1 := Hx) (2 := Hk1).
(* . 2 * k + 1 > nb_steps *)
apply inbetween_step_Hi with (1 := Hx).
destruct (Zodd_ex _ Ho).
destruct (Zeven_ex nb_steps).
rewrite Ho in H.
omega.
apply Hk.
Qed.
Definition new_location :=
match nb_steps with
| Zpos (xO _) => new_location_even
| Zpos (xI _) => new_location_odd
| _ => fun _ l => l
end.
if Zeven nb_steps then new_location_even else new_location_odd.
Theorem new_location_correct :
forall x k l, (0 <= k < nb_steps)%Z ->
......@@ -714,13 +712,9 @@ now intros _.
(* . *)
intros [p|p|] Hp _.
apply new_location_odd_correct with (2 := Hk) (3 := Hx).
rewrite Hp.
change (Zpos (xI p)) with (1 + 2 * Zpos p)%Z.
rewrite Zplus_comm.
apply Zodd_2p_plus_1.
now rewrite Hp.
apply new_location_even_correct with (2 := Hk) (3 := Hx).
rewrite Hp.
exact (Zeven_2p (Zpos p)).
now rewrite Hp.
now rewrite Hp in Hnb_steps.
(* . *)
now intros p _.
......@@ -974,7 +968,7 @@ Theorem inbetween_float_NE :
forall x m l, (0 < x)%R ->
let e := canonic_exponent beta fexp x in
inbetween_float m e x l ->
Rnd_NE_pt beta fexp x (F2R (Float beta (cond_incr (round_NE (projT1 (Zeven_odd_bool m)) l) m) e)).
Rnd_NE_pt beta fexp x (F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e)).
Proof.
intros x m l Hx e Hl.
assert (Hd := inbetween_float_DN _ _ _ Hl).
......@@ -1021,7 +1015,7 @@ rewrite Hd.
apply canonic_exponent_DN ; try easy.
rewrite <- Hd.
now apply F2R_gt_0_compat.
destruct (Zeven_odd_bool m) as ([|], Heo) ; simpl.
case_eq (Zeven m) ; intros Heo.
split.
apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd' Hu' loc_Mi).
easy.
......@@ -1044,11 +1038,15 @@ intros Hu''.
assert (Hcu : canonic beta fexp cu).
unfold canonic.
now rewrite <- Hu''.
simpl.
rewrite Hu''.
eexists ; repeat split.
exact Hcu.
replace (Fnum cu) with (Fnum (Float beta m e) + Fnum cu + -Fnum (Float beta m e))%Z by ring.
apply Zodd_plus_Zodd.
rewrite Zeven_plus.
rewrite Zeven_opp.
unfold Fnum at 3. rewrite Heo.
apply eqb_true.
rewrite Hu'' in Hu.
apply (DN_UP_parity_generic beta fexp prop_exp strong_fexp x (Float beta m e) cu) ; try easy.
apply (generic_format_discrete beta fexp x m).
......@@ -1056,10 +1054,8 @@ apply inbetween_bounds_strict_not_Eq with (2 := Hl).
apply F2R_lt_compat.
apply Zlt_succ.
easy.
rewrite Zopp_eq_mult_neg_1.
now apply Zodd_mult_Zodd.
(* - m = 0 *)
destruct (Zeven_odd_bool m) as ([|], Heo) ; simpl.
case_eq (Zeven m) ; intros Heo.
split.
apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd' Hu' loc_Mi).
easy.
......@@ -1070,8 +1066,7 @@ exists (Float beta 0 (canonic_exponent beta fexp 0)).
unfold canonic.
rewrite F2R_0.
repeat split.
rewrite <- Hm' in Heo.
elim Heo.
now rewrite <- Hm' in Heo.
(* loc_Hi *)
split.
rewrite <- Hu in Hu'.
......
......@@ -216,7 +216,7 @@ now apply FIX_format_generic.
Qed.
Theorem Rnd_NE_pt_FLT :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
Zeven (radix_val beta) = false \/ (1 < prec)%Z ->
rounding_pred (Rnd_NE_pt beta FLT_exp).
Proof.
intros H.
......
......@@ -223,7 +223,7 @@ exact FLX_exp_correct.
Qed.
Theorem Rnd_NE_pt_FLX :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
Zeven (radix_val beta) = false \/ (1 < prec)%Z ->
rounding_pred (Rnd_NE_pt beta FLX_exp).
Proof.
intros H.
......
......@@ -745,6 +745,76 @@ Qed.
End Floor_Ceil.
Section Even_Odd.
Definition Zeven (n : Z) :=
match n with
| Zpos (xO _) => true
| Zneg (xO _) => true
| Z0 => true
| _ => false
end.
Theorem Zeven_mult :
forall x y, Zeven (x * y) = orb (Zeven x) (Zeven y).
Proof.
now intros [|[xp|xp|]|[xp|xp|]] [|[yp|yp|]|[yp|yp|]].
Qed.
Theorem Zeven_opp :
forall x, Zeven (- x) = Zeven x.
Proof.
now intros [|[n|n|]|[n|n|]].
Qed.
Theorem Zeven_ex :
forall x, exists p, x = (2 * p + if Zeven x then 0 else 1)%Z.
Proof.
intros [|[n|n|]|[n|n|]].
now exists Z0.
now exists (Zpos n).
now exists (Zpos n).
now exists Z0.
exists (Zneg n - 1)%Z.
change (2 * Zneg n - 1 = 2 * (Zneg n - 1) + 1)%Z.
ring.
now exists (Zneg n).
now exists (-1)%Z.
Qed.
Theorem Zeven_2xp1 :
forall n, Zeven (2 * n + 1) = false.
Proof.
intros n.
destruct (Zeven_ex (2 * n + 1)) as (p, Hp).
revert Hp.
case (Zeven (2 * n + 1)) ; try easy.
intros H.
apply False_ind.
omega.
Qed.
Theorem Zeven_plus :
forall x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).
Proof.
intros x y.
destruct (Zeven_ex x) as (px, Hx).
rewrite Hx at 1.
destruct (Zeven_ex y) as (py, Hy).
rewrite Hy at 1.
replace (2 * px + (if Zeven x then 0 else 1) + (2 * py + (if Zeven y then 0 else 1)))%Z
with (2 * (px + py) + ((if Zeven x then 0 else 1) + (if Zeven y then 0 else 1)))%Z by ring.
case (Zeven x) ; case (Zeven y).
rewrite Zplus_0_r.
now rewrite Zeven_mult.
apply Zeven_2xp1.
apply Zeven_2xp1.
replace (2 * (px + py) + (1 + 1))%Z with (2 * (px + py + 1))%Z by ring.
now rewrite Zeven_mult.
Qed.
End Even_Odd.
Section pow.
Record radix := { radix_val : Z ; radix_prop : (2 <= radix_val )%Z }.
......@@ -1179,31 +1249,63 @@ elim He.
apply refl_equal.
Qed.
Theorem Zodd_Zpower :
forall b e, (0 <= e)%Z -> Zodd b ->
Zodd (Zpower b e).
Proof.
intros b e He Hb.
rewrite Zpower_Zpower_nat.
induction (Zabs_nat e).
exact I.
unfold Zpower_nat. simpl.
now apply Zodd_mult_Zodd.
exact He.
Qed.
Theorem Zeven_Zpower :
forall b e, (0 < e)%Z -> Zeven b ->
Zeven (Zpower b e).
forall b e, (0 < e)%Z ->
Zeven (Zpower b e) = Zeven b.
Proof.
intros b e He Hb.
intros b e He.
case_eq (Zeven b) ; intros Hb.
(* b even *)
replace e with (e - 1 + 1)%Z by ring.
rewrite Zpower_exp.
apply Zeven_mult_Zeven_r.
rewrite Zeven_mult.
replace (Zeven (b ^ 1)) with true.
apply Bool.orb_true_r.
unfold Zpower, Zpower_pos, iter_pos.
now rewrite Zmult_1_r.
omega.
discriminate.
(* b odd *)
rewrite Zpower_Zpower_nat.
induction (Zabs_nat e).
easy.
unfold Zpower_nat. simpl.
rewrite Zeven_mult.
now rewrite Hb.
now apply Zlt_le_weak.
Qed.
Theorem Zodd_Zpower :
forall b e, (0 <= e)%Z -> Zeven b = false ->
Zeven (Zpower b e) = false.
Proof.
intros b e He Hb.
destruct (Z_le_lt_eq_dec _ _ He) as [He'|He'].
rewrite <- Hb.
now apply Zeven_Zpower.
now rewrite <- He'.
Qed.
End pow.
Section Bool.
Theorem eqb_sym :
forall x y, Bool.eqb x y = Bool.eqb y x.
Proof.
now intros [|] [|].
Qed.
Theorem eqb_false :
forall x y, x = negb y -> Bool.eqb x y = false.
Proof.
now intros [|] [|].
Qed.
Theorem eqb_true :
forall x y, x = y -> Bool.eqb x y = true.
Proof.
now intros [|] [|].
Qed.
End Bool.
......@@ -19,7 +19,7 @@ Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition NE_prop (_ : R) f :=
exists g : float beta, f = F2R g /\ canonic g /\ Zeven (Fnum g).
exists g : float beta, f = F2R g /\ canonic g /\ Zeven (Fnum g) = true.
Definition Rnd_NE_pt :=
Rnd_NG_pt format NE_prop.
......@@ -32,7 +32,7 @@ Definition DN_UP_parity_pos_prop :=
canonic xu ->
F2R xd = rounding beta fexp ZrndDN x ->
F2R xu = rounding beta fexp ZrndUP x ->
Zodd (Fnum xd + Fnum xu).
Zeven (Fnum xd + Fnum xu) = false.
Definition DN_UP_parity_prop :=
forall x xd xu,
......@@ -41,7 +41,7 @@ Definition DN_UP_parity_prop :=
canonic xu ->
F2R xd = rounding beta fexp ZrndDN x ->
F2R xu = rounding beta fexp ZrndUP x ->
Zodd (Fnum xd + Fnum xu).
Zeven (Fnum xd + Fnum xu) = false.
Theorem DN_UP_parity_aux :
DN_UP_parity_pos_prop ->
......@@ -62,10 +62,9 @@ destruct xd as (md, ed).
destruct xu as (mu, eu).
simpl.
replace (md + mu)%Z
with (-1 * ((Fnum (Float beta (-mu) eu)) + Fnum (Float beta (-md) ed)))%Z
with (- ((Fnum (Float beta (-mu) eu)) + Fnum (Float beta (-md) ed)))%Z
by (unfold Fnum ; ring).
apply Zodd_mult_Zodd.
now apply (Zodd_pred 0).
rewrite Zeven_opp.
apply (Hpos (-x)%R _ _ Hx').
intros H.
apply Hfx.
......@@ -79,7 +78,7 @@ rewrite rounding_UP_opp, <- opp_F2R.
now apply f_equal.
Qed.
Definition NE_ex_prop := Zodd (radix_val beta) \/ forall e,
Definition NE_ex_prop := Zeven (radix_val beta) = false \/ forall e,
((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e).
Hypothesis strong_fexp : NE_ex_prop.
......@@ -185,22 +184,18 @@ now apply ln_beta_unique.
rewrite Hd3, Hu3.
unfold Fnum.
ring_simplify (Zpower (radix_val beta) (ex - fexp ex) - 1 + 1 * Zpower (radix_val beta) (ex - fexp (ex + 1)))%Z.
apply Zodd_pred.
destruct (Zeven_odd_dec (radix_val beta)) as [Hdo|Hdo].
apply Zeven_plus_Zeven.
apply Zeven_Zpower with (2 := Hdo).
omega.
apply Zeven_Zpower with (2 := Hdo).
unfold Zminus at 1.
rewrite 2!Zeven_plus.
rewrite Zeven_Zpower. 2: omega.
destruct strong_fexp.
now elim Zeven_not_Zodd with (1 := Hdo).
generalize (proj1 (H _) Hxe).
omega.
apply Zodd_plus_Zodd.
apply Zodd_Zpower with (2 := Hdo).
rewrite H.
rewrite Zodd_Zpower with (2 := H).
easy.
now apply Zle_minus_le_0.
rewrite Zeven_Zpower.
now rewrite Bool.eqb_reflx.
specialize (H ex).
omega.
apply Zodd_Zpower with (2 := Hdo).
apply Zle_minus_le_0.
exact Hxe2.
(* - xu < bpow ex *)
revert Hud.
unfold ulp, F2R.
......@@ -212,8 +207,7 @@ rewrite ln_beta_unique with (1 := Hexa).
intros H.
replace (Fnum xu) with (Fnum xd + 1)%Z.
replace (Fnum xd + (Fnum xd + 1))%Z with (2 * Fnum xd + 1)%Z by ring.
apply Zodd_Sn.
now apply Zeven_mult_Zeven_l.
apply Zeven_2xp1.
apply sym_eq.
apply eq_Z2R.
rewrite plus_Z2R.
......@@ -252,7 +246,7 @@ unfold generic_format.
set (ed := canonic_exponent beta fexp d).
set (md := Ztrunc (scaled_mantissa beta fexp d)).
intros Hd1.
destruct (Zeven_odd_dec md) as [He|Ho].
case_eq (Zeven md) ; [ intros He | intros Ho ].
right.
exists (Float beta md ed).
unfold Fcore_generic_fmt.canonic.
......@@ -269,8 +263,10 @@ eexists ; repeat split.
unfold Fcore_generic_fmt.canonic.
now rewrite <- Hu1.
simpl.
replace mu with (md + mu + (-1) * md)%Z by ring.
apply Zodd_plus_Zodd.
replace mu with (md + mu + -md)%Z by ring.
rewrite Zeven_plus.
rewrite Zeven_opp, Ho.
apply eqb_true.
apply (DN_UP_parity_generic x (Float beta md ed) (Float beta mu eu)).
exact Hf.
unfold Fcore_generic_fmt.canonic.
......@@ -283,7 +279,6 @@ now apply generic_DN_pt.
rewrite <- Hu1.
apply Rnd_UP_pt_unicity with (1 := Hu).
now apply generic_UP_pt.
now apply Zodd_mult_Zodd.
Qed.
Theorem Rnd_NE_pt_monotone :
......@@ -297,9 +292,9 @@ apply sym_eq.
apply Rnd_UP_pt_idempotent with (1 := Hu).
rewrite Hx.
apply Hd.
absurd (Zodd (Fnum cd + Fnum cu)).
apply Zeven_not_Zodd.
now apply Zeven_plus_Zeven.
absurd (Zeven (Fnum cd + Fnum cu) = false).
rewrite Zeven_plus.
now rewrite (proj2 Hd2), (proj2 Hu2).
apply (DN_UP_parity_aux DN_UP_parity_generic_pos x cd cu) ; try easy.
intros Hf.
apply Hx.
......@@ -696,7 +691,7 @@ Qed.
End Znearest.
Definition ZrndNE := ZrndN (fun x => if Zeven_dec (Zfloor x) then false else true).
Definition ZrndNE := ZrndN (fun x => negb (Zeven (Zfloor x))).
Theorem generic_NE_pt_pos :
forall x,
......@@ -725,9 +720,9 @@ unfold Znearest.
fold mx.
rewrite Hm.
rewrite Rcompare_Eq. 2: apply refl_equal.
destruct (Zeven_dec (Zfloor mx)) as [Hmx|Hmx].
case_eq (Zeven (Zfloor mx)) ; intros Hmx.
(* . even floor *)
change (Zeven (Ztrunc (scaled_mantissa beta fexp (rounding beta fexp ZrndDN x)))).
change (Zeven (Ztrunc (scaled_mantissa beta fexp (rounding beta fexp ZrndDN x))) = true).
destruct (Rle_or_lt (rounding beta fexp ZrndDN x) 0) as [Hr|Hr].
rewrite (Rle_antisym _ _ Hr).
unfold scaled_mantissa.
......@@ -740,7 +735,7 @@ now apply Rlt_le.
rewrite scaled_mantissa_DN ; try easy.
now rewrite Ztrunc_Z2R.
(* . odd floor *)
change (Zeven (Ztrunc (scaled_mantissa beta fexp (rounding beta fexp ZrndUP x)))).
change (Zeven (Ztrunc (scaled_mantissa beta fexp (rounding beta fexp ZrndUP x))) = true).
destruct (ln_beta beta x) as (ex, Hex).
specialize (Hex (Rgt_not_eq _ _ Hx)).
rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx)) in Hex.
......@@ -767,31 +762,29 @@ rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
rewrite Ztrunc_Z2R.
fold mx.
rewrite Hfc.
apply Zeven_Sn.
destruct (Zeven_odd_dec (Zfloor mx)) as [H|H].
now elim Hmx.
exact H.
now rewrite Zeven_plus, Hmx.
(* ... u = bpow *)
rewrite Hu'.
unfold scaled_mantissa, canonic_exponent.
rewrite ln_beta_bpow.
rewrite <- bpow_add, <- Z2R_Zpower.
rewrite Ztrunc_Z2R.
destruct (Zeven_odd_dec (radix_val beta)) as [Hr|Hr].
case_eq (Zeven (radix_val beta)) ; intros Hr.
destruct strong_fexp as [Hs|Hs].
now elim (Zeven_not_Zodd _ Hr).
now rewrite Hs in Hr.
destruct (Hs ex) as (H,_).
apply Zeven_Zpower.
omega.
rewrite Zeven_Zpower.
exact Hr.
elim Hmx.
replace (Zfloor mx) with (Zceil mx - 1)%Z by omega.
apply Zeven_pred.
omega.
assert (Zeven (Zfloor mx) = true). 2: now rewrite H in Hmx.
replace (Zfloor mx) with (Zceil mx + -1)%Z by omega.
rewrite Zeven_plus.
apply eqb_true.
unfold mx.
replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower (radix_val beta) (ex - fexp ex)).
apply Zodd_Zpower.
rewrite Zodd_Zpower with (2 := Hr).
easy.
omega.
exact Hr.
apply eq_Z2R.
rewrite Z2R_Zpower. 2: omega.
apply Rmult_eq_reg_r with (bpow (fexp ex)).
......@@ -805,7 +798,7 @@ apply bpow_gt_0.
generalize (proj1 (prop_exp ex) He).
omega.
(* .. small pos *)
elim Hmx.
assert (Zeven (Zfloor mx) = true). 2: now rewrite H in Hmx.
unfold mx, scaled_mantissa.
rewrite canonic_exponent_fexp_pos with (1 := Hex).
now rewrite mantissa_DN_small_pos.
......@@ -858,28 +851,13 @@ rewrite H.
unfold Rminus. rewrite Rplus_opp_r.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
destruct (Zeven_dec (Zfloor x)) as [H1|H1] ;
destruct (Zeven_dec (Zfloor (-x))) as [H2|H2] ; simpl ; trivial.
elim Zeven_not_Zodd with (1 := H2).
rewrite <- Zopp_involutive.
fold (Zceil x).
rewrite Zceil_floor_neq with (1 := H).
rewrite Zopp_plus_distr.
apply Zeven_plus_Zodd.
replace (- Zfloor x)%Z with (-1 * Zfloor x)%Z by ring.
now apply Zeven_mult_Zeven_r.
easy.
elim H2.
rewrite <- Zopp_involutive.
rewrite Bool.negb_involutive.
rewrite <- (Zopp_involutive (Zfloor (- x))).
fold (Zceil x).
rewrite Zeven_opp.
rewrite Zceil_floor_neq with (1 := H).
rewrite Zopp_plus_distr.
apply Zodd_plus_Zodd.
replace (- Zfloor x)%Z with (-1 * Zfloor x)%Z by ring.
apply Zodd_mult_Zodd.
easy.
now destruct (Zeven_odd_dec (Zfloor x)).
easy.
rewrite Zeven_plus.
now case (Zeven (Zfloor x)).
Qed.
Theorem generic_NE_pt :
......@@ -898,8 +876,7 @@ rewrite H1.
apply opp_F2R.
now apply canonic_opp.
simpl.
replace (- mg)%Z with ((-1) * mg)%Z by ring.
now apply Zeven_mult_Zeven_r.
now rewrite Zeven_opp.
rewrite <- rounding_NE_opp.
apply generic_NE_pt_pos.
now apply Ropp_0_gt_lt_contravar.
......
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