replacing omega with lia in some file

1 files changed, 22 insertions, 21 deletions

diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 03d863a3..004cfd5c 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -38,6 +38,7 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Asmblockprops.
+Require Import Lia.
 
 Module MB:=Machblock.
 Module AB:=Asmblock.
@@ -395,7 +396,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
 Lemma code_tail_pos:
   forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
 Proof.
-  induction 1. omega. generalize (size_positive bi); intros; omega.
+  induction 1. lia. generalize (size_positive bi); intros; lia.
 Qed.
 
 Lemma find_bblock_tail:
@@ -405,10 +406,10 @@ Lemma find_bblock_tail:
 Proof.
   induction c1; simpl; intros.
   inversion H.  
-  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
   destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
-  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
   eauto.
 Qed.
 
@@ -422,13 +423,13 @@ Proof.
   induction 1; intros.
   - subst; eauto.
   - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
-    omega.
+    lia.
 Qed.
 
 Lemma size_blocks_pos c: 0 <= size_blocks c.
 Proof.
-  induction c as [| a l ]; simpl; try omega.
-  generalize (size_positive a); omega.
+  induction c as [| a l ]; simpl; try lia.
+  generalize (size_positive a); lia.
 Qed.
 
 Remark code_tail_positive:
@@ -436,15 +437,15 @@ Remark code_tail_positive:
   code_tail ofs fn c -> 0 <= ofs.
 Proof.
   induction 1; intros; simpl.
-  - omega.
-  - generalize (size_positive bi). omega.
+  - lia.
+  - generalize (size_positive bi). lia.
 Qed.
 
 Remark code_tail_size:
   forall fn ofs c,
   code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
 Proof.
-  induction 1; intros; simpl; try omega.
+  induction 1; intros; simpl; try lia.
 Qed.
 
 Remark code_tail_bounds fn ofs c:
@@ -453,7 +454,7 @@ Proof.
   intro H; 
   exploit code_tail_size; eauto.
   generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
-  omega.
+  lia.
 Qed.
 
 Local Hint Resolve code_tail_next: core.
@@ -470,8 +471,8 @@ Proof.
   intros.
   rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
   - rewrite Ptrofs.unsigned_repr; eauto.
-    omega.
-  - rewrite Ptrofs.unsigned_repr; omega.
+    lia.
+  - rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 (** The [find_label] function returns the code tail starting at the
@@ -505,12 +506,12 @@ Proof.
   simpl; intros until c'.
   case (is_label lbl a).
   - intros. inv H. exists pos. split; auto. split.
-    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
-    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+    replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
+    generalize (size_blocks_pos c). generalize (size_positive a). lia.
   - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
-  constructor. auto. generalize (size_positive a). omega.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
+  constructor. auto. generalize (size_positive a). lia.
 Qed.
 
 (** Predictor for return addresses in generated Asm code.
@@ -589,7 +590,7 @@ Proof.
     exists (Ptrofs.repr ofs). red; intros.
     rewrite Ptrofs.unsigned_repr. congruence.
     exploit code_tail_bounds; eauto.
-    intros; apply transf_function_len in TF. omega.
+    intros; apply transf_function_len in TF. lia.
   + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
@@ -613,7 +614,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
 Remark code_tail_no_bigger:
   forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
 Proof.
-  induction 1; simpl; omega.
+  induction 1; simpl; lia.
 Qed.
 
 Remark code_tail_unique:
@@ -621,8 +622,8 @@ Remark code_tail_unique:
   code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
 Proof.
   induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
   f_equal. eauto.
 Qed.