Commit b4baed0a by Guillaume Melquiond

### Split FLX_format_* equivalence theorems into separate implications.

parent a703b4fe
 ... ... @@ -170,11 +170,11 @@ Proof. intros x Hx1. apply iff_trans with (1 := FLT_format_generic x). apply iff_trans with (1 := FLT_generic_format_FLX x Hx1). apply iff_sym. split. now apply FLX_format_generic. now apply generic_format_FLX. Qed. Theorem FLT_round_FLX : forall rnd x, (bpow (emin + prec - 1) <= Rabs x)%R -> round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x. ... ...
 ... ... @@ -56,25 +56,31 @@ generalize prec_gt_0. repeat split ; intros ; omega. Qed. Theorem FLX_format_FIX : Theorem FIX_format_FLX : forall x e, (bpow (e - 1) <= Rabs x <= bpow e)%R -> ( FLX_format x <-> FIX_format beta (e - prec) x ). FLX_format x -> FIX_format beta (e - prec) x. Proof. intros x e Hx. split. (* . *) intros ((xm, xe), (H1, H2)). intros x e Hx ((xm, xe), (H1, H2)). rewrite H1, (F2R_prec_normalize beta xm xe e prec). now eexists. exact H2. now rewrite <- H1. Qed. Theorem FLX_format_FIX : forall x e, (bpow (e - 1) <= Rabs x <= bpow e)%R -> FIX_format beta (e - prec) x -> FLX_format x. Proof. intros x e (Hx1,[Hx2|Hx2]). (* . *) destruct Hx as (Hx1,[Hx2|Hx2]). (* . . *) intros ((xm, xe), (H1, H2)). rewrite H1. eexists ; repeat split. simpl. apply lt_Z2R. apply Rmult_lt_reg_r with (bpow (e - prec)). apply bpow_gt_0. ... ... @@ -85,7 +91,7 @@ simpl. change (F2R (Float beta (Zabs xm) xe) < bpow e)%R. now rewrite <- abs_F2R, <- H1. now apply Zlt_le_weak. (* . . *) (* . *) intros ((xm, xe), (H1, H2)). assert (Ha: forall x, FLX_format (Rabs x) -> FLX_format x). clear. ... ... @@ -110,33 +116,53 @@ now apply Zpower_gt_1. Qed. Theorem FLX_format_generic : forall x : R, FLX_format x <-> generic_format beta FLX_exp x. forall x, generic_format beta FLX_exp x -> FLX_format x. Proof. intros x. destruct (Req_dec x 0) as [Hx|Hx1]. (* . *) split ; intros H ; rewrite Hx. intros x H. rewrite H. unfold FLX_format. eexists ; repeat split. simpl. apply lt_Z2R. rewrite Z2R_abs. rewrite <- scaled_mantissa_generic with (1 := H). rewrite <- scaled_mantissa_abs. apply Rmult_lt_reg_r with (bpow (canonic_exponent beta FLX_exp (Rabs x))). apply bpow_gt_0. rewrite scaled_mantissa_bpow. rewrite Z2R_Zpower, <- bpow_plus. 2: now apply Zlt_le_weak. unfold canonic_exponent, FLX_exp. ring_simplify (prec + (ln_beta beta (Rabs x) - prec))%Z. rewrite ln_beta_abs. destruct (Req_dec x 0) as [Hx|Hx]. rewrite Hx, Rabs_R0. apply bpow_gt_0. destruct (ln_beta beta x) as (ex, Ex). now apply Ex. Qed. Theorem generic_format_FLX : forall x, FLX_format x -> generic_format beta FLX_exp x. Proof. intros x ((mx,ex),(H1,H2)). rewrite H1. destruct (Z_eq_dec mx 0) as [Zmx|Zmx]. rewrite Zmx, F2R_0. apply generic_format_0. exists (Float beta 0 0). split. now rewrite F2R_0. apply Zpower_gt_0. apply generic_format_canonic_exponent. unfold canonic_exponent, FLX_exp. rewrite ln_beta_F2R with (1 := Zmx). apply Zplus_le_reg_r with (prec - ex)%Z. ring_simplify. apply bpow_lt_bpow with beta. destruct (ln_beta beta (Z2R mx)) as (emx,Emx). simpl. specialize (Emx (Z2R_neq _ _ Zmx)). apply Rle_lt_trans with (1 := proj1 Emx). rewrite <- Z2R_abs. rewrite <- Z2R_Zpower. now apply Z2R_lt. now apply Zlt_le_weak. (* . *) destruct (ln_beta beta x) as (ex, Hx2). simpl. specialize (Hx2 Hx1). apply iff_trans with (generic_format beta (FIX_exp (ex - prec)) x). apply iff_trans with (FIX_format beta (ex - prec) x). apply FLX_format_FIX. exact (conj (proj1 Hx2) (Rlt_le _ _ (proj2 Hx2))). apply FIX_format_generic. assert (Hf: FLX_exp (ln_beta beta x) = FIX_exp (ex - prec) (ln_beta beta x)). unfold FIX_exp, FLX_exp. now rewrite ln_beta_unique with (1 := Hx2). split ; unfold generic_format, scaled_mantissa, canonic_exponent ; now rewrite Hf. Qed. Theorem FLX_format_satisfies_any : ... ... @@ -144,8 +170,9 @@ Theorem FLX_format_satisfies_any : Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). intros x. apply iff_sym. split. apply FLX_format_generic. apply generic_format_FLX. Qed. (** unbounded floating-point format with normal mantissas *) ... ... @@ -222,7 +249,7 @@ exact H5. intros ((xm, xe), (H1, H2)). destruct (Req_dec x 0) as [H3|H3]. rewrite H3. apply <- FLX_format_generic. apply FLX_format_generic. apply generic_format_0. specialize (H2 H3). clear H3. rewrite H1. ... ... @@ -236,8 +263,8 @@ Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). split ; intros H. apply -> FLX_format_FLXN. now apply <- FLX_format_generic. apply -> FLX_format_generic. now apply FLX_format_generic. apply generic_format_FLX. now apply <- FLX_format_FLXN. Qed. ... ...
 ... ... @@ -194,7 +194,7 @@ destruct (Req_dec x 0) as [H4|H4]. intros _. rewrite H4. apply -> FLX_format_FLXN... apply <- FLX_format_generic... apply FLX_format_generic... apply generic_format_0. intros ((xm,xe),(H1,(H2,H3))). specialize (H2 H4). ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!