diff options
Diffstat (limited to 'flocq/IEEE754/Bits.v')
| -rw-r--r-- | flocq/IEEE754/Bits.v | 138 |
1 files changed, 88 insertions, 50 deletions
diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v index 3a84edfe..68bc541a 100644 --- a/flocq/IEEE754/Bits.v +++ b/flocq/IEEE754/Bits.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * IEEE-754 encoding of binary floating-point data *) + +From Coq Require Import Lia. Require Import Core Digits Binary. Section Binary_Bits. @@ -43,10 +45,10 @@ Proof. intros s m e Hm He. assert (0 <= mw)%Z as Hmw. destruct mw as [|mw'|mw'] ; try easy. - clear -Hm ; simpl in Hm ; omega. + clear -Hm ; simpl in Hm ; lia. assert (0 <= ew)%Z as Hew. destruct ew as [|ew'|ew'] ; try easy. - clear -He ; simpl in He ; omega. + clear -He ; simpl in He ; lia. unfold join_bits. rewrite Z.shiftl_mul_pow2 by easy. split. @@ -54,9 +56,9 @@ split. rewrite <- (Zmult_0_l (2^mw)). apply Zmult_le_compat_r. case s. - clear -He ; omega. + clear -He ; lia. now rewrite Zmult_0_l. - clear -Hm ; omega. + clear -Hm ; lia. - apply Z.lt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) * 2 ^ mw)%Z. rewrite (Zmult_plus_distr_l _ 1). apply Zplus_lt_compat_l. @@ -65,9 +67,9 @@ split. apply Zmult_le_compat_r. rewrite Zpower_plus by easy. change (2^1)%Z with 2%Z. - case s ; clear -He ; omega. - clear -Hm ; omega. - clear -Hew ; omega. + case s ; clear -He ; lia. + clear -Hm ; lia. + clear -Hew ; lia. easy. Qed. @@ -85,10 +87,10 @@ Proof. intros s m e Hm He. assert (0 <= mw)%Z as Hmw. destruct mw as [|mw'|mw'] ; try easy. - clear -Hm ; simpl in Hm ; omega. + clear -Hm ; simpl in Hm ; lia. assert (0 <= ew)%Z as Hew. destruct ew as [|ew'|ew'] ; try easy. - clear -He ; simpl in He ; omega. + clear -He ; simpl in He ; lia. unfold split_bits, join_bits. rewrite Z.shiftl_mul_pow2 by easy. apply f_equal2 ; [apply f_equal2|]. @@ -99,7 +101,7 @@ apply f_equal2 ; [apply f_equal2|]. apply Zplus_le_0_compat. apply Zmult_le_0_compat. apply He. - clear -Hm ; omega. + clear -Hm ; lia. apply Hm. + apply Zle_bool_false. apply Zplus_lt_reg_l with (2^mw * (-e))%Z. @@ -108,12 +110,12 @@ apply f_equal2 ; [apply f_equal2|]. apply Z.lt_le_trans with (2^mw * 1)%Z. now apply Zmult_lt_compat_r. apply Zmult_le_compat_l. - clear -He ; omega. - clear -Hm ; omega. + clear -He ; lia. + clear -Hm ; lia. - rewrite Zplus_comm. rewrite Z_mod_plus_full. now apply Zmod_small. -- rewrite Z_div_plus_full_l by (clear -Hm ; omega). +- rewrite Z_div_plus_full_l by (clear -Hm ; lia). rewrite Zdiv_small with (1 := Hm). rewrite Zplus_0_r. case s. @@ -175,7 +177,7 @@ rewrite Zdiv_Zdiv. apply sym_eq. case Zle_bool_spec ; intros Hs. apply Zle_antisym. -cut (x / (2^mw * 2^ew) < 2)%Z. clear ; omega. +cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia. apply Zdiv_lt_upper_bound. now apply Zmult_lt_0_compat. rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ). @@ -244,8 +246,8 @@ Theorem split_bits_of_binary_float_correct : split_bits (bits_of_binary_float x) = split_bits_of_binary_float x. Proof. intros [sx|sx|sx plx Hplx|sx mx ex Hx] ; - try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; omega ). -simpl. apply split_join_bits; split; try (zify; omega). + try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; lia ). +simpl. apply split_join_bits; split; try (zify; lia). destruct (digits2_Pnat_correct plx). unfold nan_pl in Hplx. rewrite Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx. @@ -253,7 +255,7 @@ rewrite Zpower_nat_Z in H0. eapply Z.lt_le_trans. apply H0. change 2%Z with (radix_val radix2). apply Zpower_le. rewrite Z.ltb_lt in Hplx. -unfold prec in *. zify; omega. +unfold prec in *. zify; lia. (* *) unfold bits_of_binary_float, split_bits_of_binary_float. assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z). @@ -263,14 +265,14 @@ rewrite Zpos_digits2_pos in Hx'. generalize (Zeq_bool_eq _ _ Hx'). unfold FLT_exp. unfold emin. -clear ; zify ; omega. +clear ; zify ; lia. case Zle_bool_spec ; intros H ; [ apply -> Z.le_0_sub in H | apply -> Z.lt_sub_0 in H ] ; apply split_join_bits ; try now split. (* *) split. -clear -He_gt_0 H ; omega. -cut (Zpos mx < 2 * 2^mw)%Z. clear ; omega. +clear -He_gt_0 H ; lia. +cut (Zpos mx < 2 * 2^mw)%Z. clear ; lia. replace (2 * 2^mw)%Z with (2^prec)%Z. apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)). apply Hf. @@ -282,12 +284,12 @@ now apply Zlt_le_weak. (* *) split. generalize (proj1 Hf). -clear ; omega. +clear ; lia. destruct (andb_prop _ _ Hx) as (_, Hx'). unfold emin. replace (2^ew)%Z with (2 * emax)%Z. generalize (Zle_bool_imp_le _ _ Hx'). -clear ; omega. +clear ; lia. apply sym_eq. rewrite (Zsucc_pred ew). unfold Z.succ. @@ -305,7 +307,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H]. - apply join_bits_range ; now split. - apply join_bits_range. now split. - clear -He_gt_0 ; omega. + clear -He_gt_0 ; lia. - apply Z.ltb_lt in pl_range. apply join_bits_range. split. @@ -313,7 +315,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H]. apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)). apply Z.lt_succ_r. now rewrite <- Zdigits2_Zdigits. - clear -He_gt_0 ; omega. + clear -He_gt_0 ; lia. - unfold bounded in H. apply Bool.andb_true_iff in H ; destruct H as [A B]. apply Z.leb_le in B. @@ -321,22 +323,22 @@ intros [sx|sx|sx pl pl_range|sx mx ex H]. case Zle_bool_spec ; intros H. + apply join_bits_range. * split. - clear -H ; omega. + clear -H ; lia. rewrite Zpos_digits2_pos in A. cut (Zpos mx < 2 ^ prec)%Z. unfold prec. - rewrite Zpower_plus by (clear -Hmw ; omega). + rewrite Zpower_plus by (clear -Hmw ; lia). change (2^1)%Z with 2%Z. - clear ; omega. + clear ; lia. apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)). - clear -A ; zify ; omega. + clear -A ; zify ; lia. * split. - unfold emin ; clear -A ; zify ; omega. + unfold emin ; clear -A ; zify ; lia. replace ew with ((ew - 1) + 1)%Z by ring. - rewrite Zpower_plus by (clear - Hew ; omega). + rewrite Zpower_plus by (clear - Hew ; lia). unfold emin, emax in *. change (2^1)%Z with 2%Z. - clear -B ; omega. + clear -B ; lia. + apply -> Z.lt_sub_0 in H. apply join_bits_range ; now split. Qed. @@ -370,7 +372,7 @@ unfold binary_float_of_bits_aux, split_bits. assert (Hnan: nan_pl prec 1 = true). apply Z.ltb_lt. simpl. unfold prec. - clear -Hmw ; omega. + clear -Hmw ; lia. case Zeq_bool_spec ; intros He1. case_eq (x mod 2^mw)%Z ; try easy. (* subnormal *) @@ -389,7 +391,7 @@ unfold Fexp, FLT_exp. apply sym_eq. apply Zmax_right. clear -H Hprec. -unfold prec ; omega. +unfold prec ; lia. apply Rnot_le_lt. intros H0. refine (_ (mag_le radix2 _ _ _ H0)). @@ -397,20 +399,20 @@ rewrite mag_bpow. rewrite mag_F2R_Zdigits. 2: discriminate. unfold emin, prec. apply Zlt_not_le. -cut (0 < emax)%Z. clear -H Hew ; omega. +cut (0 < emax)%Z. clear -H Hew ; lia. apply (Zpower_gt_0 radix2). -clear -Hew ; omega. +clear -Hew ; lia. apply bpow_gt_0. case Zeq_bool_spec ; intros He2. case_eq (x mod 2 ^ mw)%Z; try easy. (* nan *) intros plx Eqplx. apply Z.ltb_lt. rewrite Zpos_digits2_pos. -assert (forall a b, a <= b -> a < b+1)%Z by (intros; omega). apply H. clear H. +assert (forall a b, a <= b -> a < b+1)%Z by (intros; lia). apply H. clear H. apply Zdigits_le_Zpower. simpl. rewrite <- Eqplx. edestruct Z_mod_lt; eauto. change 2%Z with (radix_val radix2). -apply Z.lt_gt, Zpower_gt_0. omega. +apply Z.lt_gt, Zpower_gt_0. lia. case_eq (x mod 2^mw + 2^mw)%Z ; try easy. (* normal *) intros px Hm. @@ -452,7 +454,7 @@ revert He1. fold ex. cut (0 <= ex)%Z. unfold emin. -clear ; intros H1 H2 ; omega. +clear ; intros H1 H2 ; lia. eapply Z_mod_lt. apply Z.lt_gt. apply (Zpower_gt_0 radix2). @@ -471,12 +473,12 @@ revert He2. set (ex := ((x / 2^mw) mod 2^ew)%Z). cut (ex < 2^ew)%Z. replace (2^ew)%Z with (2 * emax)%Z. -clear ; intros H1 H2 ; omega. +clear ; intros H1 H2 ; lia. replace ew with (1 + (ew - 1))%Z by ring. rewrite Zpower_exp. apply refl_equal. discriminate. -clear -Hew ; omega. +clear -Hew ; lia. eapply Z_mod_lt. apply Z.lt_gt. apply (Zpower_gt_0 radix2). @@ -503,13 +505,13 @@ apply refl_equal. simpl. rewrite Zeq_bool_false. now rewrite Zeq_bool_true. -cut (1 < 2^ew)%Z. clear ; omega. +cut (1 < 2^ew)%Z. clear ; lia. now apply (Zpower_gt_1 radix2). (* *) simpl. rewrite Zeq_bool_false. rewrite Zeq_bool_true; auto. -cut (1 < 2^ew)%Z. clear ; omega. +cut (1 < 2^ew)%Z. clear ; lia. now apply (Zpower_gt_1 radix2). (* *) unfold split_bits_of_binary_float. @@ -522,19 +524,19 @@ destruct (andb_prop _ _ Bx) as (_, H1). generalize (Zle_bool_imp_le _ _ H1). unfold emin. replace (2^ew)%Z with (2 * emax)%Z. -clear ; omega. +clear ; lia. replace ew with (1 + (ew - 1))%Z by ring. rewrite Zpower_exp. apply refl_equal. discriminate. -clear -Hew ; omega. +clear -Hew ; lia. destruct (andb_prop _ _ Bx) as (H1, _). generalize (Zeq_bool_eq _ _ H1). rewrite Zpos_digits2_pos. unfold FLT_exp, emin. generalize (Zdigits radix2 (Zpos mx)). clear. -intros ; zify ; omega. +intros ; zify ; lia. (* . *) rewrite Zeq_bool_true. 2: apply refl_equal. simpl. @@ -547,7 +549,7 @@ apply -> Z.lt_sub_0 in Hm. generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm). generalize (Zdigits radix2 (Zpos mx)). clear. -intros ; zify ; omega. +intros ; zify ; lia. Qed. Theorem bits_of_binary_float_of_bits : @@ -588,12 +590,12 @@ case Zeq_bool_spec ; intros He2. case_eq mx; intros Hm. now rewrite He2. now rewrite He2. -intros. zify; omega. +intros. zify; lia. (* normal *) case_eq (mx + 2 ^ mw)%Z. intros Hm. apply False_ind. -clear -Bm Hm ; omega. +clear -Bm Hm ; lia. intros p Hm Jx Cx. rewrite <- Hm. rewrite Zle_bool_true. @@ -601,7 +603,7 @@ now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z. now ring_simplify. intros p Hm. apply False_ind. -clear -Bm Hm ; zify ; omega. +clear -Bm Hm ; zify ; lia. Qed. End Binary_Bits. @@ -623,6 +625,12 @@ Proof. apply refl_equal. Qed. +Let Hemax : (3 <= 128)%Z. +Proof. +intros H. +discriminate H. +Qed. + Definition default_nan_pl32 : { nan : binary32 | is_nan 24 128 nan = true } := exist _ (@B754_nan 24 128 false (iter_nat xO 22 xH) (refl_equal true)) (refl_equal true). @@ -639,16 +647,28 @@ Definition binop_nan_pl32 (f1 f2 : binary32) : { nan : binary32 | is_nan 24 128 | _, _ => default_nan_pl32 end. +Definition ternop_nan_pl32 (f1 f2 f3 : binary32) : { nan : binary32 | is_nan 24 128 nan = true } := + match f1, f2, f3 with + | B754_nan s1 pl1 Hpl1, _, _ => exist _ (B754_nan s1 pl1 Hpl1) (refl_equal true) + | _, B754_nan s2 pl2 Hpl2, _ => exist _ (B754_nan s2 pl2 Hpl2) (refl_equal true) + | _, _, B754_nan s3 pl3 Hpl3 => exist _ (B754_nan s3 pl3 Hpl3) (refl_equal true) + | _, _, _ => default_nan_pl32 + end. + Definition b32_erase : binary32 -> binary32 := erase 24 128. Definition b32_opp : binary32 -> binary32 := Bopp 24 128 unop_nan_pl32. Definition b32_abs : binary32 -> binary32 := Babs 24 128 unop_nan_pl32. -Definition b32_sqrt : mode -> binary32 -> binary32 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32. +Definition b32_pred : binary32 -> binary32 := Bpred _ _ Hprec Hprec_emax Hemax unop_nan_pl32. +Definition b32_succ : binary32 -> binary32 := Bsucc _ _ Hprec Hprec_emax Hemax unop_nan_pl32. +Definition b32_sqrt : mode -> binary32 -> binary32 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32. Definition b32_plus : mode -> binary32 -> binary32 -> binary32 := Bplus _ _ Hprec Hprec_emax binop_nan_pl32. Definition b32_minus : mode -> binary32 -> binary32 -> binary32 := Bminus _ _ Hprec Hprec_emax binop_nan_pl32. Definition b32_mult : mode -> binary32 -> binary32 -> binary32 := Bmult _ _ Hprec Hprec_emax binop_nan_pl32. Definition b32_div : mode -> binary32 -> binary32 -> binary32 := Bdiv _ _ Hprec Hprec_emax binop_nan_pl32. +Definition b32_fma : mode -> binary32 -> binary32 -> binary32 -> binary32 := Bfma _ _ Hprec Hprec_emax ternop_nan_pl32. + Definition b32_compare : binary32 -> binary32 -> option comparison := Bcompare 24 128. Definition b32_of_bits : Z -> binary32 := binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _). Definition bits_of_b32 : binary32 -> Z := bits_of_binary_float 23 8. @@ -672,6 +692,12 @@ Proof. apply refl_equal. Qed. +Let Hemax : (3 <= 1024)%Z. +Proof. +intros H. +discriminate H. +Qed. + Definition default_nan_pl64 : { nan : binary64 | is_nan 53 1024 nan = true } := exist _ (@B754_nan 53 1024 false (iter_nat xO 51 xH) (refl_equal true)) (refl_equal true). @@ -688,9 +714,19 @@ Definition binop_nan_pl64 (f1 f2 : binary64) : { nan : binary64 | is_nan 53 1024 | _, _ => default_nan_pl64 end. +Definition ternop_nan_pl64 (f1 f2 f3 : binary64) : { nan : binary64 | is_nan 53 1024 nan = true } := + match f1, f2, f3 with + | B754_nan s1 pl1 Hpl1, _, _ => exist _ (B754_nan s1 pl1 Hpl1) (refl_equal true) + | _, B754_nan s2 pl2 Hpl2, _ => exist _ (B754_nan s2 pl2 Hpl2) (refl_equal true) + | _, _, B754_nan s3 pl3 Hpl3 => exist _ (B754_nan s3 pl3 Hpl3) (refl_equal true) + | _, _, _ => default_nan_pl64 + end. + Definition b64_erase : binary64 -> binary64 := erase 53 1024. Definition b64_opp : binary64 -> binary64 := Bopp 53 1024 unop_nan_pl64. Definition b64_abs : binary64 -> binary64 := Babs 53 1024 unop_nan_pl64. +Definition b64_pred : binary64 -> binary64 := Bpred _ _ Hprec Hprec_emax Hemax unop_nan_pl64. +Definition b64_succ : binary64 -> binary64 := Bsucc _ _ Hprec Hprec_emax Hemax unop_nan_pl64. Definition b64_sqrt : mode -> binary64 -> binary64 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64. Definition b64_plus : mode -> binary64 -> binary64 -> binary64 := Bplus _ _ Hprec Hprec_emax binop_nan_pl64. @@ -698,6 +734,8 @@ Definition b64_minus : mode -> binary64 -> binary64 -> binary64 := Bminus _ _ Hp Definition b64_mult : mode -> binary64 -> binary64 -> binary64 := Bmult _ _ Hprec Hprec_emax binop_nan_pl64. Definition b64_div : mode -> binary64 -> binary64 -> binary64 := Bdiv _ _ Hprec Hprec_emax binop_nan_pl64. +Definition b64_fma : mode -> binary64 -> binary64 -> binary64 -> binary64 := Bfma _ _ Hprec Hprec_emax ternop_nan_pl64. + Definition b64_compare : binary64 -> binary64 -> option comparison := Bcompare 53 1024. Definition b64_of_bits : Z -> binary64 := binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _). Definition bits_of_b64 : binary64 -> Z := bits_of_binary_float 52 11. |