...

Commits (2)
This diff is collapsed.
 ... ... @@ -4,16 +4,14 @@ Section Compute. Variable beta : radix. Variable fexp : Z -> Z. Context { valid_exp : Valid_exp fexp }. Variable fexp : Valid_exp. Variable prec : Z. Hypothesis Hprec : (0 < prec)%Z. Hypothesis fexp_prec : forall e, (e - prec <= fexp e)%Z. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Variable rnd : Valid_rnd. Variable choice : bool -> Z -> location -> Z. Hypothesis rnd_choice : ... ...
This diff is collapsed.
 ... ... @@ -29,7 +29,6 @@ Notation bpow e := (bpow beta e). Section Fcalc_round_fexp. Variable fexp : Z -> Z. Context { valid_exp : Valid_exp fexp }. Notation format := (generic_format beta fexp). (** Relates location and rounding. *) ... ... @@ -265,12 +264,12 @@ Theorem inbetween_int_ZR : forall x m l, inbetween_int m x l -> Ztrunc x = cond_incr (round_ZR (Zlt_bool m 0) l) m. Proof with auto with typeclass_instances. Proof. intros x m l Hl. inversion_clear Hl as [Hx|l' Hx Hl']. (* Exact *) rewrite Hx. rewrite Zrnd_Z2R... now rewrite Zrnd_Z2R. (* not Exact *) unfold Ztrunc. assert (Hm: Zfloor x = m). ... ... @@ -357,12 +356,12 @@ Theorem inbetween_int_N : forall choice x m l, inbetween_int m x l -> Znearest choice x = cond_incr (round_N (choice m) l) m. Proof with auto with typeclass_instances. Proof. intros choice x m l Hl. inversion_clear Hl as [Hx|l' Hx Hl']. (* Exact *) rewrite Hx. rewrite Zrnd_Z2R... now rewrite Zrnd_Z2R. (* not Exact *) unfold Znearest. assert (Hm: Zfloor x = m). ... ... @@ -386,7 +385,7 @@ Theorem inbetween_int_N_sign : forall choice x m l, inbetween_int m (Rabs x) l -> Znearest choice x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (if Rlt_bool x 0 then negb (choice (-(m + 1))%Z) else choice m) l) m). Proof with auto with typeclass_instances. Proof. intros choice x m l Hl. simpl. unfold Rabs in Hl. ... ... @@ -399,7 +398,7 @@ rewrite Znearest_opp. apply f_equal. inversion_clear Hl as [Hx|l' Hx Hl']. rewrite Hx. apply Zrnd_Z2R... apply Zrnd_Z2R. assert (Hm: Zfloor (-x) = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). ... ... @@ -423,7 +422,7 @@ rewrite Rlt_bool_false with (1 := Zx). simpl. inversion_clear Hl as [Hx|l' Hx Hl']. rewrite Hx. apply Zrnd_Z2R... apply Zrnd_Z2R. assert (Hm: Zfloor x = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). ... ... @@ -633,7 +632,7 @@ Theorem truncate_correct_format : x = F2R (Float beta m' e') /\ e' = cexp beta fexp x. Proof. intros m e Hm x Fx He. assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)). assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)%Z). unfold cexp, x. now rewrite mag_F2R_Zdigits. unfold truncate. ... ... @@ -671,6 +670,15 @@ unfold k in Hk. omega. Qed. End Fcalc_round_fexp. Section valid_exp. Variable fexp : Valid_exp. Notation format := (generic_format beta (Generic_fmt.fexp fexp)). Notation truncate := (truncate (Generic_fmt.fexp fexp)). Theorem truncate_correct_partial : forall x m e l, (0 < x)%R -> ... ... @@ -716,7 +724,7 @@ ring_simplify. rewrite <- Hm'. simpl. apply sym_eq. apply valid_exp. apply valid_exp3. exact H2. apply Zle_trans with e. eapply bpow_lt_bpow. ... ... @@ -751,7 +759,7 @@ Theorem truncate_correct : Proof. intros x m e l [Hx|Hx] H1 H2. (* 0 < x *) destruct (Zle_or_lt e (fexp (Zdigits beta m + e))) as [H3|H3]. destruct (Zle_or_lt e (fexp (Zdigits beta m + e)%Z)) as [H3|H3]. (* . enough digits *) generalize (truncate_correct_partial x m e l Hx H1 H3). destruct (truncate (m, e, l)) as ((m', e'), l'). ... ... @@ -765,7 +773,7 @@ elim (Zlt_irrefl e). now apply Zle_lt_trans with (1 := H2). rewrite H2 in H1 |- *. unfold truncate. generalize (Zlt_cases 0 (fexp (Zdigits beta m + e) - e)). generalize (Zlt_cases 0 (fexp (Zdigits beta m + e)%Z - e)). case Zlt_bool. intros H. apply False_ind. ... ... @@ -823,8 +831,7 @@ Qed. Section round_dir. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Variable rnd : Valid_rnd. Variable choice : Z -> location -> Z. Hypothesis inbetween_int_valid : ... ... @@ -837,7 +844,7 @@ Theorem round_any_correct : inbetween_float beta m e x l -> (e = cexp beta fexp x \/ (l = loc_Exact /\ format x)) -> round beta fexp rnd x = F2R (Float beta (choice m l) e). Proof with auto with typeclass_instances. Proof. intros x m e l Hin [He|(Hl,Hf)]. rewrite He in Hin |- *. apply inbetween_float_round with (2 := Hin). ... ... @@ -847,7 +854,7 @@ inversion_clear Hin. rewrite Hl. replace (choice m loc_Exact) with m. rewrite <- H. apply round_generic... now apply round_generic. rewrite <- (Zrnd_Z2R rnd m) at 1. apply inbetween_int_valid. now constructor. ... ... @@ -873,8 +880,7 @@ End round_dir. Section round_dir_sign. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Variable rnd : Valid_rnd. Variable choice : bool -> Z -> location -> Z. Hypothesis inbetween_int_valid : ... ... @@ -887,7 +893,7 @@ Theorem round_sign_any_correct : inbetween_float beta m e (Rabs x) l -> (e = cexp beta fexp x \/ (l = loc_Exact /\ format x)) -> round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e). Proof with auto with typeclass_instances. Proof. intros x m e l Hin [He|(Hl,Hf)]. rewrite He in Hin |- *. apply inbetween_float_round_sign with (2 := Hin). ... ... @@ -903,7 +909,7 @@ rewrite Rlt_bool_true with (1 := Zx). simpl. rewrite F2R_Zopp. rewrite <- H, Ropp_involutive. apply round_generic... now apply round_generic. rewrite Rlt_bool_false. simpl. rewrite <- H. ... ... @@ -1034,7 +1040,7 @@ Definition round_sign_NA_correct := Definition round_trunc_sign_NA_correct := round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_N true l) m) inbetween_int_NA_sign. End Fcalc_round_fexp. End valid_exp. (** Specialization of truncate for FIX formats. *) ... ...
 ... ... @@ -36,17 +36,33 @@ Definition FIX_exp (e : Z) := emin. (** Properties of the FIX format *) Global Instance FIX_exp_valid : Valid_exp FIX_exp. Lemma FIX_exp_valid1 : forall k : Z, (FIX_exp k < k)%Z -> (FIX_exp (k + 1) <= k)%Z. Proof. intros k. unfold FIX_exp. split ; intros H. intros k Hk. now apply Zlt_le_weak. split. Qed. Lemma FIX_exp_valid2 : forall k : Z, (k <= FIX_exp k)%Z -> (FIX_exp (FIX_exp k + 1) <= FIX_exp k)%Z. Proof. intros k Hk. apply Zle_refl. now intros _ _. Qed. Lemma FIX_exp_valid3 : forall k l : Z, (k <= FIX_exp k)%Z -> (l <= FIX_exp k)%Z -> FIX_exp l = FIX_exp k. Proof. now intros k l Hk Hl. Qed. Canonical Structure FIX_exp_valid := Build_Valid_exp FIX_exp FIX_exp_valid1 FIX_exp_valid2 FIX_exp_valid3. Theorem generic_format_FIX : forall x, FIX_format x -> generic_format beta FIX_exp x. Proof. ... ... @@ -66,14 +82,15 @@ Qed. Theorem FIX_format_satisfies_any : satisfies_any FIX_format. Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)). eapply satisfies_any_eq. intros x. split. apply FIX_format_generic. apply generic_format_FIX. apply generic_format_satisfies_any. Qed. Global Instance FIX_exp_monotone : Monotone_exp FIX_exp. Global Instance FIX_exp_monotone : Monotone_exp FIX_exp_valid. Proof. intros ex ey H. apply Zle_refl. ... ...
 ... ... @@ -27,9 +27,11 @@ Variable beta : radix. Notation bpow e := (bpow beta e). Variable emin prec : Z. Variable emin : Z. Context { prec_gt_0_ : Prec_gt_0 prec }. Section prec. Variable prec : Z. Inductive FLT_format (x : R) : Prop := FLT_spec (f : float beta) : ... ... @@ -39,20 +41,56 @@ Inductive FLT_format (x : R) : Prop := Definition FLT_exp e := Zmax (e - prec) emin. (** Properties of the FLT format *) Global Instance FLT_exp_valid : Valid_exp FLT_exp. Lemma FLT_exp_valid1 : forall k : Z, (FLT_exp k < k)%Z -> (FLT_exp (k + 1) <= k)%Z. Proof. intros k. unfold FLT_exp. zify ; omega. Qed. End prec. Section Prec_gt_0. Variable prec : Prec_gt_0. Local Notation FLT_exp' := FLT_exp (only parsing). Local Notation FLT_format' := FLT_format (only parsing). Notation FLT_exp := (FLT_exp prec). Notation FLT_format := (FLT_format prec). Lemma FLT_exp_valid2 : forall k : Z, (k <= FLT_exp k)%Z -> (FLT_exp (FLT_exp k + 1) <= FLT_exp k)%Z. Proof. intros k. unfold FLT_exp. generalize (prec_gt_0 prec). repeat split ; intros ; zify ; omega. zify ; omega. Qed. Lemma FLT_exp_valid3 : forall k l : Z, (k <= FLT_exp k)%Z -> (l <= FLT_exp k)%Z -> FLT_exp l = FLT_exp k. Proof. intros k l. unfold FLT_exp. generalize (prec_gt_0 prec). zify ; omega. Qed. Canonical Structure FLT_exp_valid := Build_Valid_exp FLT_exp (FLT_exp_valid1 prec) FLT_exp_valid2 FLT_exp_valid3. Theorem generic_format_FLT : forall x, FLT_format x -> generic_format beta FLT_exp x. forall prec x, FLT_format' prec x -> generic_format beta (FLT_exp' prec) x. Proof. clear prec_gt_0_. intros x [[mx ex] H1 H2 H3]. clear prec. intros prec x [[mx ex] H1 H2 H3]. simpl in H2, H3. rewrite H1. apply generic_format_F2R. ... ... @@ -76,7 +114,7 @@ intros Hx. rewrite Hx. eexists ; repeat split ; simpl. apply lt_Z2R. rewrite Z2R_Zpower. 2: now apply Zlt_le_weak. rewrite Z2R_Zpower. 2: apply Zlt_le_weak, prec_gt_0. apply Rmult_lt_reg_r with (bpow ex). apply bpow_gt_0. rewrite <- bpow_plus. ... ... @@ -98,27 +136,24 @@ apply Zle_max_l. apply Zle_max_r. Qed. Theorem FLT_format_bpow : forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e). Proof. intros e He. apply generic_format_bpow; unfold FLT_exp. apply Z.max_case; try assumption. unfold Prec_gt_0 in prec_gt_0_; omega. generalize (prec_gt_0 prec) ; omega. Qed. Theorem FLT_format_satisfies_any : satisfies_any FLT_format. Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)). eapply satisfies_any_eq. intros x. split. apply FLT_format_generic. apply generic_format_FLT. apply generic_format_satisfies_any. Qed. Theorem cexp_FLT_FLX : ... ... @@ -157,11 +192,11 @@ now rewrite cexp_FLT_FLX. Qed. Theorem generic_format_FLX_FLT : forall x : R, generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x. forall (prec : Z) (x : R), generic_format beta (FLT_exp' prec) x -> generic_format beta (FLX_exp prec) x. Proof. clear prec_gt_0_. intros x Hx. clear prec. intros prec x Hx. unfold generic_format in Hx; rewrite Hx. apply generic_format_F2R. intros _. ... ... @@ -198,12 +233,12 @@ now apply Hex. Qed. Theorem generic_format_FIX_FLT : forall x : R, generic_format beta FLT_exp x -> forall (prec : Z) (x : R), generic_format beta (FLT_exp' prec) x -> generic_format beta (FIX_exp emin) x. Proof. clear prec_gt_0_. intros x Hx. clear prec. intros prec x Hx. rewrite Hx. apply generic_format_F2R. intros _. ... ... @@ -216,18 +251,20 @@ Theorem generic_format_FLT_FIX : (Rabs x <= bpow (emin + prec))%R -> generic_format beta (FIX_exp emin) x -> generic_format beta FLT_exp x. Proof with auto with typeclass_instances. apply generic_inclusion_le... Proof. apply generic_inclusion_le. intros e He. simpl. unfold FIX_exp. apply Zmax_lub. omega. apply Zle_refl. Qed. Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R -> ulp beta FLT_exp x = bpow emin. Proof with auto with typeclass_instances. Theorem ulp_FLT_small : forall x : R, (Rabs x < bpow (emin+prec))%R -> ulp beta FLT_exp x = bpow emin. Proof. intros x Hx. unfold ulp; case Req_bool_spec; intros Hx2. (* x = 0 *) ... ... @@ -237,10 +274,12 @@ apply Zle_not_lt; unfold FLT_exp. apply Zle_trans with (2:=Z.le_max_r _ _); omega. assert (V:FLT_exp emin = emin). unfold FLT_exp; apply Z.max_r. unfold Prec_gt_0 in prec_gt_0_; omega. generalize (prec_gt_0 prec) ; omega. intros n H2; rewrite <-V. apply f_equal, fexp_negligible_exp_eq... omega. apply f_equal, fexp_negligible_exp_eq. exact H2. simpl. now rewrite V. (* x <> 0 *) apply f_equal; unfold cexp, FLT_exp. apply Z.max_r. ... ... @@ -293,12 +332,11 @@ apply bpow_le. apply Z.le_max_l. Qed. (** FLT is a nice format: it has a monotone exponent... *) Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. Global Instance FLT_exp_monotone : Monotone_exp FLT_exp_valid. Proof. intros ex ey. simpl. unfold FLT_exp. zify ; omega. Qed. ... ... @@ -306,12 +344,13 @@ Qed. (** and it allows a rounding to nearest, ties to even. *) Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z. Global Instance exists_NE_FLT : Exists_NE beta FLT_exp. Global Instance exists_NE_FLT : Exists_NE beta FLT_exp_valid. Proof. destruct NE_prop as [H|H]. now left. right. intros e. simpl. unfold FLT_exp. destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ; rewrite H2 ; clear H2. ... ... @@ -323,4 +362,6 @@ generalize (Zmax_spec (emin + 1 - prec) emin). omega. Qed. End Prec_gt_0. End RND_FLT.
 ... ... @@ -21,43 +21,88 @@ COPYING file for more details. Require Import Raux Definitions Round_pred Generic_fmt Float_prop. Require Import FIX Ulp Round_NE. Record Prec_gt_0 := { prec :> Z ; prec_gt_0 : (0 < prec)%Z }. Section RND_FLX. Variable beta : radix. Notation bpow e := (bpow beta e). Variable prec : Z. Class Prec_gt_0 := prec_gt_0 : (0 < prec)%Z. Section prec. Context { prec_gt_0_ : Prec_gt_0 }. Variable prec : Z. Inductive FLX_format (x : R) : Prop := FLX_spec (f : float beta) : x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z -> FLX_format x. (** unbounded floating-point format with normal mantissas *) Inductive FLXN_format (x : R) : Prop := FLXN_spec (f : float beta) : x = F2R f -> (x <> 0%R -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z -> FLXN_format x. Definition FLX_exp (e : Z) := (e - prec)%Z. (** Properties of the FLX format *) Global Instance FLX_exp_valid : Valid_exp FLX_exp. Lemma FLX_exp_valid1 : forall k : Z, (FLX_exp k < k)%Z -> (FLX_exp (k + 1) <= k)%Z. Proof. intros k. unfold FLX_exp. omega. Qed. End prec. Section Prec_gt_0. Variable prec : Prec_gt_0. Local Notation FLX_exp' := FLX_exp (only parsing). Local Notation FLX_format' := FLX_format (only parsing). Notation FLX_exp := (FLX_exp prec). Notation FLX_format := (FLX_format prec). Lemma FLX_exp_valid2 : forall k : Z, (k <= FLX_exp k)%Z -> (FLX_exp (FLX_exp k + 1) <= FLX_exp k)%Z. Proof. intros k. unfold FLX_exp. generalize prec_gt_0. repeat split ; intros ; omega. generalize (prec_gt_0 prec). omega. Qed. Lemma FLX_exp_valid3 : forall k l : Z, (k <= FLX_exp k)%Z -> (l <= FLX_exp k)%Z -> FLX_exp l = FLX_exp k. Proof. intros k l. unfold FLX_exp. generalize (prec_gt_0 prec). omega. Qed. Canonical Structure FLX_exp_valid := Build_Valid_exp FLX_exp (FLX_exp_valid1 prec) FLX_exp_valid2 FLX_exp_valid3. Theorem FIX_format_FLX : forall x e, forall (prec : Z) x e, (bpow (e - 1) <= Rabs x <= bpow e)%R -> FLX_format x -> FLX_format' prec x -> FIX_format beta (e - prec) x. Proof. clear prec_gt_0_. intros x e Hx [[xm xe] H1 H2]. clear prec. intros prec x e Hx [[xm xe] H1 H2]. rewrite H1, (F2R_prec_normalize beta xm xe e prec). now eexists. exact H2. ... ... @@ -79,7 +124,7 @@ apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp (Rabs x))). apply bpow_gt_0. rewrite scaled_mantissa_mult_bpow. rewrite Z2R_Zpower, <- bpow_plus. 2: now apply Zlt_le_weak. 2: apply Zlt_le_weak, prec_gt_0. unfold cexp, FLX_exp. ring_simplify (prec + (mag beta (Rabs x) - prec))%Z. rewrite mag_abs. ... ... @@ -91,10 +136,10 @@ now apply Ex. Qed. Theorem generic_format_FLX : forall x, FLX_format x -> generic_format beta FLX_exp x. forall prec x, FLX_format' prec x -> generic_format beta (FLX_exp' prec) x. Proof. clear prec_gt_0_. intros x [[mx ex] H1 H2]. clear prec. intros prec x [[mx ex] H1 H2]. simpl in H2. rewrite H1. apply generic_format_F2R. ... ... @@ -109,11 +154,12 @@ Qed. Theorem FLX_format_satisfies_any : satisfies_any FLX_format. Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). eapply satisfies_any_eq. intros x. split. apply FLX_format_generic. apply generic_format_FLX. apply generic_format_satisfies_any. Qed. Theorem FLX_format_FIX : ... ... @@ -121,26 +167,20 @@ Theorem FLX_format_FIX : (bpow (e - 1) <= Rabs x <= bpow e)%R -> FIX_format beta (e - prec) x -> FLX_format x. Proof with auto with typeclass_instances. Proof. intros x e Hx Fx. apply FLX_format_generic. apply generic_format_FIX in Fx. revert Fx. apply generic_inclusion with (e := e)... apply generic_inclusion with (2 := Hx). apply Zle_refl. Qed. (** unbounded floating-point format with normal mantissas *) Inductive FLXN_format (x : R) : Prop := FLXN_spec (f : float beta) : x = F2R f -> (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z -> FLXN_format x. Theorem generic_format_FLXN : forall x, FLXN_format x -> generic_format beta FLX_exp x. forall prec x, FLXN_format prec x -> generic_format beta (FLX_exp' prec) x. Proof. intros x [[xm ex] H1 H2]. clear prec. intros prec x [[xm ex] H1 H2]. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx. apply generic_format_0. ... ... @@ -152,7 +192,7 @@ apply H2. Qed. Theorem FLXN_format_generic : forall x, generic_format beta FLX_exp x -> FLXN_format x. forall x, generic_format beta FLX_exp x -> FLXN_format prec x. Proof. intros x Hx. rewrite Hx. ... ... @@ -165,7 +205,7 @@ split. (* *) apply le_Z2R. rewrite Z2R_Zpower. 2: now apply Zlt_0_le_0_pred. 2: apply Zlt_0_le_0_pred, prec_gt_0. rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx). apply Rmult_le_reg_r with (bpow (cexp beta FLX_exp x)). apply bpow_gt_0. ... ... @@ -181,7 +221,7 @@ now apply Ex. (* *) apply lt_Z2R. rewrite Z2R_Zpower. 2: now apply Zlt_le_weak. 2: apply Zlt_le_weak, prec_gt_0. rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx). apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp x)). apply bpow_gt_0. ... ... @@ -197,21 +237,23 @@ now apply Ex. Qed. Theorem FLXN_format_satisfies_any : satisfies_any FLXN_format. satisfies_any (FLXN_format prec). Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). split ; intros H. now apply FLXN_format_generic. now apply generic_format_FLXN. eapply satisfies_any_eq. split. apply FLXN_format_generic. apply generic_format_FLXN. apply generic_format_satisfies_any. Qed. Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. Theorem ulp_FLX_0: ulp beta FLX_exp 0 = 0%R. Proof. unfold ulp; rewrite Req_bool_true; trivial. case (negligible_exp_spec FLX_exp). intros _; reflexivity. intros n H2; contradict H2. unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. unfold FLX_exp. generalize (prec_gt_0 prec); omega. Qed. Theorem ulp_FLX_le : ... ... @@ -244,7 +286,7 @@ left; now apply bpow_mag_gt. Qed. (** FLX is a nice format: it has a monotone exponent... *) Global Instance FLX_exp_monotone : Monotone_exp FLX_exp. Global Instance FLX_exp_monotone : Monotone_exp FLX_exp_valid. Proof. intros ex ey Hxy. now apply Zplus_le_compat_r. ... ... @@ -253,13 +295,16 @@ Qed. (** and it allows a rounding to nearest, ties to even. *) Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z. Global Instance exists_NE_FLX : Exists_NE beta FLX_exp. Global Instance exists_NE_FLX : Exists_NE beta FLX_exp_valid. Proof. destruct NE_prop as [H|H]. now left. right. simpl. unfold FLX_exp. split ; omega. Qed. End Prec_gt_0. End RND_FLX.
 ... ... @@ -27,9 +27,11 @@ Variable beta : radix. Notation bpow e := (bpow beta e). Variable emin prec : Z. Variable emin : Z. Context { prec_gt_0_ : Prec_gt_0 prec }. Section prec. Variable prec : Z. Inductive FTZ_format (x : R) : Prop := FTZ_spec (f : float beta) : ... ... @@ -41,44 +43,82 @@ Inductive FTZ_format (x : R) : Prop := Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z. (** Properties of the FTZ format *) Global Instance FTZ_exp_valid : Valid_exp FTZ_exp. Lemma FTZ_exp_valid1 : forall k : Z, (FTZ_exp k < k)%Z -> (FTZ_exp (k + 1) <= k)%Z. Proof. intros k. unfold FTZ_exp. generalize (Zlt_cases (k - prec) emin). case (Zlt_bool (k - prec) emin) ; intros H1. split ; intros H2. omega. split. intros H2. generalize (Zlt_cases (emin + prec + 1 - prec) emin). case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3. omega. generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin). generalize (Zlt_cases (k + 1 - prec) emin). case (Zlt_bool (k + 1 - prec) emin) ; omega. Qed. End prec. Section Prec_gt_0. Variable prec : Prec_gt_0. Local Notation FTZ_exp' := FTZ_exp (only parsing). Local Notation FTZ_format' := FTZ_format (only parsing). Notation FTZ_exp := (FTZ_exp prec). Notation FTZ_format := (FTZ_format prec). Lemma FTZ_exp_valid2 : forall k : Z, (k <= FTZ_exp k)%Z -> (FTZ_exp (FTZ_exp k + 1) <= FTZ_exp k)%Z. Proof. intros k. unfold FTZ_exp. generalize (Zlt_cases (k - prec) emin). generalize (prec_gt_0 prec). case (Zlt_bool (k - prec) emin) ; intros H1 H2. generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin). case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega. intros l H3. omega. Qed. Lemma FTZ_exp_valid3 : forall k l : Z, (k <= FTZ_exp k)%Z -> (l <= FTZ_exp k)%Z -> FTZ_exp l = FTZ_exp k. Proof. intros k l. unfold FTZ_exp. generalize (Zlt_cases (k - prec) emin). case (Zlt_bool (k - prec) emin) ; intros H1 H2 H3. generalize (Zlt_cases (l - prec) emin). case (Zlt_bool (l - prec) emin) ; omega. split ; intros H2. generalize (Zlt_cases (k + 1 - prec) emin). case (Zlt_bool (k + 1 - prec) emin) ; omega. generalize (prec_gt_0 prec). split ; intros ; omega. omega. Qed. Canonical Structure FTZ_exp_valid := Build_Valid_exp FTZ_exp (FTZ_exp_valid1 prec) FTZ_exp_valid2 FTZ_exp_valid3. Theorem FLXN_format_FTZ : forall x, FTZ_format x -> FLXN_format beta prec x. forall prec x, FTZ_format' prec x -> FLXN_format beta prec x. Proof. intros x [[xm xe] Hx1 Hx2 Hx3]. clear prec. intros prec x [[xm xe] Hx1 Hx2 Hx3]. eexists. exact Hx1. exact Hx2. Qed. Theorem generic_format_FTZ : forall x, FTZ_format x -> generic_format beta FTZ_exp x. forall prec x, FTZ_format' prec x -> generic_format beta (FTZ_exp' prec) x. Proof. intros x Hx. clear prec. intros prec x Hx. cut (generic_format beta (FLX_exp prec) x). apply generic_inclusion_mag. intros Zx. ... ... @@ -89,6 +129,7 @@ assert (Zxm: xm <> Z0). contradict Zx. rewrite Hx1, Zx. apply F2R_0. simpl. unfold FTZ_exp, FLX_exp. rewrite Zlt_bool_false. apply Zle_refl. ... ... @@ -148,7 +189,7 @@ change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec)) rewrite F2R_Zabs, <- Hx2. apply Hx4. apply Zle_minus_le_0. now apply (Zlt_le_succ 0). apply (Zlt_le_succ 0), prec. apply lt_Z2R. rewrite Z2R_Zpower. apply Rmult_lt_reg_r with (bpow (ex - prec)). ... ... @@ -158,18 +199,19 @@ replace (prec + (ex - prec))%Z with ex by ring. change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R. rewrite F2R_Zabs, <- Hx2. apply Hx4. now apply Zlt_le_weak. apply Zlt_le_weak, prec. now apply Zge_le. Qed. Theorem FTZ_format_satisfies_any : satisfies_any FTZ_format. Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp)). eapply satisfies_any_eq. intros x. split. apply FTZ_format_generic. apply generic_format_FTZ. apply generic_format_satisfies_any. Qed. Theorem FTZ_format_FLXN : ... ... @@ -183,40 +225,42 @@ apply generic_format_FLXN in Fx. revert Hx Fx. apply generic_inclusion_ge. intros e He. unfold FTZ_exp. simpl. unfold FTZ_exp. rewrite Zlt_bool_false. apply Zle_refl. omega. Qed. Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1). Proof with auto with typeclass_instances. Theorem ulp_FTZ_0 : ulp beta FTZ_exp 0 = bpow (emin+prec-1). Proof. unfold ulp; rewrite Req_bool_true; trivial. case (negligible_exp_spec FTZ_exp). intros T; specialize (T (emin-1)%Z); contradict T. apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_. apply Zle_not_lt; unfold FTZ_exp. assert (H := prec_gt_0 prec). rewrite Zlt_bool_true; omega. assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z). unfold FTZ_exp; rewrite Zlt_bool_true; omega. intros n H2; rewrite <-V. apply f_equal, fexp_negligible_exp_eq... omega. apply f_equal, fexp_negligible_exp_eq with (1 := H2). simpl. now rewrite V. Qed. Section FTZ_round. (** Rounding with FTZ *) Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Variable rnd : Valid_rnd. Definition Zrnd_FTZ x := if Rle_bool 1 (Rabs x) then rnd x else Z0. Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ. Proof with auto with typeclass_instances. split. (* *) Lemma Zrnd_FTZ_le : forall x y, (x <= y)%R -> (Zrnd_FTZ x <= Zrnd_FTZ y)%Z. Proof. intros x y Hxy. unfold Zrnd_FTZ. case Rle_bool_spec ; intros Hx ; ... ... @@ -235,7 +279,7 @@ apply Rle_trans with (1 := Hxy). apply RRle_abs. (* |x| < 1 *) rewrite <- (Zrnd_Z2R rnd 0). apply Zrnd_le... apply Zrnd_le. apply Rle_trans with (Z2R 1). now apply Z2R_le. destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1]. ... ... @@ -243,10 +287,14 @@ elim Rle_not_lt with (1 := Hy1). apply Rlt_le_trans with (2 := Hxy). apply (Rabs_def2 _ _ Hx). exact Hy1. (* *) Qed. Lemma Zrnd_FTZ_Z2R : forall x, Zrnd_FTZ (Z2R x) = x. Proof. intros n. unfold Zrnd_FTZ. rewrite Zrnd_Z2R... rewrite Zrnd_Z2R. case Rle_bool_spec. easy. rewrite <- Z2R_abs. ... ... @@ -256,6 +304,9 @@ clear. now case n ; trivial ; simpl ; intros [p|p|]. Qed. Canonical Structure valid_rnd_FTZ := Build_Valid_rnd Zrnd_FTZ Zrnd_FTZ_le Zrnd_FTZ_Z2R. Theorem round_FTZ_FLX : forall x : R, (bpow (emin + prec - 1) <= Rabs x)%R -> ... ... @@ -301,11 +352,11 @@ Theorem round_FTZ_small : forall x : R, (Rabs x < bpow (emin + prec - 1))%R -> round beta FTZ_exp Zrnd_FTZ x = R0. Proof with auto with typeclass_instances. Proof. intros x Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0. apply round_0... apply round_0. unfold round, scaled_mantissa, cexp. destruct (mag beta x) as (ex, He). simpl. specialize (He Hx0). ... ... @@ -336,4 +387,6 @@ Qed. End FTZ_round. End Prec_gt_0. End RND_FTZ.
This diff is collapsed.
 ... ... @@ -20,7 +20,8 @@ COPYING file for more details. (** * Rounding to nearest, ties to even: existence, unicity... *) Require Import Raux Definitions Round_pred Generic_fmt Float_prop Ulp. Notation ZnearestE := (Znearest (fun x => negb (Zeven x))). Definition choiceNE x := negb (Zeven x). Notation ZnearestE := (Znearest choiceNE). Section Fcore_rnd_NE. ... ... @@ -28,9 +29,7 @@ Variable beta : radix. Notation bpow e := (bpow beta e). Variable fexp : Z -> Z. Context { valid_exp : Valid_exp fexp }. Variable fexp : Valid_exp. Notation format := (generic_format beta fexp). Notation canonical := (canonical beta fexp). ... ... @@ -98,13 +97,13 @@ Qed. Class Exists_NE := exists_NE : Zeven beta = false \/ forall e, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e). (fexp e < e -> fexp (e + 1) < e)%Z /\ (e <= fexp e -> fexp (fexp e + 1) = fexp e)%Z. Context { exists_NE_ : Exists_NE }. Theorem DN_UP_parity_generic_pos : DN_UP_parity_pos_prop. Proof with auto with typeclass_instances. Proof. intros x xd xu H0x Hfx Hd Hu Hxd Hxu. destruct (mag beta x) as (ex, Hexa). specialize (Hexa (Rgt_not_eq _ _ H0x)). ... ... @@ -117,26 +116,26 @@ apply F2R_eq_0_reg with beta (Fexp xd). change (F2R xd = R0). rewrite Hxd. apply round_DN_small_pos with (1 := Hex) (2 := Hxe). assert (Hu3 : xu = Float beta (1 * Zpower beta (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))). assert (Hu3 : xu = Float beta (1 * Zpower beta (fexp ex - fexp (fexp ex + 1)%Z)) (fexp (fexp ex + 1)%Z)). apply canonical_unicity with (1 := Hu). apply (f_equal fexp). rewrite <- F2R_change_exp. now rewrite F2R_bpow, mag_bpow. now apply valid_exp. now apply valid_exp2. rewrite <- F2R_change_exp. rewrite F2R_bpow. apply sym_eq. rewrite Hxu. apply sym_eq. apply round_UP_small_pos with (1 := Hex) (2 := Hxe). now apply valid_exp. now apply valid_exp2. rewrite Hd3, Hu3. rewrite Zmult_1_l. simpl. destruct exists_NE_ as [H|H]. apply Zeven_Zpower_odd with (2 := H). apply Zle_minus_le_0. now apply valid_exp. now apply valid_exp2. rewrite (proj2 (H ex)). now rewrite Zminus_diag. exact Hxe. ... ... @@ -156,7 +155,7 @@ rewrite Hxd. apply (round_DN_pt beta fexp x). apply generic_format_0. now apply Rlt_le. assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp. assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp1. assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R). rewrite Hxu, Hxd. now apply round_UP_DN_ulp. ... ... @@ -164,14 +163,14 @@ destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2]. (* - xu > bpow ex *) elim (Rlt_not_le _ _ Hu2). rewrite Hxu. apply round_bounded_large_pos... now apply round_bounded_large_pos. (* - xu = bpow ex *) assert (Hu3: xu = Float beta (1 * Zpower beta (ex - fexp (ex + 1))) (fexp (ex + 1))). assert (Hu3: xu = Float beta (1 * Zpower beta (ex - fexp (ex + 1)%Z)) (fexp (ex + 1)%Z)). apply canonical_unicity with (1 := Hu). apply (f_equal fexp). rewrite <- F2R_change_exp. now rewrite F2R_bpow, mag_bpow. now apply valid_exp. now apply valid_exp1. rewrite <- Hu2. apply sym_eq. rewrite <- F2R_change_exp. ... ... @@ -336,7 +335,7 @@ Lemma round_NE_pt_pos : forall x, (0 < x)%R -> Rnd_NE_pt x (round beta fexp ZnearestE x). Proof with auto with typeclass_instances. Proof. intros x Hx. split. now apply round_N_pt. ... ... @@ -348,16 +347,17 @@ destruct (Req_dec (mx - Z2R (Zfloor mx)) (/2)) as [Hm|Hm]. left. exists (Float beta (Ztrunc (scaled_mantissa beta fexp xr)) (cexp beta fexp xr)). split. apply round_N_pt... apply round_N_pt. split. unfold Generic_fmt.canonical. simpl. apply f_equal. apply round_N_pt... apply round_N_pt. simpl. unfold xr, round, Znearest. fold mx. rewrite Hm. rewrite Rcompare_Eq. 2: apply refl_equal. unfold choiceNE. case_eq (Zeven (Zfloor mx)) ; intros Hmx. (* . even floor *) change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zfloor x))) = true). ... ... @@ -367,10 +367,10 @@ unfold scaled_mantissa. rewrite Rmult_0_l. change 0%R with (Z2R 0). now rewrite (Ztrunc_Z2R 0). rewrite <- (round_0 beta fexp Zfloor). apply round_le... rewrite <- (round_0 beta fexp [>> Zrnd Zfloor]). apply round_le. now apply Rlt_le. rewrite scaled_mantissa_DN... rewrite scaled_mantissa_DN with (1 := Hr). now rewrite Ztrunc_Z2R. (* . odd floor *) change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zceil x))) = true). ... ... @@ -379,7 +379,8 @@ specialize (Hex (Rgt_not_eq _ _ Hx)). rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx)) in Hex. destruct (Z_lt_le_dec (fexp ex) ex) as [He|He]. (* .. large pos *) assert (Hu := round_bounded_large_pos _ _ Zceil _ _ He Hex). assert (Hu := round_bounded_large_pos _ _ [>> Zrnd Zceil] _ _ He Hex). simpl Zrnd in Hu. assert (Hfc: Zceil mx = (Zfloor mx + 1)%Z). apply Zceil_floor_neq. intros H. ... ... @@ -433,7 +434,7 @@ pattern (fexp ex) ; rewrite <- cexp_fexp_pos with (1 := Hex). now apply sym_eq. apply Rgt_not_eq. apply bpow_gt_0. generalize (proj1 (valid_exp ex) He). generalize (valid_exp1 fexp ex He). omega. (* .. small pos *) assert (Zeven (Zfloor mx) = true). 2: now rewrite H in Hmx. ... ... @@ -446,7 +447,7 @@ intros g Hg. destruct (Req_dec x g) as [Hxg|Hxg]. rewrite <- Hxg. apply sym_eq. apply round_generic... apply round_generic. rewrite Hxg. apply Hg. set (d := round beta fexp Zfloor x). ... ... @@ -481,7 +482,7 @@ Theorem round_NE_opp : round beta fexp ZnearestE (-x) = (- round beta fexp ZnearestE x)%R. Proof. intros x. unfold round. simpl. unfold round. rewrite scaled_mantissa_opp, cexp_opp. rewrite Znearest_opp. rewrite <- F2R_Zopp. ... ... @@ -490,6 +491,7 @@ set (m := scaled_mantissa beta fexp x). unfold Znearest. case Rcompare ; trivial. apply (f_equal (fun (b : bool) => if b then Zceil m else Zfloor m)). unfold choiceNE. rewrite Bool.negb_involutive. rewrite Zeven_opp. rewrite Zeven_plus. ... ... @@ -499,26 +501,27 @@ Qed. Lemma round_NE_abs: forall x : R, round beta fexp ZnearestE (Rabs x) = Rabs (round beta fexp ZnearestE x). Proof with auto with typeclass_instances. Proof. intros x. apply sym_eq. unfold Rabs at 2. assert (H0: round beta fexp ZnearestE 0 = 0%R) by apply round_0. destruct (Rcase_abs x) as [Hx|Hx]. rewrite round_NE_opp. apply Rabs_left1. rewrite <- (round_0 beta fexp ZnearestE). apply round_le... rewrite <- H0. apply round_le. now apply Rlt_le. apply Rabs_pos_eq. rewrite <- (round_0 beta fexp ZnearestE). apply round_le... rewrite <- H0. apply round_le. now apply Rge_le. Qed. Theorem round_NE_pt : forall x, Rnd_NE_pt x (round beta fexp ZnearestE x). Proof with auto with typeclass_instances. Proof. intros x. destruct (total_order_T x 0) as [[Hx|Hx]|Hx]. apply Rnd_NG_pt_sym. ... ... @@ -535,7 +538,7 @@ now rewrite Zeven_opp. rewrite <- round_NE_opp. apply round_NE_pt_pos. now apply Ropp_0_gt_lt_contravar. rewrite Hx, round_0... rewrite Hx, round_0. apply Rnd_NG_pt_refl. apply generic_format_0. now apply round_NE_pt_pos. ... ...
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -26,8 +26,7 @@ Section Fprop_Sterbenz. Variable beta : radix. Notation bpow e := (bpow beta e). Variable fexp : Z -> Z. Context { valid_exp : Valid_exp fexp }. Variable fexp : Valid_exp. Context { monotone_exp : Monotone_exp fexp }. Notation format := (generic_format beta fexp). ... ...