gen_heap_alloc_gen: consistent order of argument usage

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.

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) σ.
 

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Φ".