From 9d820c00ff39670c2cda73d4ccc747f5ab7f59e3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 May 2020 13:53:18 +0200
Subject: [PATCH] Remove `Open Scope Z_scope` in HeapLang.

---
 tests/heap_lang.ref                  |  2 +-
 tests/heap_lang.v                    | 20 +++++++++++---------
 tests/ipm_paper.v                    |  8 ++++----
 tests/tree_sum.v                     |  2 +-
 theories/heap_lang/derived_laws.v    | 10 +++++-----
 theories/heap_lang/lang.v            | 17 ++++++++---------
 theories/heap_lang/lib/array.v       |  4 ++--
 theories/heap_lang/lib/counter.v     | 10 +++++-----
 theories/heap_lang/lib/ticket_lock.v |  4 ++--
 theories/heap_lang/metatheory.v      |  4 ++--
 theories/heap_lang/primitive_laws.v  |  4 ++--
 theories/heap_lang/proofmode.v       |  8 ++++----
 theories/heap_lang/proph_erasure.v   | 12 ++++++------
 13 files changed, 53 insertions(+), 52 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 9fb599d4c..4a40a842e 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -90,7 +90,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Σ : gFunctors
   heapG0 : heapG Σ
   n : Z
-  H : 0 < n
+  H : (0 < n)%Z
   Φ : val → iPropI Σ
   l : loc
   ============================
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5de009c35..68bfa9ab2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -98,14 +98,14 @@ Section tests.
       if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
 
   Lemma FindPred_spec n1 n2 E Φ :
-    n1 < n2 →
+    (n1 < n2)%Z →
     Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
   Proof.
     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Φ"); lia.
-    - by assert (n1' = n2 - 1) as -> by lia.
+    - by assert (n1' = n2 - 1)%Z as -> by lia.
   Qed.
 
   Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
@@ -113,7 +113,7 @@ Section tests.
     iIntros "HΦ". wp_lam.
     wp_op. case_bool_decide.
     - wp_apply FindPred_spec; first lia. wp_pures.
-      by replace (n - 1) with (- (-n + 2 - 1)) by lia.
+      by replace (n - 1)%Z with (- (-n + 2 - 1))%Z by lia.
     - wp_apply FindPred_spec; eauto with lia.
   Qed.
 
@@ -130,12 +130,12 @@ Section tests.
   Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
   Proof.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
-    by replace (S n - 1) with (n:Z) by lia.
+    by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
   Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
   Proof.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
-    by replace (S n - 1) with (n:Z) by lia.
+    by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
 
   Lemma wp_apply_evar e P :
@@ -162,20 +162,22 @@ Section tests.
     ⊢ WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}.
   Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
 
-  Lemma wp_alloc_array n : 0 < n →
+  Lemma wp_alloc_array n :
+    (0 < n)%Z →
     ⊢ {{{ True }}}
         AllocN #n #0
-      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}.
+      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0 }}}.
   Proof.
     iIntros (? Φ) "!> _ HΦ".
     wp_alloc l as "?"; first done.
     by iApply "HΦ".
   Qed.
 
-  Lemma twp_alloc_array n : 0 < n →
+  Lemma twp_alloc_array n :
+    (0 < n)%Z →
     ⊢ [[{ True }]]
         AllocN #n #0
-      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]].
+      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0 }]].
   Proof.
     iIntros (? Φ) "!> _ HΦ".
     wp_alloc l as "?"; first done. Show.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 8539b5d44..b3e0527dd 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -137,7 +137,7 @@ Section M.
   Instance M_valid : Valid M := λ x, x ≠ Bot.
   Instance M_op : Op M := λ x y,
     match x, y with
-    | Auth n, Frag j | Frag j, Auth n => if decide (j ≤ n)%nat then Auth n else Bot
+    | Auth n, Frag j | Frag j, Auth n => if decide (j ≤ n) then Auth n else Bot
     | Frag i, Frag j => Frag (max i j)
     | _, _ => Bot
     end.
@@ -171,9 +171,9 @@ Section M.
 
   Global Instance frag_core_id n : CoreId (Frag n).
   Proof. by constructor. Qed.
-  Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → (j ≤ n)%nat.
+  Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → j ≤ n.
   Proof. simpl. case_decide. done. by intros []. Qed.
-  Lemma auth_frag_op (j n : nat) : (j ≤ n)%nat → Auth n = Auth n ⋅ Frag j.
+  Lemma auth_frag_op (j n : nat) : j ≤ n → Auth n = Auth n ⋅ Frag j.
   Proof. intros. by rewrite /= decide_True. Qed.
 
   Lemma M_update n : Auth n ~~> Auth (S n).
@@ -209,7 +209,7 @@ Section counter_proof.
     rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
     set (N:= nroot .@ "counter").
     iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
-    { iIntros "!>". iExists 0%nat. by iFrame. }
+    { iIntros "!>". iExists 0. by iFrame. }
     iModIntro. rewrite /C; eauto 10.
   Qed.
 
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index e2406fac9..221e86d15 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 lia. }
+    { by replace (sum tl + sum tr + n)%Z with (sum tr + (sum tl + n))%Z by lia. }
     iExists ll, lr, vl, vr. by iFrame.
 Qed.
 
diff --git a/theories/heap_lang/derived_laws.v b/theories/heap_lang/derived_laws.v
index 1e36d1f7a..c2aafac5b 100644
--- a/theories/heap_lang/derived_laws.v
+++ b/theories/heap_lang/derived_laws.v
@@ -78,7 +78,7 @@ Proof.
   rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
   iDestruct (array_app with "Hl") as "[Hl1 Hl]".
   iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
-  assert (off < length vs)%nat as H by (apply lookup_lt_is_Some; by eexists).
+  assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
   rewrite take_length min_l; last by lia. iFrame "Hl2".
   iIntros (w) "Hl2".
   clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
@@ -102,7 +102,7 @@ Proof.
 Qed.
 
 Lemma twp_allocN s E v n :
-  0 < n →
+  (0 < n)%Z →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
@@ -113,7 +113,7 @@ Proof.
   by iApply mapsto_seq_array.
 Qed.
 Lemma wp_allocN s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
@@ -123,7 +123,7 @@ Proof.
 Qed.
 
 Lemma twp_allocN_vec s E v n :
-  0 < n →
+  (0 < n)%Z →
   [[{ True }]]
     AllocN #n v @ s ; E
   [[{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
@@ -133,7 +133,7 @@ Proof.
   iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
 Qed.
 Lemma wp_allocN_vec s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}}
     AllocN #n v @ s ; E
   {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4d821594c..52616a5aa 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -64,7 +64,6 @@ Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.
 
 Module heap_lang.
-Open Scope Z_scope.
 
 (** Expressions and vals. *)
 Definition proph_id := positive.
@@ -526,7 +525,7 @@ Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
   | LtOp => Some $ LitBool (bool_decide (n1 < n2))
   | EqOp => Some $ LitBool (bool_decide (n1 = n2))
   | OffsetOp => None (* Pointer arithmetic *)
-  end.
+  end%Z.
 
 Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   match op with
@@ -580,14 +579,14 @@ Proof. by rewrite /heap_array right_id. Qed.
 
 Lemma heap_array_lookup l vs ow k :
   heap_array l vs !! k = Some ow ↔
-  ∃ j w, 0 ≤ j ∧ k = l +ₗ j ∧ ow = Some w ∧ vs !! (Z.to_nat j) = Some w.
+  ∃ j w, (0 ≤ j)%Z ∧ k = l +ₗ j ∧ ow = Some w ∧ vs !! (Z.to_nat j) = Some w.
 Proof.
   revert k l; induction vs as [|v' vs IH]=> l' l /=.
   { rewrite lookup_empty. naive_solver lia. }
   rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
   - intros [[-> ?] | (Hl & j & w & ? & -> & -> & ?)].
     { eexists 0, _. rewrite loc_add_0. naive_solver lia. }
-    eexists (1 + j), _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
+    eexists (1 + j)%Z, _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
   - intros (j & w & ? & -> & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
     { rewrite loc_add_0; eauto. }
     right. split.
@@ -595,12 +594,12 @@ Proof.
     assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
     { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
     rewrite Hj /= in Hil.
-    eexists (j - 1), _. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
+    eexists (j - 1)%Z, _. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
     auto with lia.
 Qed.
 
 Lemma heap_array_map_disjoint (h : gmap loc (option val)) (l : loc) (vs : list val) :
-  (∀ i, (0 ≤ i) → (i < length vs) → h !! (l +ₗ i) = None) →
+  (∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) →
   (heap_array l vs) ##ₘ h.
 Proof.
   intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
@@ -652,8 +651,8 @@ Inductive head_step : expr → state → list observation → expr → state →
   | ForkS e σ:
      head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
   | AllocNS n v σ l :
-     0 < n →
-     (∀ i, 0 ≤ i → i < n → σ.(heap) !! (l +ₗ i) = None) →
+     (0 < n)%Z →
+     (∀ i, (0 ≤ i)%Z → (i < n)%Z → σ.(heap) !! (l +ₗ i) = None) →
      head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
                []
                (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
@@ -721,7 +720,7 @@ Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
 
 Lemma alloc_fresh v n σ :
   let l := fresh_locs (dom (gset loc) σ.(heap)) in
-  0 < n →
+  (0 < n)%Z →
   head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
             (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
 Proof.
diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index 0de0570c0..b41447205 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -81,7 +81,7 @@ Section proof.
 
   Theorem twp_array_clone stk E l q vl n :
     Z.of_nat (length vl) = n →
-    0 < n →
+    (0 < n)%Z →
     [[{ l ↦∗{q} vl }]]
       array_clone #l #n @ stk; E
     [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }]].
@@ -98,7 +98,7 @@ Section proof.
   Qed.
   Theorem wp_array_clone stk E l q vl n :
     Z.of_nat (length vl) = n →
-    0 < n →
+    (0 < n)%Z →
     {{{ l ↦∗{q} vl }}}
       array_clone #l #n @ stk; E
     {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }}}.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index c7992d8b3..52fc59ab7 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -39,7 +39,7 @@ Section mono_proof.
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
-    { iNext. iExists 0%nat. by iFrame. }
+    { iNext. iExists 0. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
   Qed.
 
@@ -70,7 +70,7 @@ Section mono_proof.
   Qed.
 
   Lemma read_mono_spec l j :
-    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
+    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝ ∧ mcounter l i }}}.
   Proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
@@ -115,10 +115,10 @@ Section contrib_spec.
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (●F O%nat ⋅ ◯F 0%nat)) as (γ) "[Hγ Hγ']";
+    iMod (own_alloc (●F O ⋅ ◯F 0)) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
-    { iNext. iExists 0%nat. by iFrame. }
+    { iNext. iExists 0. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
   Qed.
 
@@ -144,7 +144,7 @@ Section contrib_spec.
 
   Lemma read_contrib_spec γ l q n :
     {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l
-    {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
+    {{{ c, RET #c; ⌜n ≤ c⌝ ∧ ccounter γ q n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 82ce5f2f9..311c7ae21 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -85,11 +85,11 @@ Section proof.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
-    iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
+    iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by apply auth_both_valid. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
-      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
+      iExists 0, 0. iFrame. iLeft. by iFrame. }
     wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 0859f7269..5ff1dcb67 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -93,10 +93,10 @@ Proof.
 Qed.
 
 Lemma heap_closed_alloc σ l n w :
-  0 < n →
+  (0 < n)%Z →
   is_closed_val w →
   map_Forall (λ _ v, from_option is_closed_val true v) (heap σ) →
-  (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
   map_Forall (λ _ v, from_option is_closed_val true v)
              (heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
 Proof.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 9f004324f..ecc290cff 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -397,7 +397,7 @@ Proof.
 Qed.
 
 Lemma twp_allocN_seq s E v n :
-  0 < n →
+  (0 < n)%Z →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   [[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
@@ -415,7 +415,7 @@ Proof.
   - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 Lemma wp_allocN_seq s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 28eae1b6f..739d78cea 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -183,7 +183,7 @@ Implicit Types v : val.
 Implicit Types z : Z.
 
 Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
-  0 < n →
+  (0 < n)%Z →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ' = Some Δ'' ∧
@@ -197,7 +197,7 @@ Proof.
   apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
 Qed.
 Lemma tac_twp_allocN Δ s E j K v n Φ :
-  0 < n →
+  (0 < n)%Z →
   (∀ l, ∃ Δ',
     envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ
     = Some Δ' ∧
@@ -407,7 +407,7 @@ Qed.
 Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ LitV z1)%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (z1 + z2))) Δ' = Some Δ'' →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ' = Some Δ'' →
   envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
 Proof.
@@ -418,7 +418,7 @@ Proof.
 Qed.
 Lemma tac_twp_faa Δ Δ' s E i K l z1 z2 Φ :
   envs_lookup i Δ = Some (false, l ↦ LitV z1)%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (z1 + z2))) Δ = Some Δ' →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ = Some Δ' →
   envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
 Proof.
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index ca5671830..a568a68c3 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -245,8 +245,8 @@ Lemma erased_head_step_head_step_NewProph σ :
   head_steps_to_erasure_of NewProph σ #LitPoison (erase_state σ) [].
 Proof. eexists _, _, _, _; split; first eapply new_proph_id_fresh; done. Qed.
 Lemma erased_head_step_head_step_AllocN n v σ l :
-  0 < n →
-  (∀ i : Z, 0 ≤ i → i < n → erase_heap (heap σ) !! (l +ₗ i) = None) →
+  (0 < n)%Z →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → erase_heap (heap σ) !! (l +ₗ i) = None) →
   head_steps_to_erasure_of
     (AllocN #n v) σ #l (state_init_heap l n (erase_val v) (erase_state σ)) [].
 Proof.
@@ -508,9 +508,8 @@ Proof.
   (** Case split on whether e1 is a [Resolve] expression. *)
   destruct (decide (is_Resolve e1)); last first.
   { (** e1 is not a [Resolve] expression. *)
-    eapply non_resolve_prim_step_matched_by_erased_steps_ectx_item; eauto; [|].
-    - by eapply fill_not_val, val_head_stuck.
-    - intros; eapply (IH K); simpl; eauto with lia. }
+    eapply non_resolve_prim_step_matched_by_erased_steps_ectx_item; [|by eauto..].
+    by eapply fill_not_val, val_head_stuck. }
   (** e1 is a [Resolve] expression. *)
   destruct Ki; simplify_eq/=;
     repeat
@@ -677,7 +676,8 @@ Proof.
 Qed.
 
 Lemma head_step_erased_prim_step_allocN σ l n v:
-  0 < n → (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
+  (0 < n)%Z →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
   ∃ e2' σ2' ef',
     prim_step (AllocN #n (erase_val v)) (erase_state σ) [] e2' σ2' ef'.
 Proof.
-- 
GitLab