diff options
Diffstat (limited to 'flocq/IEEE754/Binary.v')
| -rw-r--r-- | flocq/IEEE754/Binary.v | 103 |
1 files changed, 80 insertions, 23 deletions
diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v index ac38c761..35d15cb3 100644 --- a/flocq/IEEE754/Binary.v +++ b/flocq/IEEE754/Binary.v @@ -627,6 +627,52 @@ Proof. now rewrite Pcompare_antisym. Qed. +Theorem bounded_le_emax_minus_prec : + forall mx ex, + bounded mx ex = true -> + (F2R (Float radix2 (Zpos mx) ex) + <= bpow radix2 emax - bpow radix2 (emax - prec))%R. +Proof. +intros mx ex Hx. +destruct (andb_prop _ _ Hx) as (H1,H2). +generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1. +generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2. +generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex). +destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). +unfold mag_val. +intros H. +elim Ex; [|now apply Rgt_not_eq, F2R_gt_0]; intros _. +rewrite <-F2R_Zabs; simpl; clear Ex; intros Ex. +generalize (Rmult_lt_compat_r (bpow radix2 (-ex)) _ _ (bpow_gt_0 _ _) Ex). +unfold F2R; simpl; rewrite Rmult_assoc, <-!bpow_plus. +rewrite H; [|intro H'; discriminate H']. +rewrite <-Z.add_assoc, Z.add_opp_diag_r, Z.add_0_r, Rmult_1_r. +rewrite <-(IZR_Zpower _ _ (Zdigits_ge_0 _ _)); clear Ex; intro Ex. +generalize (Zlt_le_succ _ _ (lt_IZR _ _ Ex)); clear Ex; intro Ex. +generalize (IZR_le _ _ Ex). +rewrite succ_IZR; clear Ex; intro Ex. +generalize (Rplus_le_compat_r (-1) _ _ Ex); clear Ex; intro Ex. +ring_simplify in Ex; revert Ex. +rewrite (IZR_Zpower _ _ (Zdigits_ge_0 _ _)); intro Ex. +generalize (Rmult_le_compat_r (bpow radix2 ex) _ _ (bpow_ge_0 _ _) Ex). +intro H'; apply (Rle_trans _ _ _ H'). +rewrite Rmult_minus_distr_r, Rmult_1_l, <-bpow_plus. +revert H1; unfold fexp, FLT_exp; intro H1. +generalize (Z.le_max_l (Z.pos (digits2_pos mx) + ex - prec) emin). +rewrite H1; intro H1'. +generalize (proj1 (Z.le_sub_le_add_r _ _ _) H1'). +rewrite Zpos_digits2_pos; clear H1'; intro H1'. +apply (Rle_trans _ _ _ (Rplus_le_compat_r _ _ _ (bpow_le _ _ _ H1'))). +replace emax with (emax - prec - ex + (ex + prec))%Z at 1 by ring. +replace (emax - prec)%Z with (emax - prec - ex + ex)%Z at 2 by ring. +do 2 rewrite (bpow_plus _ (emax - prec - ex)). +rewrite <-Rmult_minus_distr_l. +rewrite <-(Rmult_1_l (_ + _)). +apply Rmult_le_compat_r. +{ apply Rle_0_minus, bpow_le; unfold Prec_gt_0 in prec_gt_0_; lia. } +change 1%R with (bpow radix2 0); apply bpow_le; lia. +Qed. + Theorem bounded_lt_emax : forall mx ex, bounded mx ex = true -> @@ -651,7 +697,7 @@ rewrite H. 2: discriminate. revert H1. clear -H2. rewrite Zpos_digits2_pos. unfold fexp, FLT_exp. -intros ; zify ; omega. +intros ; zify ; lia. Qed. Theorem bounded_ge_emin : @@ -679,7 +725,18 @@ unfold fexp, FLT_exp. clear -prec_gt_0_. unfold Prec_gt_0 in prec_gt_0_. clearbody emin. -intros ; zify ; omega. +intros ; zify ; lia. +Qed. + +Theorem abs_B2R_le_emax_minus_prec : + forall x, + (Rabs (B2R x) <= bpow radix2 emax - bpow radix2 (emax - prec))%R. +Proof. +intros [sx|sx|sx plx Hx|sx mx ex Hx] ; simpl ; + [rewrite Rabs_R0 ; apply Rle_0_minus, bpow_le ; + revert prec_gt_0_; unfold Prec_gt_0; lia..|]. +rewrite <- F2R_Zabs, abs_cond_Zopp. +now apply bounded_le_emax_minus_prec. Qed. Theorem abs_B2R_lt_emax : @@ -728,7 +785,7 @@ rewrite Cx. unfold cexp, fexp, FLT_exp. destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). simpl. apply Z.max_lub. -cut (e' - 1 < emax)%Z. clear ; omega. +cut (e' - 1 < emax)%Z. clear ; lia. apply lt_bpow with radix2. apply Rle_lt_trans with (2 := Bx). change (Zpos mx) with (Z.abs (Zpos mx)). @@ -738,7 +795,7 @@ apply Rgt_not_eq. now apply F2R_gt_0. unfold emin. generalize (prec_gt_0 prec). -clear -Hmax ; omega. +clear -Hmax ; lia. Qed. (** Truncation *) @@ -889,7 +946,7 @@ now inversion H. (* *) intros p Hp. assert (He: (e <= fexp (Zdigits radix2 m + e))%Z). -clear -Hp ; zify ; omega. +clear -Hp ; zify ; lia. destruct (inbetween_float_ex radix2 m e l) as (x, Hx). generalize (inbetween_shr x m e l (fexp (Zdigits radix2 m + e) - e) Hm Hx). assert (Hx0 : (0 <= x)%R). @@ -1091,18 +1148,18 @@ rewrite Zpos_digits2_pos. replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec. unfold fexp, FLT_exp, emin. generalize (prec_gt_0 prec). -clear -Hmax ; zify ; omega. +clear -Hmax ; zify ; lia. change 2%Z with (radix_val radix2). case_eq (Zpower radix2 prec - 1)%Z. simpl Zdigits. generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)). -clear ; omega. +clear ; lia. intros p Hp. apply Zle_antisym. -cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega. +cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; lia. apply Zdigits_gt_Zpower. simpl Z.abs. rewrite <- Hp. -cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega. +cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; lia. apply lt_IZR. rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak. apply bpow_lt. @@ -1113,7 +1170,7 @@ simpl Z.abs. rewrite <- Hp. apply Zlt_pred. intros p Hp. generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)). -clear -Hp ; zify ; omega. +clear -Hp ; zify ; lia. apply Rnot_lt_le. intros Hx. generalize (refl_equal (bounded m2 e2)). @@ -1271,18 +1328,18 @@ rewrite Zpos_digits2_pos. replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec. unfold fexp, FLT_exp, emin. generalize (prec_gt_0 prec). -clear -Hmax ; zify ; omega. +clear -Hmax ; zify ; lia. change 2%Z with (radix_val radix2). case_eq (Zpower radix2 prec - 1)%Z. simpl Zdigits. generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)). -clear ; omega. +clear ; lia. intros p Hp. apply Zle_antisym. -cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega. +cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; lia. apply Zdigits_gt_Zpower. simpl Z.abs. rewrite <- Hp. -cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega. +cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; lia. apply lt_IZR. rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak. apply bpow_lt. @@ -1293,7 +1350,7 @@ simpl Z.abs. rewrite <- Hp. apply Zlt_pred. intros p Hp. generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)). -clear -Hp ; zify ; omega. +clear -Hp ; zify ; lia. apply Rnot_lt_le. intros Hx. generalize (refl_equal (bounded m2 e2)). @@ -1370,7 +1427,7 @@ clear -Hmax. unfold emin. intros dx dy dxy Hx Hy Hxy. zify ; intros ; subst. -omega. +lia. (* *) case sx ; case sy. apply Rlt_bool_false. @@ -1479,7 +1536,7 @@ case_eq (ex' - ex)%Z ; simpl. intros H. now rewrite Zminus_eq with (1 := H). intros p. -clear -He ; zify ; omega. +clear -He ; zify ; lia. intros. apply refl_equal. Qed. @@ -1580,7 +1637,7 @@ now rewrite is_finite_FF2B. rewrite Bsign_FF2B, Rz''. rewrite Rcompare_Gt... apply F2R_gt_0. -simpl. zify; omega. +simpl. zify; lia. intros Hz' (Vz, Rz). rewrite B2FF_FF2B, Rz. apply f_equal. @@ -1599,7 +1656,7 @@ now rewrite is_finite_FF2B. rewrite Bsign_FF2B, Rz''. rewrite Rcompare_Lt... apply F2R_lt_0. -simpl. zify; omega. +simpl. zify; lia. intros Hz' (Vz, Rz). rewrite B2FF_FF2B, Rz. apply f_equal. @@ -2150,7 +2207,7 @@ set (e' := Z.min _ _). assert (2 * e' <= ex)%Z as He. { assert (e' <= Z.div2 ex)%Z by apply Z.le_min_r. rewrite (Zdiv2_odd_eqn ex). - destruct Z.odd ; omega. } + destruct Z.odd ; lia. } generalize (Fsqrt_core_correct radix2 (Zpos mx) ex e' eq_refl He). unfold Fsqrt_core. set (mx' := match (ex - 2 * e')%Z with Z0 => _ | _ => _ end). @@ -2187,7 +2244,7 @@ apply Rlt_le_trans with (1 := Heps). fold (bpow radix2 0). apply bpow_le. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. apply Rsqr_incrst_0. 3: apply bpow_ge_0. rewrite Rsqr_mult. @@ -2211,7 +2268,7 @@ now apply IZR_le. change 4%R with (bpow radix2 2). apply bpow_le. generalize (prec_gt_0 prec). -clear -Hmax ; omega. +clear -Hmax ; lia. apply Rmult_le_pos. apply sqrt_ge_0. rewrite <- (Rplus_opp_r 1). @@ -2230,7 +2287,7 @@ unfold Rsqr. rewrite <- bpow_plus. apply bpow_le. unfold emin. -clear -Hmax ; omega. +clear -Hmax ; lia. apply generic_format_ge_bpow with fexp. intros. apply Z.le_max_r. |