make inv_mapsto for heap_lang proper definitions because they are higher-order

theories/heap_lang/lifting.v

@@ -22,7 +22,8 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
   fork_post _ := True%I;
 }.
 
-(** Override the notations so that scopes and coercions work out *)
+(** Since we use an [option val] instance of [gen_heap], we need to overwrite
+the notations.  That also helps for scopes and coercions. *)
 Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q (Some v%V))
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l 1%Qp (Some v%V))
@@ -31,13 +32,24 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
-Notation "l ↦□ I" :=
-  (inv_mapsto (L:=loc) (V:=option val) l (from_option I%stdpp%type False))
+(** Same for [gen_inv_heap], except that these are higher-order notations
+so to make rewriting work we need actual definitions here. *)
+Section definitions.
+  Context {L V : Type} `{Countable L} `{!heapG Σ}.
+  Definition inv_mapsto_own (l : loc) (v : val) (I : val → Prop) : iProp Σ :=
+    inv_mapsto_own l (Some v) (from_option I False).
+  Definition inv_mapsto (l : loc) (I : val → Prop) : iProp Σ :=
+    inv_mapsto l (from_option I False).
+End definitions.
+
+Instance: Params (@inv_mapsto_own) 4 := {}.
+Instance: Params (@inv_mapsto) 3 := {}.
+
+Notation inv_heap_inv := (inv_heap_inv loc (option val)).
+Notation "l ↦□ I" := (inv_mapsto l I%stdpp%type)
   (at level 20, format "l  ↦□  I") : bi_scope.
-Notation "l ↦_ I v" :=
-  (inv_mapsto_own (L:=loc) (V:=option val) l (Some v%V) (from_option I%stdpp%type False))
+Notation "l ↦_ I v" := (inv_mapsto_own l v%V I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
-Notation inv_heap_inv := (inv_heap_inv loc (option val)).
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
@@ -260,8 +272,8 @@ Qed.
 
 (** Heap *)
 
-(** We need to adjust the [gen_heap] lemmas because of our value type
-being [option val]. *)
+(** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
+value type being [option val]. *)
 
 Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
 Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
@@ -281,6 +293,19 @@ Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
   ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_mapsto_ne. Qed.
 
+Global Instance inv_mapsto_own_proper l v :
+  Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto_own l v).
+Proof.
+  intros I1 I2 HI. rewrite /inv_mapsto_own. f_equiv=>[] [w|]; last done.
+  simpl. apply HI.
+Qed.
+Global Instance inv_mapsto_proper l :
+  Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto l).
+Proof.
+  intros I1 I2 HI. rewrite /inv_mapsto. f_equiv=>[] [w|]; last done.
+  simpl. apply HI.
+Qed.
+
 Lemma make_inv_mapsto l v (I : val → Prop) E :
   ↑inv_heapN ⊆ E →
   I v →
@@ -289,6 +314,38 @@ Proof. iIntros (??) "#HI Hl". iApply make_inv_mapsto; done. Qed.
 Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦□ I.
 Proof. apply inv_mapsto_own_inv. Qed.
 
+Lemma inv_mapsto_own_acc_strong E :
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, l ↦_I v -∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
+        inv_mapsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
+Proof.
+  iIntros (?) "#Hinv".
+  iMod (inv_mapsto_own_acc_strong with "Hinv") as "Hacc"; first done.
+  iIntros "!> * Hl". iDestruct ("Hacc" with "Hl") as "(% & Hl & Hclose)".
+  iFrame "%∗". iIntros (w) "% Hl". iApply "Hclose"; done.
+Qed.
+
+Lemma inv_mapsto_own_acc E l v I:
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
+Proof.
+  iIntros (?) "#Hinv Hl".
+  iMod (inv_mapsto_own_acc with "Hinv Hl") as "(% & Hl & Hclose)"; first done.
+  iFrame "%∗". iIntros "!>" (w) "% Hl". iApply "Hclose"; done.
+Qed.
+
+Lemma inv_mapsto_acc l I E :
+    ↑inv_heapN ⊆ E →
+    inv_heap_inv -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
+    ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
+Proof.
+  iIntros (?) "#Hinv Hl".
+  iMod (inv_mapsto_acc with "Hinv Hl") as ([v|]) "(% & Hl & Hclose)"; [done| |done].
+  iIntros "!>". iExists (v). iFrame "%∗".
+Qed.
+
 (** The usable rules for [allocN] stated in terms of the [array] proposition
 are derived in te file [array]. *)
 Lemma heap_array_to_seq_meta l vs (n : nat) :