From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- kvx/ExtValues.v | 93 +++++++++++++++++++++++++++++---------------------------- 1 file changed, 47 insertions(+), 46 deletions(-) (limited to 'kvx/ExtValues.v') diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index a0c10ddd..b4e14898 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -17,6 +17,7 @@ Require Import Coqlib. Require Import Integers. Require Import Values. Require Import Floats ExtFloats. +Require Import Lia. Open Scope Z_scope. @@ -31,9 +32,9 @@ Proof. unfold Z.leb. pose proof (Z.compare_spec x y) as Hspec. inv Hspec. - - rewrite Z.abs_eq; omega. - - rewrite Z.abs_neq; omega. - - rewrite Z.abs_eq; omega. + - rewrite Z.abs_eq; lia. + - rewrite Z.abs_neq; lia. + - rewrite Z.abs_eq; lia. Qed. Inductive shift1_4 : Type := @@ -202,9 +203,9 @@ Proof. intros i H. destruct H as [Hlow Hhigh]. apply Int64.unsigned_repr. - split. { omega. } + split. { lia. } pose proof modulus_fits_64. - omega. + lia. Qed. Theorem divu_is_divlu: forall v1 v2 : val, @@ -237,7 +238,7 @@ Proof. {subst i0_val. pose proof modulus_fits_64. rewrite Zdiv_1_r. - omega. + lia. } destruct (Z.eq_dec i_val 0). { subst i_val. compute. @@ -245,11 +246,11 @@ Proof. intro ABSURD; discriminate ABSURD. } assert ((i_val / i0_val) < i_val). - { apply Z_div_lt; omega. } + { apply Z_div_lt; lia. } split. - { apply Z_div_pos; omega. } + { apply Z_div_pos; lia. } pose proof modulus_fits_64. - omega. + lia. Qed. Theorem modu_is_modlu: forall v1 v2 : val, @@ -280,12 +281,12 @@ Proof. reflexivity. assert((i_val mod i0_val) < i0_val). apply Z_mod_lt. - omega. + lia. split. { apply Z_mod_lt. - omega. } + lia. } pose proof modulus_fits_64. - omega. + lia. Qed. Remark if_zlt_0_half_modulus : @@ -332,7 +333,7 @@ Proof. set (y := Int64.unsigned (Int64.repr x)) in *. rewrite H64. clear H64. - omega. + lia. Qed. (* @@ -375,15 +376,15 @@ Proof. destruct (zlt i0_val Int.half_modulus) as [Hlt_half | Hge_half]. { replace Int.half_modulus with 2147483648 in * by reflexivity. - rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; omega). - destruct (zeq _ _) as [ | Hneq0]; try omega. clear Hneq0. + rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia). + destruct (zeq _ _) as [ | Hneq0]; try lia. clear Hneq0. unfold Val.loword. f_equal. unfold Int64.divs, Int.divs, Int64.loword. unfold Int.signed, Int64.signed. cbn. rewrite if_zlt_min_signed_half_modulus. change Int.half_modulus with 2147483648 in *. - destruct (zlt _ _) as [discard|]; try omega. clear discard. + destruct (zlt _ _) as [discard|]; try lia. clear discard. change (Int64.unsigned (Int64.repr (Int.unsigned (Int.repr Int.min_signed) - Int.modulus))) @@ -391,8 +392,8 @@ Proof. change Int64.half_modulus with 9223372036854775808. change Int64.modulus with 18446744073709551616. cbn. - rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; omega). - destruct (zlt i0_val 9223372036854775808) as [discard |]; try omega. + rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; lia). + destruct (zlt i0_val 9223372036854775808) as [discard |]; try lia. clear discard. change (Int.unsigned (Int.repr Int.min_signed) - Int.modulus) with (-2147483648). destruct (Z.eq_dec i0_val 1) as [H1 | Hnot1]. @@ -418,14 +419,14 @@ Proof. set (delta := (i0_val - Int.modulus)) in *. assert (delta = Int64.modulus*(delta/Int64.modulus)) as Hdelta. { apply Z_div_exact_full_2. - compute. omega. + compute. lia. assumption. } set (k := (delta / Int64.modulus)) in *. change Int64.modulus with 18446744073709551616 in *. change Int.modulus with 4294967296 in *. change Int.half_modulus with 2147483648 in *. change (Int.unsigned Int.mone) with 4294967295 in *. - omega. + lia. } unfold Int.divs, Int64.divs, Val.loword, Int64.loword. change (Int.unsigned (Int.repr Int.min_signed)) with 2147483648. @@ -451,7 +452,7 @@ Proof. intro BIG. unfold Int.signed, Int.unsigned in *. cbn in *. destruct (zlt _ _). - omega. + lia. trivial. Qed. @@ -476,11 +477,11 @@ Proof. subst. rewrite Z.quot_0_l. auto with zarith. - omega. + lia. } assert ((Z.quot a b) < a). { - apply Z.quot_lt; omega. + apply Z.quot_lt; lia. } auto with zarith. Qed. @@ -516,9 +517,9 @@ Proof. change (Int.unsigned (Int.repr Int.min_signed)) with (2147483648) in *. rewrite big_unsigned_signed. change Int.modulus with 4294967296. - omega. + lia. change Int.half_modulus with 2147483648. - omega. + lia. } unfold Int.eq in EXCEPTION. destruct (zeq _ _) in EXCEPTION; try discriminate. @@ -552,8 +553,8 @@ Lemma Z_quot_pos_pos_bound: forall a b m, Proof. intros. split. - { rewrite <- (Z.quot_0_l b) by omega. - apply Z_quot_monotone; omega. + { rewrite <- (Z.quot_0_l b) by lia. + apply Z_quot_monotone; lia. } apply Z.le_trans with (m := a). { @@ -566,10 +567,10 @@ Lemma Z_quot_neg_pos_bound: forall a b m, intros. assert (0 <= - (a ÷ b) <= -m). { - rewrite <- Z.quot_opp_l by omega. - apply Z_quot_pos_pos_bound; omega. + rewrite <- Z.quot_opp_l by lia. + apply Z_quot_pos_pos_bound; lia. } - omega. + lia. Qed. Lemma Z_quot_signed_pos_bound: forall a b, @@ -580,7 +581,7 @@ Proof. destruct (Z_lt_ge_dec a 0). { split. - { apply Z_quot_neg_pos_bound; omega. } + { apply Z_quot_neg_pos_bound; lia. } { eapply Z.le_trans with (m := 0). { apply Z_quot_neg_pos_bound with (m := Int.min_signed); trivial. split. tauto. auto with zarith. @@ -592,9 +593,9 @@ Proof. { eapply Z.le_trans with (m := 0). discriminate. apply Z_quot_pos_pos_bound with (m := Int.max_signed); trivial. - split. omega. tauto. + split. lia. tauto. } - { apply Z_quot_pos_pos_bound; omega. + { apply Z_quot_pos_pos_bound; lia. } } Qed. @@ -608,42 +609,42 @@ Proof. intros. replace b with (-(-b)) by auto with zarith. - rewrite Z.quot_opp_r by omega. + rewrite Z.quot_opp_r by lia. assert (-2147483647 <= (a ÷ - b) <= 2147483648). - 2: omega. + 2: lia. destruct (Z_lt_ge_dec a 0). { replace a with (-(-a)) by auto with zarith. - rewrite Z.quot_opp_l by omega. + rewrite Z.quot_opp_l by lia. assert (-2147483648 <= - a ÷ - b <= 2147483647). - 2: omega. + 2: lia. split. { - rewrite Z.quot_opp_l by omega. + rewrite Z.quot_opp_l by lia. assert (a ÷ - b <= 2147483648). - 2: omega. + 2: lia. { apply Z.le_trans with (m := 0). - rewrite <- (Z.quot_0_l (-b)) by omega. - apply Z_quot_monotone; omega. + rewrite <- (Z.quot_0_l (-b)) by lia. + apply Z_quot_monotone; lia. discriminate. } } assert (- a ÷ - b < -a ). - 2: omega. - apply Z_quot_lt; omega. + 2: lia. + apply Z_quot_lt; lia. } { split. { apply Z.le_trans with (m := 0). discriminate. - rewrite <- (Z.quot_0_l (-b)) by omega. - apply Z_quot_monotone; omega. + rewrite <- (Z.quot_0_l (-b)) by lia. + apply Z_quot_monotone; lia. } { apply Z.le_trans with (m := a). apply Z_quot_le. - all: omega. + all: lia. } } Qed. -- cgit