From d7d078a98519ec0227d01f167118b6e747685bb8 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Sat, 16 May 2020 08:48:58 -0500
Subject: [PATCH] Use lia to avoid omega deprecation warnings

Fixes #319
---
 tests/heap_lang.v                 | 10 +++++-----
 tests/ipm_paper.v                 |  4 ++--
 tests/proofmode.v                 |  2 +-
 tests/tree_sum.v                  |  2 +-
 theories/program_logic/adequacy.v |  2 +-
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5f74f0332..c1a914da8 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -104,17 +104,17 @@ Section tests.
     iIntros (Hn) "HΦ".
     iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
     wp_rec. wp_pures. case_bool_decide; wp_if.
-    - iApply ("IH" with "[%] [%] HΦ"); omega.
-    - by assert (n1' = n2 - 1) as -> by omega.
+    - iApply ("IH" with "[%] [%] HΦ"); lia.
+    - by assert (n1' = n2 - 1) as -> by lia.
   Qed.
 
   Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
   Proof.
     iIntros "HΦ". wp_lam.
     wp_op. case_bool_decide.
-    - wp_apply FindPred_spec; first omega. wp_pures.
-      by replace (n - 1) with (- (-n + 2 - 1)) by omega.
-    - wp_apply FindPred_spec; eauto with omega.
+    - wp_apply FindPred_spec; first lia. wp_pures.
+      by replace (n - 1) with (- (-n + 2 - 1)) by lia.
+    - wp_apply FindPred_spec; eauto with lia.
   Qed.
 
   Lemma Pred_user E :
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 1822dfc3b..8539b5d44 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -232,7 +232,7 @@ Section counter_proof.
       wp_cmpxchg_suc. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. rewrite {3}/C; eauto 10.
-    - wp_cmpxchg_fail; first (intros [=]; abstract omega).
+    - wp_cmpxchg_fail; first (intros [=]; abstract lia).
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
@@ -248,6 +248,6 @@ Section counter_proof.
     { iApply own_op. by iFrame. }
     rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
     iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    rewrite /C; eauto 10 with omega.
+    rewrite /C; eauto 10 with lia.
   Qed.
 End counter_proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index a68c061d1..6db8fd04f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -422,7 +422,7 @@ Lemma test_iInduction_wf (x : nat) P Q :
 Proof.
   iIntros "#HP HQ".
   iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
-  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega.
+  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
 Qed.
 
 Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat → nat → PROP) y :
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index d7f1865a9..e2406fac9 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -48,7 +48,7 @@ Proof.
     wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
     wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
     iApply "HΦ". iSplitL "Hl".
-    { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
+    { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by lia. }
     iExists ll, lr, vl, vr. by iFrame.
 Qed.
 
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index a0637add5..52e256df1 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -46,7 +46,7 @@ Proof.
     iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>".
     rewrite !app_length /= !app_length.
     replace (length t1' + S (length t2' + length efs))
-      with (length efs + (length t1' + S (length t2'))) by omega. iFrame.
+      with (length efs + (length t1' + S (length t2'))) by lia. iFrame.
 Qed.
 
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
-- 
GitLab