replacing omega with lia in some file

2 files changed, 34 insertions, 32 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index c48af2fc..6143ab55 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -18,6 +18,7 @@
 Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits Axioms.
 Require Archi.
+Require Import Lia.
 
 (** * Comparisons *)
 
@@ -1205,20 +1206,20 @@ Proof.
   simpl.
   pose proof half_modulus_pos as HMOD.
   destruct (zlt 0 half_modulus) as [HMOD' | HMOD'].
-  2: omega.
+  2: lia.
   clear HMOD'.
   destruct (zlt (intval x) half_modulus) as [ LOW | HIGH].
   {
     destruct x as [ix RANGE].
     simpl in *.
-    destruct (zlt ix 0). omega.
+    destruct (zlt ix 0). lia.
     reflexivity.
   }
   destruct (zlt _ _) as [LOW' | HIGH']; trivial.
   destruct x as [ix RANGE].
   simpl in *.
   rewrite half_modulus_modulus in *.
-  omega.
+  lia.
 Qed.
 Local Opaque repr.
 
@@ -2482,20 +2483,20 @@ Proof.
       clear H.
       rewrite two_power_nat_two_p.
       split.
-      omega.
+      lia.
       set (w := (Z.of_nat wordsize)) in *.
       assert ((two_p 2) <= (two_p w)) as MONO.
       {
         apply two_p_monotone.
-        omega.
+        lia.
       }
       change (two_p 2) with 4 in MONO.
-      omega.
+      lia.
     }
     generalize wordsize_max_unsigned.
     fold zwordsize.
     generalize wordsize_pos.
-    omega.
+    lia.
   }
   rewrite unsigned_repr by assumption.
   simpl.
@@ -3677,27 +3678,27 @@ Lemma shr'63:
 Proof.
   intro.
   unfold shr', mone, zero.
-  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega).
+  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
   apply same_bits_eq.
   intros i BIT.
   rewrite testbit_repr by assumption.
-  rewrite Z.shiftr_spec by omega.
-  rewrite bits_signed by omega.
+  rewrite Z.shiftr_spec by lia.
+  rewrite bits_signed by lia.
   simpl.
   change zwordsize with 64 in *.
   destruct (zlt _ _) as [LT | GE].
   {
-    replace i with 0 in * by omega.
+    replace i with 0 in * by lia.
     change (0 + 63) with (zwordsize - 1).
     rewrite  sign_bit_of_signed.
     destruct (lt x _).
-    all: rewrite testbit_repr by (change zwordsize with 64 in *; omega).
+    all: rewrite testbit_repr by (change zwordsize with 64 in *; lia).
     all: simpl; reflexivity.
   }
   change (64 - 1) with (zwordsize - 1).
   rewrite  sign_bit_of_signed.
   destruct (lt x _).
-  all: rewrite testbit_repr by (change zwordsize with 64 in *; omega).
+  all: rewrite testbit_repr by (change zwordsize with 64 in *; lia).
   { symmetry.
     apply Ztestbit_m1.
     tauto.
@@ -3711,11 +3712,11 @@ Lemma shru'63:
 Proof.
   intro.
   unfold shru'.
-  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega).
+  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
   apply same_bits_eq.
   intros i BIT.
   rewrite testbit_repr by assumption.
-  rewrite Z.shiftr_spec by omega.
+  rewrite Z.shiftr_spec by lia.
   unfold lt.
   rewrite signed_zero.
   unfold one, zero.
@@ -3728,15 +3729,15 @@ Proof.
       rewrite sign_bit_of_signed.
       unfold lt.
       rewrite signed_zero.
-      destruct (zlt _ _); try omega.
+      destruct (zlt _ _); try lia.
       reflexivity.
     }
     change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i+63)).
-    rewrite bits_above by (change zwordsize with 64; omega).
+    rewrite bits_above by (change zwordsize with 64; lia).
     rewrite Ztestbit_1.
     destruct (zeq i 0); trivial.
     subst i.
-    omega.
+    lia.
   }
   destruct (zeq i 0) as [IZERO | INONZERO].
   { subst i.
@@ -3745,14 +3746,14 @@ Proof.
     unfold lt.
     rewrite signed_zero.
     rewrite bits_zero.
-    destruct (zlt _ _); try omega.
+    destruct (zlt _ _); try lia.
     reflexivity.
   }
   change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)).
   rewrite bits_zero.
   apply bits_above.
   change zwordsize with 64.
-  omega.
+  lia.
 Qed.
   
 Theorem shrx'1_shr':
diff --git a/lib/IterList.v b/lib/IterList.v
index bde47068..d28124c7 100644
--- a/lib/IterList.v
+++ b/lib/IterList.v
@@ -1,4 +1,5 @@
 Require Import Coqlib.
+Require Import Lia.
 
 (** TODO: are these def and lemma already defined in the standard library ?
 
@@ -55,17 +56,17 @@ Qed.
 Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat.
 Proof.
   unfold iter_tail; induction n; auto.
-  intros l; destruct l. { simpl; omega. }
+  intros l; destruct l. { simpl; lia. }
   intros; simpl. erewrite IHn; eauto.
-  simpl in *; omega.
+  simpl in *; lia.
 Qed.
 
 Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l).
 Proof.
   unfold iter_tail; induction n; simpl.
-  - intros l; destruct l; simpl; omega || eauto.
+  - intros l; destruct l; simpl; lia || eauto.
   - intros l H; destruct (IHn (tl l)) as (x & H1).
-    + destruct l; simpl in *; try omega.
+    + destruct l; simpl in *; try lia.
     + rewrite H1; eauto.
 Qed.
 
@@ -74,20 +75,20 @@ Proof.
   intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto.
   rewrite EQ.
   rewrite (length_iter_tail n2 l); eauto.
-  omega.
+  lia.
 Qed.
 
 Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat.
 Proof.
-  destruct (le_lt_dec n (List.length l)); try omega.
-  intros; exploit (iter_tail_inject1 n (length l) l); try omega.
+  destruct (le_lt_dec n (List.length l)); try lia.
+  intros; exploit (iter_tail_inject1 n (length l) l); try lia.
   rewrite iter_tail_reach_nil. auto.
 Qed.
 
 Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l).
 Proof.
   induction l; auto.
-  rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega.
+  rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. lia.
 Qed.
 
 Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l).
@@ -99,13 +100,13 @@ Lemma is_tail_list_nth_z A (l1 l2: list A):
   is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
 Proof.
   induction 1; simpl.
-  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
+  - replace (list_length_z c - list_length_z c) with 0; lia || auto.
   - assert (X: list_length_z (i :: c2) > list_length_z c1).
     { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
       exploit is_tail_bound; simpl; eauto.
-      omega. }
-    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
+      lia. }
+    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try lia.
     replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
     rewrite list_length_z_cons.
-    omega.
+    lia.
 Qed.