From 2c926d86e09f9fea1a78c080617bb0a2676eeb00 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 2 Jun 2019 10:34:20 +0200
Subject: [PATCH] gen_heap_alloc_gen: consistent order of argument usage

---
 theories/base_logic/lib/gen_heap.v | 4 ++--
 theories/heap_lang/lang.v          | 1 +
 theories/heap_lang/lifting.v       | 6 ++----
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 9f64f3cb7..62a47dfb3 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -143,12 +143,12 @@ Section gen_heap.
   Qed.
 
   Lemma gen_heap_alloc_gen σ σ' :
-    σ ##ₘ σ' → gen_heap_ctx σ ==∗ gen_heap_ctx (σ' ∪ σ) ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
+    σ' ##ₘ σ → gen_heap_ctx σ ==∗ gen_heap_ctx (σ' ∪ σ) ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
   Proof.
     revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
       iIntros (σ Hσdisj) "Hσ".
     - by rewrite left_id big_opM_empty; iFrame.
-    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_r.
+    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_l.
       rewrite big_opM_insert //; iFrame.
       assert (σ !! l = None).
       { eapply map_disjoint_Some_r; first by eauto.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 653bd26bb..64c807b78 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -512,6 +512,7 @@ Proof.
   move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
 Qed.
 
+(* [h] is added on the right here to make [state_init_heap_singleton] true. *)
 Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
   state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) ∪ h) σ.
 
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 514c533d8..99016dec4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -238,8 +238,7 @@ Proof.
   iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
-  { symmetry.
-    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
+  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
   iModIntro; iSplit; auto.
   iFrame. iApply "HΦ".
@@ -254,8 +253,7 @@ Proof.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
-  { symmetry.
-    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
+  { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
   iModIntro; iSplit; auto.
   iFrame; iSplit; auto. iApply "HΦ".
-- 
GitLab