Commit 614a6aac by Guillaume Melquiond

### Use Zeven definition and theorems from the standard library.

parent 70d42306
 ... ... @@ -510,12 +510,12 @@ apply f_equal; unfold FLT_exp. rewrite Z.max_l. ring. omega. assert ((Zeven (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h)))) = false). assert ((Z.even (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h)))) = false). replace (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h))) with (Zpower radix2 prec -1)%Z. unfold Zminus; rewrite Zeven_plus. rewrite Zeven_opp. rewrite Zeven_Zpower. unfold Zminus; rewrite Z.even_add. rewrite Z.even_opp. rewrite Z.even_pow. reflexivity. unfold Prec_gt_0 in prec_gt_0_; omega. apply eq_IZR. ... ... @@ -1086,7 +1086,7 @@ apply Rle_lt_trans with (-(((IZR z) /2) - IZR (ZnearestE (IZR z / 2)))). right; ring. apply Rle_lt_trans with (1:= RRle_abs _). rewrite Rabs_Ropp. apply Rle_lt_trans with (1:=Znearest_N (fun x => negb (Zeven x)) _). apply Rle_lt_trans with (1:=Znearest_N (fun x => negb (Z.even x)) _). apply Rle_lt_trans with (1*/2);[right; ring|idtac]. apply Rlt_le_trans with ((IZR z)*/2);[idtac|right; field]. apply Rmult_lt_compat_r. ... ...
 ... ... @@ -1242,8 +1242,8 @@ apply Rplus_le_compat_r. apply IZR_le, kLe2. rewrite minus_IZR; simpl. generalize (beta); intros n. case (Zeven_odd_dec n); intros V. apply Zeven_ex_iff in V; destruct V as (m, Hm). case (Z.even_odd_dec n); intros V. apply Z.even_ex_iff in V; destruct V as (m, Hm). rewrite Hm, mult_IZR. replace (2*IZR m / 2) with (IZR m). rewrite Zceil_IZR. ... ...
 ... ... @@ -410,7 +410,7 @@ Definition new_location_even k l := end. Theorem new_location_even_correct : Zeven nb_steps = true -> Z.even nb_steps = true -> forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_even k l). ... ... @@ -467,7 +467,7 @@ Definition new_location_odd k l := end. Theorem new_location_odd_correct : Zeven nb_steps = false -> Z.even nb_steps = false -> forall x k l, (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_odd k l). ... ... @@ -504,7 +504,7 @@ apply Hk. Qed. Definition new_location := if Zeven nb_steps then new_location_even else new_location_odd. if Z.even nb_steps then new_location_even else new_location_odd. Theorem new_location_correct : forall x k l, (0 <= k < nb_steps)%Z -> ... ...
 ... ... @@ -444,34 +444,34 @@ Qed. Theorem inbetween_int_NE : forall x m l, inbetween_int m x l -> ZnearestE x = cond_incr (round_N (negb (Zeven m)) l) m. ZnearestE x = cond_incr (round_N (negb (Z.even m)) l) m. Proof. intros x m l Hl. now apply inbetween_int_N with (choice := fun x => negb (Zeven x)). now apply inbetween_int_N with (choice := fun x => negb (Z.even x)). Qed. Theorem inbetween_float_NE : forall x m l, let e := cexp beta fexp x in inbetween_float beta m e x l -> round beta fexp ZnearestE x = F2R (Float beta (cond_incr (round_N (negb (Zeven m)) l) m) e). round beta fexp ZnearestE x = F2R (Float beta (cond_incr (round_N (negb (Z.even m)) l) m) e). Proof. apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (negb (Zeven m)) l) m). apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (negb (Z.even m)) l) m). exact inbetween_int_NE. Qed. Theorem inbetween_int_NE_sign : forall x m l, inbetween_int m (Rabs x) l -> ZnearestE x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Zeven m)) l) m). ZnearestE x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Z.even m)) l) m). Proof. intros x m l Hl. erewrite inbetween_int_N_sign with (choice := fun x => negb (Zeven x)). erewrite inbetween_int_N_sign with (choice := fun x => negb (Z.even x)). 2: eexact Hl. apply f_equal. case Rlt_bool. rewrite Zeven_opp, Zeven_plus. now case (Zeven m). rewrite Z.even_opp, Z.even_add. now case (Z.even m). apply refl_equal. Qed. ... ... @@ -479,9 +479,9 @@ Theorem inbetween_float_NE_sign : forall x m l, let e := cexp beta fexp x in inbetween_float beta m e (Rabs x) l -> round beta fexp ZnearestE x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Zeven m)) l) m)) e). round beta fexp ZnearestE x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Z.even m)) l) m)) e). Proof. apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_N (negb (Zeven m)) l) m). apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_N (negb (Z.even m)) l) m). exact inbetween_int_NE_sign. Qed. ... ... @@ -801,7 +801,7 @@ rewrite Zdiv_0_l, Zmod_0_l. eexists. apply f_equal. unfold new_location. now case Zeven. now case Z.even. now eexists. destruct H as (e', H). rewrite H. ... ... @@ -1008,16 +1008,16 @@ Definition round_trunc_sign_ZR_correct := round_trunc_sign_any_correct _ (fun s m l => m) inbetween_int_ZR_sign. Definition round_NE_correct := round_any_correct _ (fun m l => cond_incr (round_N (negb (Zeven m)) l) m) inbetween_int_NE. round_any_correct _ (fun m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE. Definition round_trunc_NE_correct := round_trunc_any_correct _ (fun m l => cond_incr (round_N (negb (Zeven m)) l) m) inbetween_int_NE. round_trunc_any_correct _ (fun m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE. Definition round_sign_NE_correct := round_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Zeven m)) l) m) inbetween_int_NE_sign. round_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE_sign. Definition round_trunc_sign_NE_correct := round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Zeven m)) l) m) inbetween_int_NE_sign. round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE_sign. Definition round_NA_correct := round_any_correct _ (fun m l => cond_incr (round_N (Zle_bool 0 m) l) m) inbetween_int_NA. ... ...
 ... ... @@ -47,7 +47,7 @@ Definition Fsqrt_core prec m e := let d := Zdigits beta m in let s := Zmax (2 * prec - d) 0 in let e' := (e - s)%Z in let (s', e'') := if Zeven e' then (s, e') else (s + 1, e' - 1)%Z in let (s', e'') := if Z.even e' then (s, e') else (s + 1, e' - 1)%Z in let m' := match s' with | Zpos p => (m * Zpower_pos beta p)%Z ... ... @@ -71,11 +71,11 @@ unfold Fsqrt_core. set (d := Zdigits beta m). set (s := Zmax (2 * prec - d) 0). (* . exponent *) case_eq (if Zeven (e - s) then (s, (e - s)%Z) else ((s + 1)%Z, (e - s - 1)%Z)). case_eq (if Z.even (e - s) then (s, (e - s)%Z) else ((s + 1)%Z, (e - s - 1)%Z)). intros s' e' Hse. assert (He: (Zeven e' = true /\ 0 <= s' /\ 2 * prec - d <= s' /\ s' + e' = e)%Z). assert (He: (Z.even e' = true /\ 0 <= s' /\ 2 * prec - d <= s' /\ s' + e' = e)%Z). revert Hse. case_eq (Zeven (e - s)) ; intros He Hse ; inversion Hse. case_eq (Z.even (e - s)) ; intros He Hse ; inversion Hse. repeat split. exact He. unfold s. ... ... @@ -87,7 +87,7 @@ fold s. apply Zle_succ. repeat split. unfold Zminus at 1. now rewrite Zeven_plus, He. now rewrite Z.even_add, He. apply Zle_trans with (2 := H). apply Zle_max_r. apply Zle_trans with (2 := H). ... ...
 ... ... @@ -304,7 +304,7 @@ zify ; omega. Qed. (** and it allows a rounding to nearest, ties to even. *) Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z. Hypothesis NE_prop : Z.even beta = false \/ (1 < prec)%Z. Global Instance exists_NE_FLT : Exists_NE beta FLT_exp. Proof. ... ...
 ... ... @@ -251,7 +251,7 @@ now apply Zplus_le_compat_r. Qed. (** and it allows a rounding to nearest, ties to even. *) Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z. Hypothesis NE_prop : Z.even beta = false \/ (1 < prec)%Z. Global Instance exists_NE_FLX : Exists_NE beta FLX_exp. Proof. ... ...
 ... ... @@ -20,7 +20,7 @@ COPYING file for more details. (** * Rounding to nearest, ties to even: existence, unicity... *) Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp. Notation ZnearestE := (Znearest (fun x => negb (Zeven x))). Notation ZnearestE := (Znearest (fun x => negb (Z.even x))). Section Fcore_rnd_NE. ... ... @@ -36,7 +36,7 @@ Notation format := (generic_format beta fexp). Notation canonical := (canonical beta fexp). Definition NE_prop (_ : R) f := exists g : float beta, f = F2R g /\ canonical g /\ Zeven (Fnum g) = true. exists g : float beta, f = F2R g /\ canonical g /\ Z.even (Fnum g) = true. Definition Rnd_NE_pt := Rnd_NG_pt format NE_prop. ... ... @@ -49,7 +49,7 @@ Definition DN_UP_parity_pos_prop := canonical xu -> F2R xd = round beta fexp Zfloor x -> F2R xu = round beta fexp Zceil x -> Zeven (Fnum xu) = negb (Zeven (Fnum xd)). Z.even (Fnum xu) = negb (Z.even (Fnum xd)). Definition DN_UP_parity_prop := forall x xd xu, ... ... @@ -58,7 +58,7 @@ Definition DN_UP_parity_prop := canonical xu -> F2R xd = round beta fexp Zfloor x -> F2R xu = round beta fexp Zceil x -> Zeven (Fnum xu) = negb (Zeven (Fnum xd)). Z.even (Fnum xu) = negb (Z.even (Fnum xd)). Lemma DN_UP_parity_aux : DN_UP_parity_pos_prop -> ... ... @@ -78,11 +78,11 @@ now rewrite Ropp_involutive, Ropp_0. destruct xd as (md, ed). destruct xu as (mu, eu). simpl. rewrite <- (Bool.negb_involutive (Zeven mu)). rewrite <- (Bool.negb_involutive (Z.even mu)). apply f_equal. apply sym_eq. rewrite <- (Zeven_opp mu), <- (Zeven_opp md). change (Zeven (Fnum (Float beta (-md) ed)) = negb (Zeven (Fnum (Float beta (-mu) eu)))). rewrite <- (Z.even_opp mu), <- (Z.even_opp md). change (Z.even (Fnum (Float beta (-md) ed)) = negb (Z.even (Fnum (Float beta (-mu) eu)))). apply (Hpos (-x)%R _ _ Hx'). intros H. apply Hfx. ... ... @@ -97,7 +97,7 @@ now apply f_equal. Qed. Class Exists_NE := exists_NE : Zeven beta = false \/ forall e, exists_NE : Z.even beta = false \/ forall e, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e). Context { exists_NE_ : Exists_NE }. ... ... @@ -203,18 +203,18 @@ apply sym_eq. now apply mag_unique. rewrite Hd3, Hu3. unfold Fnum. rewrite Zeven_mult. simpl. rewrite Z.even_mul. simpl. unfold Zminus at 2. rewrite Zeven_plus. rewrite Z.even_add. rewrite eqb_sym. simpl. fold (negb (Zeven (beta ^ (ex - fexp ex)))). fold (negb (Z.even (beta ^ (ex - fexp ex)))). rewrite Bool.negb_involutive. rewrite (Zeven_Zpower beta (ex - fexp ex)). 2: omega. rewrite (Z.even_pow beta (ex - fexp ex)). 2: omega. destruct exists_NE_. rewrite H. apply Zeven_Zpower_odd with (2 := H). now apply Zle_minus_le_0. apply Zeven_Zpower. apply Z.even_pow. specialize (H ex). omega. (* - xu < bpow ex *) ... ... @@ -228,7 +228,7 @@ rewrite mag_unique with (1 := Hd4). rewrite mag_unique with (1 := Hexa). intros H. replace (Fnum xu) with (Fnum xd + 1)%Z. rewrite Zeven_plus. rewrite Z.even_add. now apply eqb_sym. apply sym_eq. apply eq_IZR. ... ... @@ -268,7 +268,7 @@ unfold generic_format. set (ed := cexp beta fexp d). set (md := Ztrunc (scaled_mantissa beta fexp d)). intros Hd1. case_eq (Zeven md) ; [ intros He | intros Ho ]. case_eq (Z.even md) ; [ intros He | intros Ho ]. right. exists (Float beta md ed). unfold Generic_fmt.canonical. ... ... @@ -358,9 +358,9 @@ unfold xr, round, Znearest. fold mx. rewrite Hm. rewrite Rcompare_Eq. 2: apply refl_equal. case_eq (Zeven (Zfloor mx)) ; intros Hmx. case_eq (Z.even (Zfloor mx)) ; intros Hmx. (* . even floor *) change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zfloor x))) = true). change (Z.even (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zfloor x))) = true). destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr]. rewrite (Rle_antisym _ _ Hr). unfold scaled_mantissa. ... ... @@ -372,7 +372,7 @@ now apply Rlt_le. rewrite scaled_mantissa_DN... now rewrite Ztrunc_IZR. (* . odd floor *) change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zceil x))) = true). change (Z.even (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zceil x))) = true). destruct (mag beta x) as (ex, Hex). specialize (Hex (Rgt_not_eq _ _ Hx)). rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx)) in Hex. ... ... @@ -399,23 +399,23 @@ rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. rewrite Ztrunc_IZR. fold mx. rewrite Hfc. now rewrite Zeven_plus, Hmx. now rewrite Z.even_add, Hmx. (* ... u = bpow *) rewrite Hu'. unfold scaled_mantissa, cexp. rewrite mag_bpow. rewrite <- bpow_plus, <- IZR_Zpower. rewrite Ztrunc_IZR. case_eq (Zeven beta) ; intros Hr. case_eq (Z.even beta) ; intros Hr. destruct exists_NE_ as [Hs|Hs]. now rewrite Hs in Hr. destruct (Hs ex) as (H,_). rewrite Zeven_Zpower. rewrite Z.even_pow. exact Hr. omega. assert (Zeven (Zfloor mx) = true). 2: now rewrite H in Hmx. assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. replace (Zfloor mx) with (Zceil mx + -1)%Z by omega. rewrite Zeven_plus. rewrite Z.even_add. apply eqb_true. unfold mx. replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower beta (ex - fexp ex)). ... ... @@ -435,7 +435,7 @@ apply bpow_gt_0. generalize (proj1 (valid_exp ex) He). omega. (* .. small pos *) assert (Zeven (Zfloor mx) = true). 2: now rewrite H in Hmx. assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. unfold mx, scaled_mantissa. rewrite cexp_fexp_pos with (1 := Hex). now rewrite mantissa_DN_small_pos. ... ... @@ -490,8 +490,8 @@ unfold Znearest. case Rcompare ; trivial. apply (f_equal (fun (b : bool) => if b then Zceil m else Zfloor m)). rewrite Bool.negb_involutive. rewrite Zeven_opp. rewrite Zeven_plus. rewrite Z.even_opp. rewrite Z.even_add. now rewrite eqb_sym. Qed. ... ... @@ -530,7 +530,7 @@ rewrite H1. now rewrite F2R_Zopp. now apply canonical_opp. simpl. now rewrite Zeven_opp. now rewrite Z.even_opp. rewrite <- round_NE_opp. apply round_NE_pt_pos. now apply Ropp_0_gt_lt_contravar. ... ...
 ... ... @@ -69,29 +69,8 @@ End Proof_Irrelevance. Section Even_Odd. (** Zeven, used for rounding to nearest, ties to even *) 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. forall x, exists p, x = (2 * p + if Z.even x then 0 else 1)%Z. Proof. intros [|[n|n|]|[n|n|]]. now exists Z0. ... ... @@ -105,37 +84,6 @@ 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 Zpower. ... ... @@ -181,40 +129,14 @@ rewrite Zpower_nat_S. now apply Zmult_lt_0_compat. Qed. Theorem Zeven_Zpower : forall b e, (0 < e)%Z -> Zeven (Zpower b e) = Zeven b. Proof. intros b e He. case_eq (Zeven b) ; intros Hb. (* b even *) replace e with (e - 1 + 1)%Z by ring. rewrite Zpower_exp. rewrite Zeven_mult. replace (Zeven (b ^ 1)) with true. apply Bool.orb_true_r. unfold Zpower, Zpower_pos. simpl. 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 Zeven_Zpower_odd : forall b e, (0 <= e)%Z -> Zeven b = false -> Zeven (Zpower b e) = false. forall b e, (0 <= e)%Z -> Z.even b = false -> Z.even (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 apply Z.even_pow. now rewrite <- He'. Qed. ... ...
 ... ... @@ -855,7 +855,7 @@ Definition round_mode m := Definition choice_mode m sx mx lx := match m with | mode_NE => cond_incr (round_N (negb (Zeven mx)) lx) mx | mode_NE => cond_incr (round_N (negb (Z.even mx)) lx) mx | mode_ZR => mx | mode_DN => cond_incr (round_sign_DN sx lx) mx | mode_UP => cond_incr (round_sign_UP sx lx) mx ... ... @@ -1747,7 +1747,7 @@ Definition Fsqrt_core_binary m e := let d := Zdigits2 m in let s := Zmax (2 * prec - d) 0 in let e' := (e - s)%Z in let (s', e'') := if Zeven e' then (s, e') else (s + 1, e' - 1)%Z in let (s', e'') := if Z.even e' then (s, e') else (s + 1, e' - 1)%Z in let m' := match s' with | Zpos p => Z.shiftl m (Zpos p) ... ... @@ -1871,7 +1871,7 @@ apply sqrt_ge_0. (* *) unfold Fsqrt_core, Fsqrt_core_binary. rewrite Zdigits2_Zdigits. destruct (if Zeven _ then _ else _) as [[|s'|s'] e''] ; try easy. destruct (if Z.even _ then _ else _) as [[|s'|s'] e''] ; try easy. now rewrite Z.shiftl_mul_pow2. Qed. ... ...
 ... ... @@ -25,7 +25,7 @@ Require Import Core Operations. Definition Zrnd_odd x := match Req_EM_T x (IZR (Zfloor x)) with | left _ => Zfloor x | right _ => match (Zeven (Zfloor x)) with | right _ => match (Z.even (Zfloor x)) with | true => Zceil x | false => Zfloor x end ... ... @@ -44,7 +44,7 @@ apply Zle_trans with (Zfloor y). now apply Zfloor_le. unfold Zrnd_odd; destruct (Req_EM_T y (IZR (Zfloor y))). now apply Zle_refl. case (Zeven (Zfloor y)). case (Z.even (Zfloor y)). apply le_IZR. apply Rle_trans with y. apply Zfloor_lb. ... ... @@ -56,12 +56,12 @@ destruct (Req_EM_T x (IZR (Zfloor x))) as [Hx|Hx]. (* .. *) apply H. (* .. *) case_eq (Zeven (Zfloor x)); intros Hx2. case_eq (Z.even (Zfloor x)); intros Hx2. 2: apply H. unfold Zrnd_odd; destruct (Req_EM_T y (IZR (Zfloor y))) as [Hy|Hy]. apply Zceil_glb. now rewrite <- Hy. case_eq (Zeven (Zfloor y)); intros Hy2. case_eq (Z.even (Zfloor y)); intros Hy2. now apply Zceil_le. apply Zceil_glb. assert (H0:(Zfloor x <= Zfloor y)%Z) by now apply Zfloor_le. ... ... @@ -76,22 +76,22 @@ rewrite <- H1, Hx2; discriminate. intros n; unfold Zrnd_odd. rewrite Zfloor_IZR, Zceil_IZR. destruct (Req_EM_T (IZR n) (IZR n)); trivial. case (Zeven n); trivial. case (Z.even n); trivial. Qed. Lemma Zrnd_odd_Zodd: forall x, x <> (IZR (Zfloor x)) -> (Zeven (Zrnd_odd x)) = false. (Z.even (Zrnd_odd x)) = false. Proof. intros x Hx; unfold Zrnd_odd. destruct (Req_EM_T x (IZR (Zfloor x))) as [H|H]. now contradict H. case_eq (Zeven (Zfloor x)). case_eq (Z.even (Zfloor x)). (* difficult case *) intros H'. rewrite Zceil_floor_neq. rewrite Zeven_plus, H'. rewrite Z.even_add, H'. reflexivity. now apply sym_not_eq. trivial. ... ... @@ -119,7 +119,7 @@ Notation cexp := (cexp beta fexp). Definition Rnd_odd_pt (x f : R) := format f /\ ((f = x)%R \/ ((Rnd_DN_pt format x f \/ Rnd_UP_pt format x f) /\ exists g : float beta, f = F2R g /\ canonical g /\ Zeven (Fnum g) = false)). exists g : float beta, f = F2R g /\ canonical g /\ Z.even (Fnum g) = false)). Definition Rnd_odd (rnd : R -> R) := forall x : R, Rnd_odd_pt x (rnd x). ... ... @@ -158,7 +158,7 @@ rewrite Hg1; reflexivity. split. now apply canonical_opp. simpl. now rewrite Zeven_opp. now rewrite Z.even_opp. Qed. ... ... @@ -193,14 +193,14 @@ rewrite <- opp_IZR, Zfloor_IZR. now rewrite opp_IZR, <- Y1. intros Y1 Y2. unfold Zceil; rewrite Ropp_involutive. replace (Zeven (Zfloor (- r))) with (negb (Zeven (Zfloor r))). case (Zeven (Zfloor r)); simpl; ring. apply trans_eq with (Zeven (Zceil r)). replace (Z.even (Zfloor (- r))) with (negb (Z.even (Zfloor r))). case (Z.even (Zfloor r)); simpl; ring. apply trans_eq with (Z.even (Zceil r)). rewrite Zceil_floor_neq. rewrite Zeven_plus. rewrite Z.even_add. simpl; reflexivity. now apply sym_not_eq. rewrite <- (Zeven_opp (Zfloor (- r))). rewrite <- (Z.even_opp (Zfloor (- r))). reflexivity. apply cexp_opp. Qed. ... ... @@ -259,7 +259,7 @@ apply Rmult_le_pos. now left. apply bpow_ge_0. intros L. case_eq (Zeven (Zfloor (scaled_mantissa beta fexp x))). case_eq (Z.even (Zfloor (scaled_mantissa beta fexp x))). (* . *) generalize (generic_format_round beta fexp Zceil x). unfold generic_format. ... ... @@ -270,9 +270,9 @@ exists (Float beta mf ef). unfold canonical.