replacing omega with lia in some file

1 files changed, 47 insertions, 46 deletions

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.