diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2020-12-28 15:53:36 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-28 15:53:36 +0100 |
| commit | d4513f41c54869c9b4ba96ab79d50933a1d5c25a (patch) | |
| tree | b5ef5b74c19f386791d1f572c45b6b7af0e90451 /flocq/Core/FLX.v | |
| parent | 548e62be073aa5a7b39d5826cd72681daef7c6a1 (diff) | |
| download | compcert-d4513f41c54869c9b4ba96ab79d50933a1d5c25a.tar.gz compcert-d4513f41c54869c9b4ba96ab79d50933a1d5c25a.zip | |
Update Flocq to 3.4.0 (#383)
Diffstat (limited to 'flocq/Core/FLX.v')
| -rw-r--r-- | flocq/Core/FLX.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v index 803d96ef..78bffba5 100644 --- a/flocq/Core/FLX.v +++ b/flocq/Core/FLX.v @@ -48,7 +48,7 @@ Proof. intros k. unfold FLX_exp. generalize prec_gt_0. -repeat split ; intros ; omega. +repeat split ; intros ; lia. Qed. Theorem FIX_format_FLX : @@ -212,7 +212,7 @@ Proof. case (negligible_exp_spec FLX_exp). intros _; reflexivity. intros n H2; contradict H2. -unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. +unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; lia. Qed. Theorem generic_format_FLX_1 : @@ -221,13 +221,13 @@ Proof. unfold generic_format, scaled_mantissa, cexp, F2R; simpl. rewrite Rmult_1_l, (mag_unique beta 1 1). { unfold FLX_exp. - rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. - rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. + rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. + rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. rewrite <- bpow_plus. now replace (_ + _)%Z with Z0 by ring. } rewrite Rabs_R1; simpl; split; [now right|]. unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt. -assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega. +assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); lia. Qed. Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. @@ -356,7 +356,7 @@ destruct NE_prop as [H|H]. now left. right. unfold FLX_exp. -split ; omega. +split ; lia. Qed. End RND_FLX. |