From d4513f41c54869c9b4ba96ab79d50933a1d5c25a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Dec 2020 15:53:36 +0100 Subject: Update Flocq to 3.4.0 (#383) --- flocq/Prop/Div_sqrt_error.v | 30 ++-- flocq/Prop/Double_rounding.v | 417 ++++++++++++++++++++++--------------------- flocq/Prop/Mult_error.v | 43 +++-- flocq/Prop/Plus_error.v | 23 ++- flocq/Prop/Relative.v | 24 +-- flocq/Prop/Round_odd.v | 36 ++-- flocq/Prop/Sterbenz.v | 2 +- 7 files changed, 298 insertions(+), 277 deletions(-) (limited to 'flocq/Prop') diff --git a/flocq/Prop/Div_sqrt_error.v b/flocq/Prop/Div_sqrt_error.v index 79220438..9aa9c508 100644 --- a/flocq/Prop/Div_sqrt_error.v +++ b/flocq/Prop/Div_sqrt_error.v @@ -42,9 +42,7 @@ rewrite H; apply generic_format_0. rewrite Hx, Hy, <- F2R_plus. apply generic_format_F2R. intros _. -case_eq (Fplus fx fy). -intros mz ez Hz. -rewrite <- Hz. +change (F2R _) with (F2R (Fplus fx fy)). apply Z.le_trans with (Z.min (Fexp fx) (Fexp fy)). rewrite F2R_plus, <- Hx, <- Hy. unfold cexp. @@ -52,7 +50,7 @@ apply Z.le_trans with (1:=Hfexp _). apply Zplus_le_reg_l with prec; ring_simplify. apply mag_le_bpow with (1 := H). now apply Z.min_case. -rewrite <- Fexp_Fplus, Hz. +rewrite <- Fexp_Fplus. apply Z.le_refl. Qed. @@ -100,7 +98,7 @@ apply Rlt_le_trans with (1 := Heps1). change 1%R with (bpow 0). apply bpow_le. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. rewrite Rmult_1_r. rewrite Hx2, <- Hx1. unfold cexp. @@ -193,7 +191,7 @@ now apply IZR_lt. rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l. apply Rle_trans with (bpow (-1)). apply bpow_le. -omega. +lia. replace (2 * (-1 + 5 / 4))%R with (/2)%R by field. apply Rinv_le. now apply IZR_lt. @@ -280,11 +278,11 @@ apply Rle_not_lt. rewrite <- Hr1. apply abs_round_ge_generic... apply generic_format_bpow. -unfold FLX_exp; omega. +unfold FLX_exp; lia. apply Es. apply Rlt_le_trans with (1:=H). apply bpow_le. -omega. +lia. now apply Rlt_le. Qed. @@ -319,7 +317,7 @@ rewrite <- bpow_plus; apply bpow_le; unfold e; set (mxm1 := (_ - 1)%Z). replace (_ * _)%Z with (2 * (mxm1 / 2) + mxm1 mod 2 - mxm1 mod 2)%Z by ring. rewrite <- Z.div_mod; [|now simpl]. apply (Zplus_le_reg_r _ _ (mxm1 mod 2 - mag beta x)%Z). -unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); omega. +unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); lia. Qed. Notation u_ro := (u_ro beta prec). @@ -346,7 +344,7 @@ assert (Hulp1p2eps : (ulp beta (FLX_exp prec) (1 + 2 * u_ro) = 2 * u_ro)%R). rewrite succ_FLX_1, mag_1, bpow_1, <- H2eps; simpl. apply (Rlt_le_trans _ 2); [apply Rplus_lt_compat_l|]. { unfold u_ro; rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l; [|lra]. - change R1 with (bpow 0); apply bpow_lt; omega. } + change R1 with (bpow 0); apply bpow_lt; lia. } apply IZR_le, Zle_bool_imp_le, radix_prop. } assert (Hsucc1p2eps : (succ beta (FLX_exp prec) (1 + 2 * u_ro) = 1 + 4 * u_ro)%R). @@ -383,7 +381,7 @@ ring_simplify; apply Rsqr_incr_0_var. apply Rmult_le_pos; [|now apply pow_le]. assert (Heps_le_half : (u_ro <= 1 / 2)%R). { unfold u_ro, Rdiv; rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|]. - change 1%R with (bpow 0); apply bpow_le; omega. } + change 1%R with (bpow 0); apply bpow_le; lia. } apply (Rle_trans _ (-8 * u_ro + 4)); [lra|]. apply Rplus_le_compat_r, Rmult_le_compat_r; [apply Pu_ro|]. now assert (H : (0 <= u_ro ^ 2)%R); [apply pow2_ge_0|lra]. } @@ -447,13 +445,13 @@ destruct (sqrt_error_N_FLX_aux2 _ Fmu HmuGe1) as [Hmu'|[Hmu'|Hmu']]. { rewrite Rminus_diag_eq, Rabs_R0; [|now simpl]. now apply Rmult_le_pos; [|apply Rabs_pos]. } apply generic_format_bpow'; [now apply FLX_exp_valid|]. - unfold FLX_exp; omega. } + unfold FLX_exp; lia. } { assert (Hsqrtmu : (1 <= sqrt mu < 1 + u_ro)%R); [rewrite Hmu'; split|]. { rewrite <- sqrt_1 at 1; apply sqrt_le_1_alt; lra. } { rewrite <- sqrt_square; [|lra]; apply sqrt_lt_1_alt; split; [lra|]. ring_simplify; assert (0 < u_ro ^ 2)%R; [apply pow_lt|]; lra. } assert (Fbpowe : generic_format beta (FLX_exp prec) (bpow e)). - { apply generic_format_bpow; unfold FLX_exp; omega. } + { apply generic_format_bpow; unfold FLX_exp; lia. } assert (Hrt : rt = bpow e :> R). { unfold rt; fold t; rewrite Ht; simpl; apply Rle_antisym. { apply round_N_le_midp; [now apply FLX_exp_valid|exact Fbpowe|]. @@ -495,7 +493,7 @@ assert (Hulpt : (ulp beta (FLX_exp prec) t = 2 * u_ro * bpow e)%R). { apply sqrt_lt_1_alt; split; [lra|]. apply (Rlt_le_trans _ _ _ HmuLtsqradix); right. now unfold bpow, Z.pow_pos; simpl; rewrite Zmult_1_r, mult_IZR. } - apply IZR_le, (Z.le_trans _ 2), Zle_bool_imp_le, radix_prop; omega. } + apply IZR_le, (Z.le_trans _ 2), Zle_bool_imp_le, radix_prop; lia. } rewrite Hmagt; ring. } rewrite Ht; apply Rmult_lt_0_compat; [|now apply bpow_gt_0]. now apply (Rlt_le_trans _ 1); [lra|rewrite <- sqrt_1; apply sqrt_le_1_alt]. } @@ -656,7 +654,7 @@ apply Fourier_util.Rle_mult_inv_pos; assumption. case (Zle_lt_or_eq 0 n); try exact H. clear H; intros H. case (Zle_lt_or_eq 1 n). -omega. +lia. clear H; intros H. set (ex := cexp beta fexp x). set (ey := cexp beta fexp y). @@ -715,7 +713,7 @@ rewrite Rinv_l, Rmult_1_r, Rmult_1_l. assert (mag beta x < mag beta y)%Z. case (Zle_or_lt (mag beta y) (mag beta x)); try easy. intros J; apply monotone_exp in J; clear -J Hexy. -unfold ex, ey, cexp in Hexy; omega. +unfold ex, ey, cexp in Hexy; lia. left; apply lt_mag with beta; easy. (* n = 1 -> Sterbenz + rnd_small *) intros Hn'; fold n; rewrite <- Hn'. diff --git a/flocq/Prop/Double_rounding.v b/flocq/Prop/Double_rounding.v index 055409bb..3e942fe0 100644 --- a/flocq/Prop/Double_rounding.v +++ b/flocq/Prop/Double_rounding.v @@ -122,7 +122,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx'']. apply (Rle_lt_trans _ _ _ Hr1). apply Rmult_lt_compat_l; [lra|]. apply bpow_lt. - omega. + lia. - (* x'' <> 0 *) assert (Lx'' : mag x'' = mag x :> Z). { apply Zle_antisym. @@ -203,7 +203,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx']. replace (2 * (/ 2 * _)) with (bpow (fexp1 (mag x) - mag x)) by field. apply Rle_trans with 1; [|lra]. change 1 with (bpow 0); apply bpow_le. - omega. + lia. - (* x' <> 0 *) assert (Px' : 0 < x'). { assert (0 <= x'); [|lra]. @@ -314,10 +314,10 @@ Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2']. - (* fexp1 (mag x) <= fexp2 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia. now apply round_round_lt_mid_same_place. - (* fexp2 (mag x) < fexp1 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. generalize (Hx' Hf2''); intro Hx''. now apply round_round_lt_mid_further_place. Qed. @@ -380,7 +380,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx'']. apply (Rle_lt_trans _ _ _ Hr1). apply Rmult_lt_compat_l; [lra|]. apply bpow_lt. - omega. + lia. - (* x'' <> 0 *) assert (Lx'' : mag x'' = mag x :> Z). { apply Zle_antisym. @@ -460,11 +460,11 @@ assert (Hx''pow : x'' = bpow (mag x)). unfold x'', round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_le_reg_r (bpow (- fexp2 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)); [|lia]. apply IZR_le. apply Zlt_succ_le; unfold Z.succ. apply lt_IZR. - rewrite plus_IZR; rewrite IZR_Zpower; [|omega]. + rewrite plus_IZR; rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. bpow_simplify. @@ -482,12 +482,12 @@ assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x). - apply Rmult_lt_compat_l; [lra|]. rewrite 2!ulp_neq_0; try now apply Rgt_not_eq. unfold cexp; apply bpow_lt. - omega. } + lia. } unfold round, F2R, scaled_mantissa, cexp; simpl. assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). { rewrite Hx''pow. rewrite mag_bpow. - assert (fexp1 (mag x + 1) <= mag x)%Z; [|omega]. + assert (fexp1 (mag x + 1) <= mag x)%Z; [|lia]. destruct (Zle_or_lt (mag x) (fexp1 (mag x))) as [Hle|Hlt]; [|now apply Vfexp1]. assert (H : (mag x = fexp1 (mag x) :> Z)%Z); @@ -497,9 +497,9 @@ assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x'')))%Z). - rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x)))%Z). + rewrite IZR_Zpower; [|exact Hf]. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. now bpow_simplify. - + rewrite IZR_Zpower; [|omega]. + + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; [|now apply Rle_ge; apply bpow_ge_0]. @@ -588,10 +588,10 @@ Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'. destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2']. - (* fexp1 (mag x) <= fexp2 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia. now apply round_round_gt_mid_same_place. - (* fexp2 (mag x) < fexp1 (mag x) *) - assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|]. + assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. generalize (Hx' Hf2''); intro Hx''. now apply round_round_gt_mid_further_place. Qed. @@ -606,7 +606,7 @@ Lemma mag_mult_disj : Proof. intros x y Zx Zy. destruct (mag_mult beta x y Zx Zy). -omega. +lia. Qed. Definition round_round_mult_hyp fexp1 fexp2 := @@ -691,7 +691,7 @@ intros Hprec x y Fx Fy. apply round_round_mult; [|now apply generic_format_FLX|now apply generic_format_FLX]. unfold round_round_mult_hyp; split; intros ex ey; unfold FLX_exp; -omega. +lia. Qed. End Double_round_mult_FLX. @@ -721,7 +721,7 @@ generalize (Zmax_spec (ex + ey - prec') emin'); generalize (Zmax_spec (ex + ey - 1 - prec') emin'); generalize (Zmax_spec (ex - prec) emin); generalize (Zmax_spec (ey - prec) emin); -omega. +lia. Qed. End Double_round_mult_FLT. @@ -753,7 +753,7 @@ destruct (Z.ltb_spec (ex + ey - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex + ey - 1 - prec') emin'); -omega. +lia. Qed. End Double_round_mult_FTZ. @@ -770,7 +770,7 @@ Lemma mag_plus_disj : Proof. intros x y Py Hxy. destruct (mag_plus beta x y Py Hxy). -omega. +lia. Qed. Lemma mag_plus_separated : @@ -798,10 +798,10 @@ Lemma mag_minus_disj : \/ (mag (x - y) = (mag x - 1)%Z :> Z)). Proof. intros x y Px Py Hln. -assert (Hxy : y < x); [now apply (lt_mag beta); [ |omega]|]. +assert (Hxy : y < x); [now apply (lt_mag beta); [ |lia]|]. generalize (mag_minus beta x y Py Hxy); intro Hln2. generalize (mag_minus_lb beta x y Px Py Hln); intro Hln3. -omega. +lia. Qed. Lemma mag_minus_separated : @@ -831,7 +831,7 @@ split. apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption]. apply (generic_format_bpow beta fexp (mag x - 1)). replace (_ + _)%Z with (mag x : Z) by ring. - assert (fexp (mag x) < mag x)%Z; [|omega]. + assert (fexp (mag x) < mag x)%Z; [|lia]. now apply mag_generic_gt; [|now apply Rgt_not_eq|]. - rewrite Rabs_right. + apply Rlt_trans with x. @@ -884,7 +884,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. rewrite Rmult_plus_distr_r. rewrite <- Fx. rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. bpow_simplify. now rewrite <- Fy. } apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. @@ -904,7 +904,7 @@ intros fexp1 fexp2 x y Hlnx Hlny Fx Fy. destruct (Z.le_gt_cases (fexp1 (mag x)) (fexp1 (mag y))) as [Hle|Hgt]. - now apply (round_round_plus_aux0_aux_aux fexp1). - rewrite Rplus_comm in Hlnx, Hlny |- *. - now apply (round_round_plus_aux0_aux_aux fexp1); [omega| | | |]. + now apply (round_round_plus_aux0_aux_aux fexp1); [lia| | | |]. Qed. (* fexp1 (mag x) - 1 <= mag y : @@ -927,20 +927,20 @@ destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt]. [now apply (mag_plus_separated fexp1)|]. apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]; rewrite Lxy. - + now apply Hexp4; omega. - + now apply Hexp3; omega. + + now apply Hexp4; lia. + + now apply Hexp3; lia. - (* fexp1 (mag x) < mag y *) apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]. destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - + now apply Hexp4; omega. + + now apply Hexp4; lia. + apply Hexp2; apply (mag_le beta y x Py) in Hyx. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - * now apply Hexp3; omega. + * now apply Hexp3; lia. * apply Hexp2. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. Qed. Lemma round_round_plus_aux1_aux : @@ -983,7 +983,7 @@ assert (UB : y * bpow (- fexp (mag x)) < / IZR (beta ^ k)). + bpow_simplify. rewrite bpow_opp. destruct k. - * omega. + * lia. * simpl; unfold Raux.bpow, Z.pow_pos. now apply Rle_refl. * casetype False; apply (Z.lt_irrefl 0). @@ -1003,7 +1003,7 @@ rewrite (Zfloor_imp mx). apply (Rlt_le_trans _ _ _ UB). rewrite bpow_opp. apply Rinv_le; [now apply bpow_gt_0|]. - now rewrite IZR_Zpower; [right|omega]. } + now rewrite IZR_Zpower; [right|lia]. } split. - rewrite <- Rplus_0_r at 1; apply Rplus_le_compat_l. now apply Rlt_le. @@ -1014,7 +1014,7 @@ split. apply Rlt_trans with (bpow (mag y)). + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. - + apply bpow_lt; omega. + + apply bpow_lt; lia. Qed. (* mag y <= fexp1 (mag x) - 2 : round_round_lt_mid applies. *) @@ -1034,18 +1034,18 @@ assert (Hbeta : (2 <= beta)%Z). now apply Zle_bool_imp_le. } intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. assert (Lxy : mag (x + y) = mag x :> Z); - [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |omega]|]. + [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|]. destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). { replace (/2 * /2) with (/4) by field. rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. apply (IZR_le (2 * 2) (beta * (beta * 1))). rewrite Zmult_1_r. - now apply Zmult_le_compat; omega. } -assert (P2 : (0 < 2)%Z) by omega. + now apply Zmult_le_compat; lia. } +assert (P2 : (0 < 2)%Z) by lia. unfold round_round_eq. apply round_round_lt_mid. - exact Vfexp1. @@ -1053,7 +1053,7 @@ apply round_round_lt_mid. - lra. - now rewrite Lxy. - rewrite Lxy. - assert (fexp1 (mag x) < mag x)%Z; [|omega]. + assert (fexp1 (mag x) < mag x)%Z; [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). @@ -1088,10 +1088,10 @@ apply round_round_lt_mid. replace (_ - _) with (- (/ 2)) by lra. apply Ropp_le_contravar. { apply Rle_trans with (bpow (- 1)). - - apply bpow_le; omega. + - apply bpow_le; lia. - unfold Raux.bpow, Z.pow_pos; simpl. apply Rinv_le; [lra|]. - apply IZR_le; omega. } + apply IZR_le; lia. } Qed. (* round_round_plus_aux{0,1} together *) @@ -1115,7 +1115,7 @@ destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 2)) as [Hly|Hly]. rewrite (round_generic beta fexp2). + reflexivity. + now apply valid_rnd_N. - + assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z); [omega|]. + + assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia. now apply (round_round_plus_aux0 fexp1). Qed. @@ -1140,7 +1140,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. + reflexivity. + now apply valid_rnd_N. + apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -1151,7 +1151,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * reflexivity. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -1199,21 +1199,21 @@ assert (Lyx : (mag y <= mag x)%Z); destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - (* mag x - 2 < mag y *) assert (Hor : (mag y = mag x :> Z) - \/ (mag y = mag x - 1 :> Z)%Z); [omega|]. + \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + (* mag y = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heq. apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. + (* mag y = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heqm1. apply Hexp4. @@ -1224,7 +1224,7 @@ destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. + (* mag (x - y) = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - omega. + lia. * now rewrite Lxmy; apply Hexp3. + (* mag (x - y) = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; @@ -1261,8 +1261,8 @@ assert (Hfy : (fexp1 (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - apply Z.le_trans with (fexp1 (mag (x - y))). - + apply Hexp4; omega. - + omega. + + apply Hexp4; lia. + + lia. - now apply Hexp3. Qed. @@ -1289,7 +1289,7 @@ assert (Hfy : (fexp (mag y) < mag y)%Z); destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. - (* bpow (mag x - 1) < x *) assert (Lxy : mag (x - y) = mag x :> Z); - [now apply (mag_minus_separated fexp); [| | | | | |omega]|]. + [now apply (mag_minus_separated fexp); [| | | | | |lia]|]. assert (Rxy : round beta fexp Zceil (x - y) = x). { unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Lxy. @@ -1311,7 +1311,7 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. + apply bpow_le. - omega. + lia. - rewrite <- (Rplus_0_r (IZR _)) at 2. apply Rplus_le_compat_l. rewrite <- Ropp_0; apply Ropp_le_contravar. @@ -1334,9 +1334,9 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. now intro Hx'; rewrite Hx' in Hxy; apply (Rlt_irrefl y). + rewrite Rabs_right; lra. - apply (mag_minus_lb beta x y Px Py). - omega. } + lia. } assert (Hfx1 : (fexp (mag x - 1) < mag x - 1)%Z); - [now apply (valid_exp_large fexp (mag y)); [|omega]|]. + [now apply (valid_exp_large fexp (mag y)); [|lia]|]. assert (Rxy : round beta fexp Zceil (x - y) <= x). { rewrite Xpow at 2. unfold round, F2R, scaled_mantissa, cexp; simpl. @@ -1344,10 +1344,10 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. apply (Rmult_le_reg_r (bpow (- fexp (mag x - 1)%Z))); [now apply bpow_gt_0|]. bpow_simplify. - rewrite <- (IZR_Zpower beta (_ - _ - _)); [|omega]. + rewrite <- (IZR_Zpower beta (_ - _ - _)); [|lia]. apply IZR_le. apply Zceil_glb. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. rewrite Xpow at 1. rewrite Rmult_minus_distr_r. bpow_simplify. @@ -1383,7 +1383,7 @@ intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' Fx Fy. assert (Px := Rlt_trans 0 y x Py Hxy). destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). @@ -1392,7 +1392,7 @@ assert (Bpow2 : bpow (- 2) <= / 2 * / 2). apply Rinv_le; [lra|]. apply (IZR_le (2 * 2) (beta * (beta * 1))). rewrite Zmult_1_r. - now apply Zmult_le_compat; omega. } + now apply Zmult_le_compat; lia. } assert (Ly : y < bpow (mag y)). { apply Rabs_lt_inv. apply bpow_mag_gt. } @@ -1401,19 +1401,19 @@ apply round_round_gt_mid. - exact Vfexp1. - exact Vfexp2. - lra. -- apply Hexp4; omega. -- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|omega]. +- apply Hexp4; lia. +- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia]. apply (valid_exp_large fexp1 (mag x - 1)). - + apply (valid_exp_large fexp1 (mag y)); [|omega]. + + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - + now apply mag_minus_lb; [| |omega]. + + now apply mag_minus_lb; [| |lia]. - unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). ring_simplify. replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. apply Rlt_le_trans with (bpow (fexp1 (mag (x - y)) - 2)). + apply Rle_lt_trans with y; - [now apply round_round_minus_aux2_aux; try assumption; omega|]. + [now apply round_round_minus_aux2_aux; try assumption; lia|]. apply (Rlt_le_trans _ _ _ Ly). now apply bpow_le. + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus]. @@ -1428,7 +1428,7 @@ apply round_round_gt_mid. rewrite Zmult_1_r; apply Rinv_le. lra. now apply IZR_le. - * apply bpow_le; omega. + * apply bpow_le; lia. - intro Hf2'. unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y) @@ -1436,7 +1436,7 @@ apply round_round_gt_mid. ring_simplify. replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. apply Rle_lt_trans with y; - [now apply round_round_minus_aux2_aux; try assumption; omega|]. + [now apply round_round_minus_aux2_aux; try assumption; lia|]. apply (Rlt_le_trans _ _ _ Ly). apply Rle_trans with (bpow (fexp1 (mag (x - y)) - 2)); [now apply bpow_le|]. @@ -1501,12 +1501,12 @@ destruct (Req_dec y x) as [Hy|Hy]. { rewrite (round_generic beta fexp2). - reflexivity. - now apply valid_rnd_N. - - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z); [omega|]. + - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z) by lia. now apply (round_round_minus_aux1 fexp1). } + rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. - * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z); [omega|]. + * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia. now apply (round_round_minus_aux0 fexp1). Qed. @@ -1532,7 +1532,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -1543,7 +1543,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -1626,9 +1626,9 @@ Proof. intros Hprec. unfold FLX_exp. unfold round_round_plus_hyp; split; [|split; [|split]]; -intros ex ey; try omega. +intros ex ey; try lia. unfold Prec_gt_0 in prec_gt_0_. -omega. +lia. Qed. Theorem round_round_plus_FLX : @@ -1683,19 +1683,19 @@ unfold round_round_plus_hyp; split; [|split; [|split]]; intros ex ey. - generalize (Zmax_spec (ex + 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - unfold Prec_gt_0 in prec_gt_0_. generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. Qed. Theorem round_round_plus_FLT : @@ -1753,18 +1753,18 @@ unfold round_round_plus_hyp; split; [|split; [|split]]; intros ex ey. - destruct (Z.ltb_spec (ex + 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. Qed. Theorem round_round_plus_FTZ : @@ -1832,20 +1832,20 @@ destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt]. [now apply (mag_plus_separated fexp1)|]. apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]; rewrite Lxy. - + now apply Hexp4; omega. - + now apply Hexp3; omega. + + now apply Hexp4; lia. + + now apply Hexp3; lia. - (* fexp1 (mag x) < mag y *) apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption]. destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - + now apply Hexp4; omega. + + now apply Hexp4; lia. + apply Hexp2; apply (mag_le beta y x Py) in Hyx. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy. - * now apply Hexp3; omega. + * now apply Hexp3; lia. * apply Hexp2. replace (_ - _)%Z with (mag x : Z) by ring. - omega. + lia. Qed. (* mag y <= fexp1 (mag x) - 1 : round_round_lt_mid applies. *) @@ -1863,16 +1863,16 @@ Lemma round_round_plus_radix_ge_3_aux1 : Proof. intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. assert (Lxy : mag (x + y) = mag x :> Z); - [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |omega]|]. + [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|]. destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Bpow3 : bpow (- 1) <= / 3). { unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rinv_le; [lra|]. now apply IZR_le. } -assert (P1 : (0 < 1)%Z) by omega. +assert (P1 : (0 < 1)%Z) by lia. unfold round_round_eq. apply round_round_lt_mid. - exact Vfexp1. @@ -1880,7 +1880,7 @@ apply round_round_lt_mid. - lra. - now rewrite Lxy. - rewrite Lxy. - assert (fexp1 (mag x) < mag x)%Z; [|omega]. + assert (fexp1 (mag x) < mag x)%Z; [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). @@ -1914,7 +1914,7 @@ apply round_round_lt_mid. apply (Rplus_le_reg_r (- 1)); ring_simplify. replace (_ - _) with (- (/ 3)) by lra. apply Ropp_le_contravar. - now apply Rle_trans with (bpow (- 1)); [apply bpow_le; omega|]. + now apply Rle_trans with (bpow (- 1)); [apply bpow_le; lia|]. Qed. (* round_round_plus_radix_ge_3_aux{0,1} together *) @@ -1940,7 +1940,7 @@ destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 1)) as [Hly|Hly]. rewrite (round_generic beta fexp2). + reflexivity. + now apply valid_rnd_N. - + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z); [omega|]. + + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia. now apply (round_round_plus_radix_ge_3_aux0 fexp1). Qed. @@ -1966,7 +1966,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. + reflexivity. + now apply valid_rnd_N. + apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -1977,7 +1977,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * reflexivity. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -2009,21 +2009,21 @@ assert (Lyx : (mag y <= mag x)%Z); destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. - (* mag x - 2 < mag y *) assert (Hor : (mag y = mag x :> Z) - \/ (mag y = mag x - 1 :> Z)%Z); [omega|]. + \/ (mag y = mag x - 1 :> Z)%Z) by lia. destruct Hor as [Heq|Heqm1]. + (* mag y = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heq. apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. + (* mag y = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - apply Z.le_trans with (mag (x - y)); [omega|]. + apply Z.le_trans with (mag (x - y)); [lia|]. now apply mag_minus. * rewrite Heqm1. apply Hexp4. @@ -2034,7 +2034,7 @@ destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge]. + (* mag (x - y) = mag x *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. * apply Hexp4. - omega. + lia. * now rewrite Lxmy; apply Hexp3. + (* mag (x - y) = mag x - 1 *) apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]; @@ -2071,8 +2071,8 @@ assert (Hfy : (fexp1 (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy]. - apply Z.le_trans with (fexp1 (mag (x - y))). - + apply Hexp4; omega. - + omega. + + apply Hexp4; lia. + + lia. - now apply Hexp3. Qed. @@ -2097,7 +2097,7 @@ intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' assert (Px := Rlt_trans 0 y x Py Hxy). destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); - [now apply Hexp4; omega|]. + [now apply Hexp4; lia|]. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow3 : bpow (- 1) <= / 3). @@ -2113,12 +2113,12 @@ apply round_round_gt_mid. - exact Vfexp1. - exact Vfexp2. - lra. -- apply Hexp4; omega. -- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|omega]. +- apply Hexp4; lia. +- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia]. apply (valid_exp_large fexp1 (mag x - 1)). - + apply (valid_exp_large fexp1 (mag y)); [|omega]. + + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - + now apply mag_minus_lb; [| |omega]. + + now apply mag_minus_lb; [| |lia]. - unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). ring_simplify. @@ -2135,7 +2135,7 @@ apply round_round_gt_mid. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. - now apply IZR_le; omega. + now apply IZR_le; lia. - intro Hf2'. unfold midp'. apply (Rplus_lt_reg_r (/ 2 * (ulp beta fexp1 (x - y) @@ -2164,7 +2164,7 @@ apply round_round_gt_mid. replace (_ - _) with (- / 3) by field. apply Ropp_le_contravar. apply Rle_trans with (bpow (- 1)). - * apply bpow_le; omega. + * apply bpow_le; lia. * unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now apply IZR_le. @@ -2204,12 +2204,12 @@ destruct (Req_dec y x) as [Hy|Hy]. { rewrite (round_generic beta fexp2). - reflexivity. - now apply valid_rnd_N. - - assert (Hf1 : (fexp1 (mag (x - y)) <= mag y)%Z); [omega|]. + - assert (Hf1 : (fexp1 (mag (x - y)) <= mag y)%Z) by lia. now apply (round_round_minus_radix_ge_3_aux1 fexp1). } + rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. - * assert (Hf1 : (fexp1 (mag x) <= mag y)%Z); [omega|]. + * assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia. now apply (round_round_minus_radix_ge_3_aux0 fexp1). Qed. @@ -2236,7 +2236,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fy. - (* x <> 0 *) destruct (Req_dec y 0) as [Zy|Nzy]. @@ -2247,7 +2247,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). - now intros _; apply Hexp4; omega. + now intros _; apply Hexp4; lia. exact Fx. + (* y <> 0 *) assert (Px : 0 < x); [lra|]. @@ -2332,9 +2332,9 @@ Proof. intros Hprec. unfold FLX_exp. unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; -intros ex ey; try omega. +intros ex ey; try lia. unfold Prec_gt_0 in prec_gt_0_. -omega. +lia. Qed. Theorem round_round_plus_radix_ge_3_FLX : @@ -2393,19 +2393,19 @@ unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; intros ex ey. - generalize (Zmax_spec (ex + 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - 1 - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. - unfold Prec_gt_0 in prec_gt_0_. generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ey - prec) emin). - omega. + lia. Qed. Theorem round_round_plus_radix_ge_3_FLT : @@ -2467,18 +2467,18 @@ unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; intros ex ey. - destruct (Z.ltb_spec (ex + 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - 1 - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ey - prec) emin); - omega. + lia. Qed. Theorem round_round_plus_radix_ge_3_FTZ : @@ -2546,11 +2546,11 @@ intros Cmid. destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. - (* generic_format beta fexp1 x *) rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. - now apply (generic_inclusion_mag beta fexp1); [omega|]. + now apply (generic_inclusion_mag beta fexp1); [lia|]. - (* ~ generic_format beta fexp1 x *) assert (Hceil : round beta fexp1 Zceil x = rd + u1); [now apply round_UP_DN_ulp|]. - assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|]. + assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))). + (* x - rd < / 2 * (u1 - u2) *) apply round_round_lt_mid_further_place; try assumption. @@ -2587,7 +2587,7 @@ Proof. intros x Px. rewrite (mag_sqrt beta x Px). generalize (Zdiv2_odd_eqn (mag x + 1)). -destruct Z.odd ; intros ; omega. +destruct Z.odd ; intros ; lia. Qed. Lemma round_round_sqrt_aux : @@ -2638,7 +2638,7 @@ assert (Pb : 0 < b). apply Rlt_Rminus. unfold u2, u1. apply bpow_lt. - omega. } + lia. } assert (Pb' : 0 < b'). { now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. } assert (Hr : sqrt x <= a + b'). @@ -2654,7 +2654,7 @@ assert (Hf1 : (2 * fexp1 (mag (sqrt x)) <= fexp1 (mag (x)))%Z); [destruct (mag_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|]. assert (Hlx : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } @@ -2698,7 +2698,7 @@ destruct (Req_dec a 0) as [Za|Nza]. unfold b'; change (bpow _) with u1. apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra]. apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l. - unfold u2, u1, ulp, cexp; apply bpow_lt; omega. + unfold u2, u1, ulp, cexp; apply bpow_lt; lia. - (* a <> 0 *) assert (Pa : 0 < a); [lra|]. assert (Hla : (mag a = mag (sqrt x) :> Z)). @@ -2731,7 +2731,7 @@ destruct (Req_dec a 0) as [Za|Nza]. * apply pow2_ge_0. * unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. apply Rinv_le; [lra|]. - change 4%Z with (2 * 2)%Z; apply IZR_le, Zmult_le_compat; omega. + change 4%Z with (2 * 2)%Z; apply IZR_le, Zmult_le_compat; lia. * rewrite <- (Rplus_0_l (u1 ^ 2)) at 1; apply Rplus_le_compat_r. apply pow2_ge_0. } assert (Hr' : x <= a * a + u1 * a). @@ -2744,11 +2744,11 @@ destruct (Req_dec a 0) as [Za|Nza]. apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite Fx at 1; bpow_simplify. - rewrite <- IZR_Zpower; [|omega]. + rewrite <- IZR_Zpower; [|lia]. rewrite <- plus_IZR, <- 2!mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR. unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -2787,12 +2787,12 @@ destruct (Req_dec a 0) as [Za|Nza]. apply Rinv_le; [lra|]. apply IZR_le. rewrite <- (Zmult_1_l 2). - apply Zmult_le_compat; omega. + apply Zmult_le_compat; lia. + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra]. unfold pow; do 2 rewrite Rmult_1_r. assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|]. assert (u2 < u1); [|now apply Rmult_lt_compat]. - unfold u1, u2, ulp, cexp; apply bpow_lt; omega. } + unfold u1, u2, ulp, cexp; apply bpow_lt; lia. } apply (Rlt_irrefl (a * a + u1 * a)). apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b). + rewrite <- (Rplus_0_r (a * a + _)) at 1. @@ -2835,7 +2835,8 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. generalize ((proj1 (proj2 Hexp)) 1%Z). replace (_ - 1)%Z with 1%Z by ring. intro Hexp10. - assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10]. + assert (Hf0 : (fexp1 1 < 1)%Z) by lia. + clear Hexp10. apply (valid_exp_large fexp1 1); [exact Hf0|]. apply mag_ge_bpow. rewrite Zeq_minus; [|reflexivity]. @@ -2847,18 +2848,18 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z). { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H). - omega. } + lia. } apply round_round_mid_cases. + exact Vfexp1. + exact Vfexp2. + now apply sqrt_lt_R0. - + omega. - + omega. + + lia. + + lia. + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). Qed. @@ -2878,7 +2879,7 @@ Proof. intros Hprec. unfold FLX_exp. unfold Prec_gt_0 in prec_gt_0_. -unfold round_round_sqrt_hyp; split; [|split]; intro ex; omega. +unfold round_round_sqrt_hyp; split; [|split]; intro ex; lia. Qed. Theorem round_round_sqrt_FLX : @@ -2919,14 +2920,14 @@ unfold Prec_gt_0 in prec_gt_0_. unfold round_round_sqrt_hyp; split; [|split]; intros ex. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - 1 - prec) emin). - omega. + lia. - generalize (Zmax_spec (2 * ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). - omega. + lia. Qed. Theorem round_round_sqrt_FLT : @@ -2969,18 +2970,18 @@ unfold Prec_gt_0 in *. unfold round_round_sqrt_hyp; split; [|split]; intros ex. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); - omega. + lia. - intro H. destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); - omega. + lia. + casetype False. rewrite (Zlt_bool_true _ _ H') in H. - omega. + lia. Qed. Theorem round_round_sqrt_FTZ : @@ -3057,7 +3058,7 @@ assert (Pb : 0 < b). apply Rlt_Rminus. unfold u2, u1, ulp, cexp. apply bpow_lt. - omega. } + lia. } assert (Pb' : 0 < b'). { now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. } assert (Hr : sqrt x <= a + b'). @@ -3073,7 +3074,7 @@ assert (Hf1 : (2 * fexp1 (mag (sqrt x)) <= fexp1 (mag (x)))%Z); [destruct (mag_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|]. assert (Hlx : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } @@ -3117,7 +3118,7 @@ destruct (Req_dec a 0) as [Za|Nza]. unfold b'; change (bpow _) with u1. apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra]. apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l. - unfold u2, u1, ulp, cexp; apply bpow_lt; omega. + unfold u2, u1, ulp, cexp; apply bpow_lt; lia. - (* a <> 0 *) assert (Pa : 0 < a); [lra|]. assert (Hla : (mag a = mag (sqrt x) :> Z)). @@ -3162,11 +3163,11 @@ destruct (Req_dec a 0) as [Za|Nza]. apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite Fx at 1; bpow_simplify. - rewrite <- IZR_Zpower; [|omega]. + rewrite <- IZR_Zpower; [|lia]. rewrite <- plus_IZR, <- 2!mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR. unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x))))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -3203,12 +3204,12 @@ destruct (Req_dec a 0) as [Za|Nza]. unfold Raux.bpow; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rinv_le; [lra|]. - apply IZR_le; omega. + apply IZR_le; lia. + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra]. unfold pow; do 2 rewrite Rmult_1_r. assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|]. assert (u2 < u1); [|now apply Rmult_lt_compat]. - unfold u1, u2, ulp, cexp; apply bpow_lt; omega. } + unfold u1, u2, ulp, cexp; apply bpow_lt; lia. } apply (Rlt_irrefl (a * a + u1 * a)). apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b). + rewrite <- (Rplus_0_r (a * a + _)) at 1. @@ -3263,7 +3264,8 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. generalize ((proj1 (proj2 Hexp)) 1%Z). replace (_ - 1)%Z with 1%Z by ring. intro Hexp10. - assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10]. + assert (Hf0 : (fexp1 1 < 1)%Z) by lia. + clear Hexp10. apply (valid_exp_large fexp1 1); [exact Hf0|]. apply mag_ge_bpow. rewrite Zeq_minus; [|reflexivity]. @@ -3275,18 +3277,18 @@ destruct (Rle_or_lt x 0) as [Npx|Px]. assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z). { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z). { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx]. - - apply (valid_exp_large fexp1 (mag x)); [|omega]. + - apply (valid_exp_large fexp1 (mag x)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - rewrite <- Hlx. now apply mag_generic_gt; [|apply Rgt_not_eq|]. } generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H). - omega. } + lia. } apply round_round_mid_cases. + exact Vfexp1. + exact Vfexp2. + now apply sqrt_lt_R0. - + omega. - + omega. + + lia. + + lia. + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_radix_ge_4_aux Hbeta fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). @@ -3307,7 +3309,7 @@ Proof. intros Hprec. unfold FLX_exp. unfold Prec_gt_0 in prec_gt_0_. -unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intro ex; omega. +unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intro ex; lia. Qed. Theorem round_round_sqrt_radix_ge_4_FLX : @@ -3350,14 +3352,14 @@ unfold Prec_gt_0 in prec_gt_0_. unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (2 * ex - 1 - prec) emin). - omega. + lia. - generalize (Zmax_spec (2 * ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). - omega. + lia. Qed. Theorem round_round_sqrt_radix_ge_4_FLT : @@ -3402,18 +3404,18 @@ unfold Prec_gt_0 in *. unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (2 * ex - 1 - prec) emin); - omega. + lia. - intro H. destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H']. + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); - omega. + lia. + casetype False. rewrite (Zlt_bool_true _ _ H') in H. - omega. + lia. Qed. Theorem round_round_sqrt_radix_ge_4_FTZ : @@ -3479,7 +3481,7 @@ assert (Hf : F2R f = x). rewrite plus_IZR. rewrite Rmult_plus_distr_r. rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. unfold cexp at 2; bpow_simplify. unfold Zminus; rewrite bpow_plus. rewrite (Rmult_comm _ (bpow (- 1))). @@ -3489,11 +3491,11 @@ assert (Hf : F2R f = x). rewrite Ebeta. rewrite (mult_IZR 2). rewrite Rinv_mult_distr; - [|simpl; lra | apply IZR_neq; omega]. + [|simpl; lra | apply IZR_neq; lia]. rewrite <- Rmult_assoc; rewrite (Rmult_comm (IZR n)); rewrite (Rmult_assoc _ (IZR n)). rewrite Rinv_r; - [rewrite Rmult_1_r | apply IZR_neq; omega]. + [rewrite Rmult_1_r | apply IZR_neq; lia]. simpl; fold (cexp beta fexp1 x). rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq. fold u; rewrite Xmid at 2. @@ -3525,12 +3527,12 @@ assert (Hf : F2R f = x). unfold round, F2R, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite Lrd. - rewrite <- (IZR_Zpower _ (_ - _)); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)); [|lia]. rewrite <- mult_IZR. rewrite (Zfloor_imp (Zfloor (x * bpow (- fexp1 (mag x))) * beta ^ (fexp1 (mag x) - fexp2 (mag x)))). + rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. bpow_simplify. now unfold rd. + split; [now apply Rle_refl|]. @@ -3557,7 +3559,7 @@ assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)). apply Hex. now apply Rgt_not_eq. } unfold round_round_eq. -rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|omega]. +rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|lia]. set (x'' := round beta fexp2 (Znearest choice2) x). destruct (Req_dec x'' 0) as [Zx''|Nzx'']; [now rewrite Zx''; rewrite round_0; [|apply valid_rnd_N]|]. @@ -3566,7 +3568,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). destruct (Rlt_or_le x'' (bpow (mag x))). + (* x'' < bpow (mag x) *) rewrite (round_N_small_pos beta fexp1 _ _ (mag x)); - [reflexivity|split; [|exact H0]|omega]. + [reflexivity|split; [|exact H0]|lia]. apply round_large_pos_ge_bpow; [now apply valid_rnd_N| |now apply Hlx]. fold x''; assert (0 <= x''); [|lra]; unfold x''. rewrite <- (round_0 beta fexp2 (Znearest choice2)). @@ -3581,7 +3583,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite mag_bpow. assert (Hf11 : (fexp1 (mag x + 1) = fexp1 (mag x) :> Z)%Z); - [apply Vfexp1; omega|]. + [apply Vfexp1; lia|]. rewrite Hf11. apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x)))); [|now apply Rgt_not_eq; apply bpow_gt_0]. @@ -3590,7 +3592,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). apply Znearest_imp. simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. rewrite Rabs_right; [|now apply Rle_ge; apply bpow_ge_0]. - apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; omega|]. + apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; lia|]. unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop); simpl. @@ -3598,11 +3600,11 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). apply Rinv_lt_contravar. * apply Rmult_lt_0_compat; [lra|]. rewrite mult_IZR; apply Rmult_lt_0_compat; - apply IZR_lt; omega. + apply IZR_lt; lia. * apply IZR_lt. apply (Z.le_lt_trans _ _ _ Hbeta). rewrite <- (Zmult_1_r beta) at 1. - apply Zmult_lt_compat_l; omega. + apply Zmult_lt_compat_l; lia. - (* mag x < fexp2 (mag x) *) casetype False; apply Nzx''. now apply (round_N_small_pos beta _ _ _ (mag x)). @@ -3630,11 +3632,11 @@ assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)). apply Hex. now apply Rgt_not_eq. } rewrite (round_N_small_pos beta fexp1 choice1 x (mag x)); - [|exact Hlx|omega]. + [|exact Hlx|lia]. destruct (Req_dec x'' 0) as [Zx''|Nzx'']; [now rewrite Zx''; rewrite round_0; [reflexivity|apply valid_rnd_N]|]. rewrite (round_N_small_pos beta _ _ x'' (mag x)); - [reflexivity| |omega]. + [reflexivity| |lia]. split. - apply round_large_pos_ge_bpow. + now apply valid_rnd_N. @@ -3680,19 +3682,19 @@ set (u2 := ulp beta fexp2 x). intros Cz Clt Ceq Cgt. destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]]. - (* mag x < fexp1 (mag x) - 1 *) - assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by omega. + assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by lia. now apply round_round_really_zero. - (* mag x = fexp1 (mag x) - 1 *) - assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by omega. + assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by lia. destruct (Rlt_or_le x (bpow (mag x) - / 2 * u2)) as [Hlt'|Hge']. + now apply round_round_zero. + now apply Cz. - (* mag x > fexp1 (mag x) - 1 *) - assert (H : (fexp1 (mag x) <= mag x)%Z) by omega. + assert (H : (fexp1 (mag x) <= mag x)%Z) by lia. destruct (Rtotal_order x (midp fexp1 x)) as [Hlt'|[Heq'|Hgt']]. + (* x < midp fexp1 x *) destruct (Rlt_or_le x (midp fexp1 x - / 2 * u2)) as [Hlt''|Hle'']. - * now apply round_round_lt_mid_further_place; [| | |omega| |]. + * now apply round_round_lt_mid_further_place; [| | |lia| |]. * now apply Clt; [|split]. + (* x = midp fexp1 x *) now apply Ceq. @@ -3703,12 +3705,11 @@ destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]]. - (* generic_format beta fexp1 x *) unfold round_round_eq; rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. - now apply (generic_inclusion_mag beta fexp1); [omega|]. + now apply (generic_inclusion_mag beta fexp1); [lia|]. - (* ~ generic_format beta fexp1 x *) assert (Hceil : round beta fexp1 Zceil x = x' + u1); [now apply round_UP_DN_ulp|]. - assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); - [omega|]. + assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x); [|now apply round_round_gt_mid_further_place]. revert Hle''; unfold midp, midp'; fold x'. @@ -3724,7 +3725,7 @@ Lemma mag_div_disj : Proof. intros x y Px Py. generalize (mag_div beta x y (Rgt_not_eq _ _ Px) (Rgt_not_eq _ _ Py)). -omega. +lia. Qed. Definition round_round_div_hyp fexp1 fexp2 := @@ -3829,7 +3830,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; - [apply valid_exp|omega]. } + [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. @@ -3842,7 +3843,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) bpow_simplify. rewrite (Rmult_comm p). unfold p; bpow_simplify. - rewrite <- IZR_Zpower; [|omega]. + rewrite <- IZR_Zpower; [|lia]. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_le. @@ -3850,7 +3851,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) apply Zlt_le_succ. apply lt_IZR. rewrite mult_IZR. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. @@ -4000,7 +4001,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; - [apply valid_exp|omega]. } + [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. @@ -4016,7 +4017,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)%Z); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia]. do 5 rewrite <- mult_IZR. rewrite <- plus_IZR. rewrite <- minus_IZR. @@ -4026,7 +4027,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_assoc. @@ -4063,7 +4064,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; omega. + apply Hexp; try assumption; rewrite <- Hxy; lia. Qed. Lemma round_round_div_aux2 : @@ -4139,7 +4140,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; - [apply valid_exp|omega]. } + [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. @@ -4213,7 +4214,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; - apply Hexp; try assumption; rewrite <- Hxy; omega. + apply Hexp; try assumption; rewrite <- Hxy; lia. + apply Rge_le; rewrite Fx at 1; apply Rle_ge. rewrite Fy at 1 2. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); @@ -4225,7 +4226,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. - rewrite <- (IZR_Zpower _ (_ - _)%Z); [|omega]. + rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia]. do 5 rewrite <- mult_IZR. do 2 rewrite <- plus_IZR. apply IZR_le. @@ -4233,7 +4234,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. - rewrite IZR_Zpower; [|omega]. + rewrite IZR_Zpower; [|lia]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite (Rmult_assoc _ (IZR mx)). @@ -4379,8 +4380,8 @@ intros Hprec. unfold Prec_gt_0 in prec_gt_0_. unfold FLX_exp. unfold round_round_div_hyp. -split; [now intro ex; omega|]. -split; [|split; [|split]]; intros ex ey; omega. +split; [now intro ex; lia|]. +split; [|split; [|split]]; intros ex ey; lia. Qed. Theorem round_round_div_FLX : @@ -4425,27 +4426,27 @@ unfold round_round_div_hyp. split; [intro ex|split; [|split; [|split]]; intros ex ey]. - generalize (Zmax_spec (ex - prec') emin'). generalize (Zmax_spec (ex - prec) emin). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey - prec) emin). generalize (Zmax_spec (ex - ey - prec') emin'). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey + 1 - prec) emin). generalize (Zmax_spec (ex - ey + 1 - prec') emin'). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey - prec) emin). generalize (Zmax_spec (ex - ey - prec') emin'). - omega. + lia. - generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ey - prec) emin). generalize (Zmax_spec (ex - ey - prec) emin). generalize (Zmax_spec (ex - ey - prec') emin'). - omega. + lia. Qed. Theorem round_round_div_FLT : @@ -4493,27 +4494,27 @@ unfold round_round_div_hyp. split; [intro ex|split; [|split; [|split]]; intros ex ey]. - destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey + 1 - prec) emin); destruct (Z.ltb_spec (ex - ey + 1 - prec') emin'); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. + lia. - destruct (Z.ltb_spec (ex - prec) emin); destruct (Z.ltb_spec (ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec) emin); destruct (Z.ltb_spec (ex - ey - prec') emin'); - omega. + lia. Qed. Theorem round_round_div_FTZ : diff --git a/flocq/Prop/Mult_error.v b/flocq/Prop/Mult_error.v index 57a3856f..f4467025 100644 --- a/flocq/Prop/Mult_error.v +++ b/flocq/Prop/Mult_error.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Error of the multiplication is in the FLX/FLT format *) + +From Coq Require Import Lia. Require Import Core Operations Plus_error. Section Fprop_mult_error. @@ -71,7 +73,7 @@ unfold cexp, FLX_exp. rewrite mag_unique with (1 := Hex). rewrite mag_unique with (1 := Hey). rewrite mag_unique with (1 := Hexy). -cut (exy - 1 < ex + ey)%Z. omega. +cut (exy - 1 < ex + ey)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := proj1 Hexy). rewrite Rabs_mult. @@ -89,7 +91,7 @@ rewrite mag_unique with (1 := Hey). rewrite mag_unique with (1 := Hexy). cut ((ex - 1) + (ey - 1) < exy)%Z. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 Hexy). rewrite Rabs_mult. @@ -163,7 +165,7 @@ apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). -unfold FLX_exp; omega. +unfold FLX_exp; lia. Qed. End Fprop_mult_error. @@ -209,10 +211,10 @@ assumption. apply Rle_trans with (2:=Hxy). apply bpow_le. generalize (prec_gt_0 prec). -clear ; omega. +clear ; lia. rewrite <- (round_FLT_FLX beta emin) in H1. 2:apply Rle_trans with (2:=Hxy). -2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega. +2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; lia. unfold f; rewrite <- H1. apply generic_format_F2R. intros _. @@ -242,7 +244,7 @@ specialize (Ex Hx0). destruct (mag beta y) as (ey,Ey) ; simpl. specialize (Ey Hy0). assert (emin + 2 * prec -1 < ex + ey)%Z. -2: omega. +2: lia. apply (lt_bpow beta). apply Rle_lt_trans with (1:=Hxy). rewrite Rabs_mult, bpow_plus. @@ -262,7 +264,7 @@ intros Hy _. rewrite <- (Rmult_1_l (bpow _)) at 1. apply Rmult_le_compat_r. apply bpow_ge_0. -apply IZR_le; omega. +apply IZR_le; lia. intros H1 H2; contradict H2. replace ny with 0%Z. simpl; ring. @@ -296,7 +298,7 @@ destruct (mag beta x) as (ex,Hx). destruct (mag beta y) as (ey,Hy). simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z. 2: apply Zplus_le_compat; apply Z.le_max_l. -assert (e + 2*prec -1< ex+ey)%Z;[idtac|omega]. +assert (e + 2*prec -1< ex+ey)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (1:=H1). rewrite Rabs_mult, bpow_plus. @@ -327,9 +329,30 @@ apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). -unfold FLT_exp; rewrite Z.max_l; [|omega]; rewrite <- Z.add_max_distr_r. -set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; omega|]. +unfold FLT_exp; rewrite Z.max_l; [|lia]; rewrite <- Z.add_max_distr_r. +set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; lia|]. apply Z.le_max_l. Qed. +Lemma mult_bpow_pos_exact_FLT : + forall x e, + format x -> + (0 <= e)%Z -> + format (x * bpow e)%R. +Proof. +intros x e Fx He. +destruct (Req_dec x 0) as [Zx|Nzx]. +{ rewrite Zx, Rmult_0_l; apply generic_format_0. } +rewrite Fx. +set (mx := Ztrunc _); set (ex := cexp _). +pose (f := {| Fnum := mx; Fexp := ex + e |} : float beta). +apply (generic_format_F2R' _ _ _ f). +{ now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } +intro Nzmx; unfold mx, ex; rewrite <- Fx. +unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). +unfold FLT_exp; rewrite <-Z.add_max_distr_r. +replace (_ - _ + e)%Z with (mag beta x + e - prec)%Z; [ |ring]. +apply Z.max_le_compat_l; lia. +Qed. + End Fprop_mult_error_FLT. diff --git a/flocq/Prop/Plus_error.v b/flocq/Prop/Plus_error.v index 42f80093..514d3aab 100644 --- a/flocq/Prop/Plus_error.v +++ b/flocq/Prop/Plus_error.v @@ -50,19 +50,19 @@ destruct (Zle_or_lt e' e) as [He|He]. exists m. unfold F2R at 2. simpl. rewrite Rmult_assoc, <- bpow_plus. -rewrite <- IZR_Zpower. 2: omega. +rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR, Zrnd_IZR... unfold F2R. simpl. rewrite mult_IZR. rewrite Rmult_assoc. -rewrite IZR_Zpower. 2: omega. +rewrite IZR_Zpower by lia. rewrite <- bpow_plus. apply (f_equal (fun v => IZR m * bpow v)%R). ring. exists ((rnd (IZR m * bpow (e - e'))) * Zpower beta (e' - e))%Z. unfold F2R. simpl. rewrite mult_IZR. -rewrite IZR_Zpower. 2: omega. +rewrite IZR_Zpower by lia. rewrite 2!Rmult_assoc. rewrite <- 2!bpow_plus. apply (f_equal (fun v => _ * bpow v)%R). @@ -326,8 +326,7 @@ exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z. rewrite Fx at 1; unfold F2R; simpl. rewrite mult_IZR, Rmult_assoc. f_equal. -rewrite IZR_Zpower. -2: omega. +rewrite IZR_Zpower by lia. rewrite <- bpow_plus; f_equal; ring. Qed. @@ -351,7 +350,7 @@ case (Zle_or_lt (mag beta (x/IZR beta)) (mag beta y)); intros H1. pose (e:=cexp (x / IZR beta)). destruct (ex_shift x e) as (nx, Hnx); try exact Fx. apply monotone_exp. -rewrite <- (mag_minus1 x Zx); omega. +rewrite <- (mag_minus1 x Zx); lia. destruct (ex_shift y e) as (ny, Hny); try assumption. apply monotone_exp... destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn). @@ -406,11 +405,11 @@ apply V; left. apply lt_mag with beta. now apply Rabs_pos_lt. rewrite <- mag_minus1 in H1; try assumption. -rewrite 2!mag_abs; omega. +rewrite 2!mag_abs; lia. (* . *) destruct U as [U|U]. rewrite U; apply Z.le_trans with (mag beta x). -omega. +lia. rewrite <- mag_abs. apply mag_le. now apply Rabs_pos_lt. @@ -424,13 +423,13 @@ now apply Rabs_pos_lt. rewrite 2!mag_abs. assert (mag beta y < mag beta x - 1)%Z. now rewrite (mag_minus1 x Zx). -omega. +lia. apply cexp_round_ge... apply round_plus_neq_0... contradict H1; apply Zle_not_lt. rewrite <- (mag_minus1 x Zx). replace y with (-x)%R. -rewrite mag_opp; omega. +rewrite mag_opp; lia. lra. now exists n. Qed. @@ -520,7 +519,7 @@ rewrite <- mag_minus1; try assumption. unfold FLT_exp; apply bpow_le. apply Z.le_trans with (2:=Z.le_max_l _ _). destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try omega. +assert (e + prec < n)%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. @@ -568,7 +567,7 @@ unfold cexp. rewrite <- mag_minus1 by easy. unfold FLX_exp; apply bpow_le. destruct (mag beta x) as (n,Hn); simpl. -assert (e + prec < n)%Z; try omega. +assert (e + prec < n)%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v index 5f87bd84..6b8e8f77 100644 --- a/flocq/Prop/Relative.v +++ b/flocq/Prop/Relative.v @@ -147,7 +147,7 @@ apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). exact Hx. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. apply He. @@ -218,7 +218,7 @@ apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. rewrite <- bpow_plus. apply bpow_le. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. @@ -230,7 +230,7 @@ now apply round_le. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). -omega. +lia. Qed. Theorem relative_error_round_F2R_emin : @@ -283,7 +283,7 @@ apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). exact Hx. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. apply He. @@ -375,7 +375,7 @@ apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. rewrite <- bpow_plus. apply bpow_le. generalize (Hmin ex). -omega. +lia. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. @@ -387,7 +387,7 @@ now apply round_le. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). -omega. +lia. Qed. Theorem relative_error_N_round_F2R_emin : @@ -425,7 +425,7 @@ Lemma relative_error_FLX_aux : Proof. intros k. unfold FLX_exp. -omega. +lia. Qed. Variable rnd : R -> Z. @@ -505,7 +505,7 @@ Proof. unfold u_ro; apply (Rmult_lt_reg_l 2); [lra|]. rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l, Rmult_1_r; [|lra]. apply (Rle_lt_trans _ (bpow 0)); - [apply bpow_le; omega|simpl; lra]. + [apply bpow_le; lia|simpl; lra]. Qed. Lemma u_rod1pu_ro_pos : (0 <= u_ro / (1 + u_ro))%R. @@ -659,7 +659,7 @@ Proof. intros k Hk. unfold FLT_exp. generalize (Zmax_spec (k - prec) emin). -omega. +lia. Qed. Variable rnd : R -> Z. @@ -843,7 +843,7 @@ destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice as (eps,(Heps1,Heps2)). now apply FLT_exp_valid. intros; unfold FLT_exp. -rewrite Zmax_left; omega. +lia. rewrite Rabs_right;[assumption|apply Rle_ge; now left]. exists eps; exists 0%R. split;[assumption|split]. @@ -869,14 +869,14 @@ rewrite ulp_neq_0. apply bpow_le. unfold FLT_exp, cexp. rewrite Zmax_right. -omega. +lia. destruct (mag beta x) as (e,He); simpl. assert (e-1 < emin+prec)%Z. apply (lt_bpow beta). apply Rle_lt_trans with (2:=Hx). rewrite <- (Rabs_pos_eq x) by now apply Rlt_le. now apply He, Rgt_not_eq. -omega. +lia. split ; ring. Qed. diff --git a/flocq/Prop/Round_odd.v b/flocq/Prop/Round_odd.v index df2952cc..a433c381 100644 --- a/flocq/Prop/Round_odd.v +++ b/flocq/Prop/Round_odd.v @@ -68,7 +68,7 @@ assert (H0:(Zfloor x <= Zfloor y)%Z) by now apply Zfloor_le. case (Zle_lt_or_eq _ _ H0); intros H1. apply Rle_trans with (1:=Zceil_ub _). rewrite Zceil_floor_neq. -apply IZR_le; omega. +apply IZR_le; lia. now apply sym_not_eq. contradict Hy2. rewrite <- H1, Hx2; discriminate. @@ -503,7 +503,7 @@ Proof. intros x Hx. apply generic_inclusion_mag with fexp; trivial; intros Hx2. generalize (fexpe_fexp (mag beta x)). -omega. +lia. Qed. @@ -525,7 +525,7 @@ rewrite Rmult_assoc, <- bpow_plus. rewrite <- Hg1; unfold F2R. apply f_equal, f_equal. ring. -omega. +lia. split; trivial. split. unfold canonical, cexp. @@ -536,7 +536,7 @@ rewrite Z.even_pow. rewrite Even_beta. apply Bool.orb_true_intro. now right. -omega. +lia. Qed. @@ -713,7 +713,7 @@ rewrite Zmult_1_r; apply Rinv_le. exact Rlt_0_2. apply IZR_le. specialize (radix_gt_1 beta). -omega. +lia. apply Rlt_le_trans with (bpow (fexp e)*1)%R. 2: right; ring. unfold Rdiv; apply Rmult_lt_compat_l. @@ -766,7 +766,7 @@ rewrite Zplus_comm; unfold Zminus; apply f_equal2. rewrite Fexp_Fplus. rewrite Z.min_l. now rewrite Fexp_d. -rewrite Hu'2; omega. +rewrite Hu'2; lia. Qed. Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta, @@ -797,7 +797,7 @@ Lemma fexp_m_eq_0: (0 = F2R d)%R -> Proof with auto with typeclass_instances. intros Y. assert ((fexp (mag beta (F2R u) - 1) <= fexp (mag beta (F2R u))))%Z. -2: omega. +2: lia. destruct (mag beta x) as (e,He). rewrite Rabs_right in He. 2: now left. @@ -812,8 +812,8 @@ ring_simplify (fexp e + 1 - 1)%Z. replace (fexp (fexp e)) with (fexp e). case exists_NE_; intros V. contradict V; rewrite Even_beta; discriminate. -rewrite (proj2 (V e)); omega. -apply sym_eq, valid_exp; omega. +rewrite (proj2 (V e)); lia. +apply sym_eq, valid_exp; lia. Qed. Lemma Fm: generic_format beta fexpe m. @@ -829,7 +829,7 @@ rewrite <- Fexp_d; trivial. rewrite Cd. unfold cexp. generalize (fexpe_fexp (mag beta (F2R d))). -omega. +lia. (* *) destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. apply generic_format_F2R' with g. @@ -838,7 +838,7 @@ intros H; unfold cexp; rewrite Hg2. rewrite mag_m_0; try assumption. apply Z.le_trans with (1:=fexpe_fexp _). generalize (fexp_m_eq_0 Y). -omega. +lia. Qed. @@ -857,7 +857,7 @@ rewrite <- Fexp_d; trivial. rewrite Cd. unfold cexp. generalize (fexpe_fexp (mag beta (F2R d))). -omega. +lia. (* *) destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. apply exists_even_fexp_lt. @@ -866,7 +866,7 @@ rewrite Hg2. rewrite mag_m_0; trivial. apply Z.le_lt_trans with (1:=fexpe_fexp _). generalize (fexp_m_eq_0 Y). -omega. +lia. Qed. @@ -952,7 +952,7 @@ eexists; split. apply sym_eq, Y. simpl; unfold cexp. apply Z.le_lt_trans with (1:=fexpe_fexp _). -omega. +lia. absurd (true=false). discriminate. rewrite <- Hk3, <- Hk'3. @@ -1105,14 +1105,14 @@ intros _; rewrite Zx, round_0... destruct (mag beta x) as (e,He); simpl; intros H. apply mag_unique; split. apply abs_round_ge_generic... -apply FLT_format_bpow... -auto with zarith. +apply generic_format_FLT_bpow... +now apply Z.lt_le_pred. now apply He. assert (V: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta e)%R). apply abs_round_le_generic... -apply FLT_format_bpow... -auto with zarith. +apply generic_format_FLT_bpow... +now apply Zlt_le_weak. left; now apply He. case V; try easy; intros K. assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x (round beta (FLT_exp emin prec) Zrnd_odd x)). diff --git a/flocq/Prop/Sterbenz.v b/flocq/Prop/Sterbenz.v index 746b7026..9594ac5d 100644 --- a/flocq/Prop/Sterbenz.v +++ b/flocq/Prop/Sterbenz.v @@ -67,7 +67,7 @@ rewrite <- F2R_plus. apply generic_format_F2R. intros _. case_eq (Fplus fx fy). -intros mxy exy Pxy. +intros mxy exy Pxy; simpl. rewrite <- Pxy, F2R_plus, <- Hx, <- Hy. unfold cexp. replace exy with (fexp (Z.min ex ey)). -- cgit