replacing omega with lia in some file

2 files changed, 15 insertions, 13 deletions

diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v
index 404c2a96..c8eadbd7 100644
--- a/scheduling/postpass_lib/Machblock.v
+++ b/scheduling/postpass_lib/Machblock.v
@@ -29,6 +29,7 @@ Require Import Conventions.
 Require Stacklayout.
 Require Import Mach.
 Require Import Linking.
+Require Import Lia.
 
 (** * Abstract Syntax *)
 
@@ -87,9 +88,9 @@ Lemma size_null b:
 Proof.
   destruct b as [h b e]. cbn. unfold size. cbn.
   intros H.
-  assert (length h = 0%nat) as Hh; [ omega |].
-  assert (length b = 0%nat) as Hb; [ omega |].
-  assert (length_opt e = 0%nat) as He; [ omega|].
+  assert (length h = 0%nat) as Hh; [ lia |].
+  assert (length b = 0%nat) as Hb; [ lia |].
+  assert (length_opt e = 0%nat) as He; [ lia|].
   repeat split.
   destruct h; try (cbn in Hh; discriminate); auto.
   destruct b; try (cbn in Hb; discriminate); auto.
diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v
index d121a54b..1d6c6e18 100644
--- a/scheduling/postpass_lib/Machblockgenproof.v
+++ b/scheduling/postpass_lib/Machblockgenproof.v
@@ -30,6 +30,7 @@ Require Import Linking.
 Require Import Machblock.
 Require Import Machblockgen.
 Require Import ForwardSimulationBlock.
+Require Import Lia.
 
 Ltac subst_is_trans_code H :=
   rewrite is_trans_code_inv in H;
@@ -318,12 +319,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe
 
 Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
 Proof.
-  unfold add_label, size; cbn; omega.
+  unfold add_label, size; cbn; lia.
 Qed.
 
 Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1.
 Proof.
-  intro H. unfold add_basic, size; rewrite H; cbn. omega.
+  intro H. unfold add_basic, size; rewrite H; cbn. lia.
 Qed.
 
 
@@ -341,13 +342,13 @@ Proof.
   remember (trans_code (i::c)) as bl.
   rewrite <- is_trans_code_inv in Heqbl.
   inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl.
-  - rewrite size_add_to_newblock; omega.
+  - rewrite size_add_to_newblock; lia.
   - rewrite size_add_label;
     subst_is_trans_code H.
-    omega.
+    lia.
   - rewrite size_add_basic; auto.
     subst_is_trans_code H. 
-    omega.
+    lia.
 Qed.
 
 Local Hint Resolve dist_end_block_code_simu_mid_block: core.
@@ -357,9 +358,9 @@ Lemma size_nonzero c b bl:
   is_trans_code c (b :: bl) -> size b <> 0.
 Proof.
    intros H; inversion H; subst.
-   - rewrite size_add_to_newblock; omega.
-   - rewrite size_add_label; omega.
-   - rewrite size_add_basic; auto; omega.
+   - rewrite size_add_to_newblock; lia.
+   - rewrite size_add_label; lia.
+   - rewrite size_add_basic; auto; lia.
 Qed.
 
 Inductive is_header: list label -> Mach.code -> Mach.code -> Prop :=
@@ -633,7 +634,7 @@ Proof.
       unfold dist_end_block_code. 
       subst_is_trans_code Heqtc.
       lapply (size_nonzero c b bl); auto.
-      omega.
+      lia.
     }
     rewrite X in H; unfold size in H.
     (* decomposition of starN in 3 parts: header + body + exit *)
@@ -697,7 +698,7 @@ Proof.
   apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state).
 (* simu_mid_block *)
   - intros s1 t s1' H1 H2.
-    destruct H1; cbn in * |- *; omega || (intuition auto);
+    destruct H1; cbn in * |- *; lia || (intuition auto);
     destruct H2; eapply cfi_dist_end_block; cbn; eauto.
 (* public_preserved *)
   - apply senv_preserved.