diff options
Diffstat (limited to 'flocq/Core/Generic_fmt.v')
| -rw-r--r-- | flocq/Core/Generic_fmt.v | 123 |
1 files changed, 106 insertions, 17 deletions
diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index cb37bd91..af1bf3c1 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * What is a real number belonging to a format, and many properties. *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Float_prop. Section Generic. @@ -52,7 +54,7 @@ apply Znot_ge_lt. intros Hl. apply Z.ge_le in Hl. assert (H' := proj2 (proj2 (valid_exp l) Hl) k). -omega. +lia. Qed. Theorem valid_exp_large' : @@ -67,7 +69,7 @@ apply Z.ge_le in H'. assert (Hl := Z.le_trans _ _ _ H H'). apply valid_exp in Hl. assert (H1 := proj2 Hl k H'). -omega. +lia. Qed. Definition cexp x := @@ -425,7 +427,7 @@ rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. -clear ; zify ; omega. +clear ; zify ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. @@ -522,7 +524,7 @@ specialize (Ex Hxz). apply Rlt_le_trans with (1 := proj2 Ex). apply bpow_le. specialize (Hp ex). -omega. +lia. Qed. Theorem generic_format_bpow_inv' : @@ -544,7 +546,7 @@ apply bpow_gt_0. split. apply bpow_ge_0. apply (bpow_lt _ _ 0). -clear -He ; omega. +clear -He ; lia. Qed. Theorem generic_format_bpow_inv : @@ -555,7 +557,7 @@ Proof. intros e He. apply generic_format_bpow_inv' in He. assert (H := valid_exp_large' (e + 1) e). -omega. +lia. Qed. Section Fcore_generic_round_pos. @@ -587,7 +589,7 @@ rewrite <- (Zrnd_IZR (Zceil x)). apply Zrnd_le. apply Zceil_ub. rewrite Zceil_floor_neq. -omega. +lia. intros H. rewrite <- H in Hx. rewrite Zfloor_IZR, Zrnd_IZR in Hx. @@ -630,7 +632,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)). apply IZR_Zpower. -omega. +lia. rewrite <- Hf. apply IZR_le. apply Zfloor_lub. @@ -657,7 +659,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)). apply IZR_Zpower. -omega. +lia. rewrite <- Hf. apply IZR_le. apply Zceil_glb. @@ -738,7 +740,7 @@ destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. apply bpow_le. apply valid_exp, proj2 in Hx1. specialize (Hx1 ey). - omega. + lia. apply Rle_trans with (bpow ex). now apply round_bounded_large_pos. apply bpow_le. @@ -1380,7 +1382,7 @@ specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. apply Rle_trans with (bpow (ex - 1)). apply bpow_le. -cut (e < ex)%Z. omega. +cut (e < ex)%Z. lia. apply (lt_bpow beta). now apply Rle_lt_trans with (2 := proj2 He). destruct (Zle_or_lt ex (fexp ex)). @@ -1389,7 +1391,7 @@ rewrite Hr in Hd. elim Rlt_irrefl with (1 := Hd). rewrite Hr. apply bpow_le. -omega. +lia. apply (round_bounded_large_pos rnd x ex H He). Qed. @@ -1526,7 +1528,7 @@ unfold cexp. set (ex := mag beta x). generalize (exp_not_FTZ ex). generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z). -omega. +lia. rewrite <- H. rewrite <- mult_IZR, Ztrunc_IZR. unfold F2R. simpl. @@ -1802,7 +1804,7 @@ Theorem Znearest_imp : Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. -clear ; zify ; omega. +clear ; zify ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. @@ -1937,7 +1939,7 @@ replace (- _ + _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r. apply (Rlt_le_trans _ _ _ (proj2 Hex)). apply Rle_trans with (bpow (fexp (mag beta x) - 1)). - apply bpow_le. - rewrite (mag_unique beta x ex); [omega|]. + rewrite (mag_unique beta x ex); [lia|]. now rewrite Rabs_right. - unfold Zminus; rewrite bpow_plus. rewrite Rmult_comm. @@ -2012,6 +2014,68 @@ Qed. End rndNA. +Notation Znearest0 := (Znearest (fun x => (Zlt_bool x 0))). + +Section rndN0. + +Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _. + +Theorem round_N0_pt : + forall x, + Rnd_N0_pt generic_format x (round Znearest0 x). +Proof. +intros x. +generalize (round_N_pt (fun t => Zlt_bool t 0) x). +set (f := round (Znearest (fun t => Zlt_bool t 0)) x). +intros Rxf. +destruct (Req_dec (x - round Zfloor x) (round Zceil x - x)) as [Hm|Hm]. +(* *) +apply Rnd_N0_pt_N. +apply generic_format_0. +exact Rxf. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +(* . *) +rewrite Rabs_pos_eq with (1 := Hx). +rewrite Rabs_pos_eq. +unfold f. +rewrite round_N_middle with (1 := Hm). +rewrite Zlt_bool_false. +now apply round_DN_pt. +apply Zfloor_lub. +apply Rmult_le_pos with (1 := Hx). +apply bpow_ge_0. +apply Rnd_N_pt_ge_0 with (2 := Hx) (3 := Rxf). +apply generic_format_0. +(* . *) +rewrite Rabs_left with (1 := Hx). +rewrite Rabs_left1. +apply Ropp_le_contravar. +unfold f. +rewrite round_N_middle with (1 := Hm). +rewrite Zlt_bool_true. +now apply round_UP_pt. +apply lt_IZR. +apply Rle_lt_trans with (scaled_mantissa x). +apply Zfloor_lb. +simpl. +rewrite <- (Rmult_0_l (bpow (- (cexp x))%Z)%R). +apply Rmult_lt_compat_r with (2 := Hx). +apply bpow_gt_0. +apply Rnd_N_pt_le_0 with (3 := Rxf). +apply generic_format_0. +now apply Rlt_le. +(* *) +split. +apply Rxf. +intros g Rxg. +rewrite Rnd_N_pt_unique with (3 := Hm) (4 := Rxf) (5 := Rxg). +apply Rle_refl. +apply round_DN_pt; easy. +apply round_UP_pt; easy. +Qed. + +End rndN0. + Section rndN_opp. Theorem Znearest_opp : @@ -2055,6 +2119,31 @@ rewrite opp_IZR. now rewrite Ropp_mult_distr_l_reverse. Qed. +Lemma round_N0_opp : + forall x, + (round Znearest0 (- x) = - round Znearest0 x)%R. +Proof. +intros x. +rewrite round_N_opp. +apply Ropp_eq_compat. +apply round_ext. +clear x; intro x. +unfold Znearest. +case_eq (Rcompare (x - IZR (Zfloor x)) (/ 2)); intro C; +[|reflexivity|reflexivity]. +apply Rcompare_Eq_inv in C. +assert (H : negb (- (Zfloor x + 1) <? 0)%Z = (Zfloor x <? 0)%Z); + [|now rewrite H]. +rewrite negb_Zlt_bool. +case_eq (Zfloor x <? 0)%Z; intro C'. +apply Zlt_is_lt_bool in C'. +apply Zle_bool_true. +lia. +apply Z.ltb_ge in C'. +apply Zle_bool_false. +lia. +Qed. + End rndN_opp. Lemma round_N_small : @@ -2293,10 +2382,10 @@ rewrite negb_Zle_bool. case_eq (0 <=? Zfloor x)%Z; intro C'. - apply Zle_bool_imp_le in C'. apply Zlt_bool_true. - omega. + lia. - rewrite Z.leb_gt in C'. apply Zlt_bool_false. - omega. + lia. Qed. End rndNA_opp. |