replacing omega with lia in some file

1 files changed, 8 insertions, 7 deletions

diff --git a/kvx/PostpassSchedulingproof.v b/kvx/PostpassSchedulingproof.v
index c290387b..937b3be6 100644
--- a/kvx/PostpassSchedulingproof.v
+++ b/kvx/PostpassSchedulingproof.v
@@ -20,6 +20,7 @@ Require Import Asmblockgenproof0 Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -93,12 +94,12 @@ Proof.
     rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
     assert (size bb = size a + size b).
     { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
-      repeat (rewrite Nat2Z.inj_add). omega. }
+      repeat (rewrite Nat2Z.inj_add). lia. }
     clear EXA H0 H1. rewrite H in EXEB.
     assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
     rewrite H0. rewrite <- pc_set_add; auto.
-    exploit size_positive. instantiate (1 := a). intro. omega.
-    exploit size_positive. instantiate (1 := b). intro. omega.
+    exploit size_positive. instantiate (1 := a). intro. lia.
+    exploit size_positive. instantiate (1 := b). intro. lia.
 Qed.
 
 Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
@@ -140,7 +141,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma symbols_preserved:
@@ -224,7 +225,7 @@ Proof.
     + apply IHlbb in H. destruct H as (c & TAIL). exists c.
       enough (pos = pos - size a + size a) as ->.
       apply code_tail_S; auto.
-      omega.
+      lia.
 Qed.
 
 Lemma code_tail_head_app:
@@ -291,7 +292,7 @@ Lemma verified_schedule_not_empty:
   verified_schedule bb = OK lbb -> lbb <> nil.
 Proof.
   intros. apply verified_schedule_size in H.
-  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
+  pose (size_positive bb). assert (size_blocks lbb > 0) by lia. clear H g.
   destruct lbb; simpl in *; discriminate.
 Qed.
 
@@ -356,7 +357,7 @@ Proof.
   induction tc.
   - intros. simpl in H. discriminate.
   - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
-    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + inv H. assert (k = k') by lia. subst. reflexivity.
     + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
 Qed.