apply review suggestions

tests/heap_lang.ref

@@ -118,10 +118,10 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  f : val → Prop
-  Heq : ∀ v : val, f v ↔ f #true
+  I : val → Prop
+  Heq : ∀ v : val, I v ↔ I #true
   ============================
-  ⊢ l ↦□ (λ _ : val, f #true)
+  ⊢ l ↦□ (λ _ : val, I #true)
 1 subgoal
   
   Σ : gFunctors

tests/heap_lang.v

@@ -228,9 +228,9 @@ Section inv_mapsto_tests.
   Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
 
   (* Make sure [setoid_rewrite] works. *)
-  Lemma inv_mapsto_setoid_rewrite (l : loc) (f : val → Prop) :
-    (∀ v, f v ↔ f #true) →
-    ⊢ l ↦□ (λ v, f v).
+  Lemma inv_mapsto_setoid_rewrite (l : loc) (I : val → Prop) :
+    (∀ v, I v ↔ I #true) →
+    ⊢ l ↦□ (λ v, I v).
   Proof.
     iIntros (Heq). setoid_rewrite Heq. Show.
   Abort.

theories/base_logic/lib/gen_inv_heap.v

@@ -14,7 +14,7 @@ it is that they are reading in that case. In that extreme case, the invariant
 may just be [True].
 
 Since invariant locations cannot be deallocated, they only make sense when
-modelling languages with garbage collection.  HeapLang can be used to model
+modeling languages with garbage collection.  HeapLang can be used to model
 either language by choosing whether or not to use the [Free] operation.  By
 making "invariant" locations a separate assertion, we can keep all the other
 proofs that do not need it conservative.  *)

theories/heap_lang/lang.v

@@ -18,7 +18,7 @@ Noteworthy design choices:
 - Even after deallocating a location, the heap remembers that these locations
   were previously allocated and makes sure they do not get reused. This is
   necessary to ensure soundness of the [meta] feature provided by [gen_heap].
-  Also, unlike in langauges like C, allocated and deallocated "blocks" do not
+  Also, unlike in languages like C, allocated and deallocated "blocks" do not
   have to match up: you can allocate a large array of locations and then
   deallocate a hole out of it in the middle.
 

theories/heap_lang/lifting.v

@@ -32,10 +32,11 @@ 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.
 
-(** Same for [gen_inv_heap], except that these are higher-order notations
-so to make rewriting work we need actual definitions here. *)
+(** Same for [gen_inv_heap], except that these are higher-order notations so to
+make setoid rewriting in the predicate [I] work we need actual definitions
+here. *)
 Section definitions.
-  Context {L V : Type} `{Countable L} `{!heapG Σ}.
+  Context `{!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 Σ :=
@@ -48,7 +49,7 @@ 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 v%V I%stdpp%type)
+Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
@@ -296,13 +297,13 @@ 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.
+  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.
+  intros I1 I2 HI. rewrite /inv_mapsto. f_equiv=>-[w|]; last done.
   simpl. apply HI.
 Qed.
 
@@ -315,21 +316,21 @@ 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)).
+  ↑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)".
+  iIntros "!>" (l v I) "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)).
+  ↑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.
@@ -337,8 +338,8 @@ Proof.
 Qed.
 
 Lemma inv_mapsto_acc l I E :
-    ↑inv_heapN ⊆ E →
-    inv_heap_inv -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
+  ↑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".

theories/heap_lang/proofmode.v

@@ -539,7 +539,7 @@ Tactic Notation "wp_free" :=
     [solve_mapsto ()
     |pm_reflexivity
     |wp_finish]
-  | _ => fail "wp_load: not a 'wp'"
+  | _ => fail "wp_free: not a 'wp'"
   end.
 
 Tactic Notation "wp_load" :=