show that allocating a single ref is like normal map insertion

theories/base_logic/lib/gen_heap.v

@@ -143,17 +143,17 @@ 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 right_id big_opM_empty; iFrame.
+    - by rewrite left_id big_opM_empty; iFrame.
     - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_r.
       rewrite big_opM_insert //; iFrame.
       assert (σ !! l = None).
       { eapply map_disjoint_Some_r; first by eauto.
         rewrite lookup_insert //. }
-      rewrite -insert_union_r //.
+      rewrite -insert_union_l //.
       iMod (gen_heap_alloc with "Hσ") as "[$ $]"; last done.
       apply lookup_union_None; split; auto.
   Qed.

theories/heap_lang/lang.v

@@ -513,7 +513,14 @@ Proof.
 Qed.
 
 Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
-  state_upd_heap (λ h, h ∪ heap_array l (replicate (Z.to_nat n) v)) σ.
+  state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) ∪ h) σ.
+
+Lemma state_init_heap_singleton l v σ :
+  state_init_heap l 1 v σ = state_upd_heap <[l:=v]> σ.
+Proof.
+  destruct σ as [h p]. rewrite /state_init_heap /=. f_equiv.
+  rewrite right_id insert_union_singleton_l. done.
+Qed.
 
 Inductive head_step : expr → state → list observation → expr → state → list expr → Prop :=
   | RecS f x e σ :

[Robbert Krebbers]

What's the point of swapping the order of arguments here? It's rather strange that σ ##ₘ σ' and σ' ∪ σ are in opposite order now. What was there first made much more sense.

[Ralf Jung]

The new lemma I added just does not hold the other way around. Unions of maps is unfortunately not commutative.

[Robbert Krebbers]

It is commutative if you have σ ##ₘ σ'.

Lemma map_union_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.

[Robbert Krebbers]

Anyway, 2c926d86 is consistent in the order, and killed some occurrences of symmetry. So I guess it's good now :).

[Ralf Jung]

It is commutative if you have σ ##ₘ σ'.

Sure but the caller of the lemma would have to do that -- kind of not the idea of a lemma that is supposed to factor out such work.

Anyway, 2c926d86 is consistent in the order, and killed some occurrences of symmetry. So I guess it's good now :).

That was the hope. :)