diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /flocq/Core/FLX.v | |
parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
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. |