diff options
Diffstat (limited to 'flocq/Calc/Round.v')
| -rw-r--r-- | flocq/Calc/Round.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/flocq/Calc/Round.v b/flocq/Calc/Round.v index 5bde6af4..704a1ab2 100644 --- a/flocq/Calc/Round.v +++ b/flocq/Calc/Round.v @@ -19,6 +19,7 @@ COPYING file for more details. (** * Helper function for computing the rounded value of a real number. *) +From Coq Require Import Lia. Require Import Core Digits Float_prop Bracket. Section Fcalc_round. @@ -88,7 +89,7 @@ destruct Px as [Px|Px]. destruct Bx as [Bx1 Bx2]. apply lt_0_F2R in Bx1. apply gt_0_F2R in Bx2. - omega. + lia. Qed. (** Relates location and rounding. *) @@ -585,7 +586,7 @@ apply Zlt_succ. rewrite Zle_bool_true with (1 := Hm). rewrite Zle_bool_false. now case Rlt_bool. -omega. +lia. Qed. Definition truncate_aux t k := @@ -674,7 +675,7 @@ unfold cexp. rewrite mag_F2R_Zdigits. 2: now apply Zgt_not_eq. unfold k in Hk. clear -Hk. -omega. +lia. rewrite <- Hm', F2R_0. apply generic_format_0. Qed. @@ -717,14 +718,14 @@ simpl. apply Zfloor_div. intros H. generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)). -omega. +lia. rewrite scaled_mantissa_generic with (1 := Fx). now rewrite Zfloor_IZR. (* *) split. apply refl_equal. unfold k in Hk. -omega. +lia. Qed. Theorem truncate_correct_partial' : @@ -744,7 +745,7 @@ destruct Zlt_bool ; intros Hk. now apply inbetween_float_new_location. ring. - apply (conj H1). - omega. + lia. Qed. Theorem truncate_correct_partial : @@ -790,7 +791,7 @@ intros x m e l [Hx|Hx] H1 H2. destruct Zlt_bool. intros H. apply False_ind. - omega. + lia. intros _. apply (conj H1). right. @@ -803,7 +804,7 @@ intros x m e l [Hx|Hx] H1 H2. rewrite mag_F2R_Zdigits with (1 := Zm). now apply Zlt_le_weak. - assert (Hm: m = 0%Z). - cut (m <= 0 < m + 1)%Z. omega. + cut (m <= 0 < m + 1)%Z. lia. assert (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R as Hx'. apply inbetween_float_bounds with (1 := H1). rewrite <- Hx in Hx'. @@ -1156,7 +1157,7 @@ exact H1. unfold k in Hk. destruct H2 as [H2|H2]. left. -omega. +lia. right. split. exact H2. @@ -1165,7 +1166,7 @@ inversion_clear H1. rewrite H. apply generic_format_F2R. unfold cexp. -omega. +lia. Qed. End Fcalc_round. |