update documentation and make it match reality

CHANGELOG.md

@@ -70,9 +70,8 @@ lemma.
 
 * Make the `inG` instances for `libG` fields local, so they are only used inside
   the library that defines the `libG`.
-* Prepare for supporting later credits, by adding a resource `£ n` describing
-  ownership of `n` credits that can be eliminated at fancy updates.
-  Note that HeapLang has not yet been equipped with support for later credits.
+* Add infrastructure for supporting later credits, by adding a resource `£ n`
+  describing ownership of `n` credits that can be eliminated at fancy updates.
   + To retain backwards compatibility with the interaction laws of fancy updates
     with the plainly modality (`BiFUpdPlainly`), which are incompatible with
     later credits, the logic has a new parameter of type `has_lc`, which is
@@ -126,14 +125,18 @@ lemma.
   number of steps taken so far. This number is tied to ghost state in the state
   interpretation, which is exposed, updated, and used with new lemmas
   `wp_lb_init`, `wp_lb_update`, and `wp_step_fupdN_lb`. (by Jonas Kastberg Hinrichsen)
-* In line with the support for later credits (see `base_logic`), `heapGS_gen`
-  now takes an additional `has_lc` parameter, and `heapGS` is a short-hand for
-  `heapGS_gen HasLc`. The adequacy statements for HeapLang have been changed
-  accordingly:
+* Make pattern argument of `wp_pure` tactic optional (defaults to wildcard
+  pattern, matching all redexes).
+* In line with the support for later credits (see `base_logic`), the tactic
+  `wp_pure` now takes an optional parameter `credit:"H"` which generates a
+  hypothesis `H` for a single later credit `£ 1` that can be eliminated using
+  `lc_fupd_elim_later`.
+  The typeclass `heapGS_gen` now takes an additional `has_lc` parameter, and
+  `heapGS` is a short-hand for `heapGS_gen HasLc`. The adequacy statements for
+  HeapLang have been changed accordingly:
   + `heap_adequacy` provides `heapGS`, thus enabling the use of later credits.
     This precludes usage of the laws in `BiFUpdPlainly` in the HeapLang instance of Iris.
   + `heap_total` provides `heapGS_gen HasNoLc`.
-  Currently, the primitive laws for HeapLang do not yet provide later credits.
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

docs/heap_lang.md

@@ -55,9 +55,12 @@ that the current goal is of the shape `WP e @ E {{ Q }}`.
 
 Tactics to take one or more pure program steps:
 
-- `wp_pure`: Perform one pure reduction step.  Pure steps are defined by the
-  `PureExec` typeclass and include beta reduction, projections, constructors, as
-  well as unary and binary arithmetic operators.
+- `wp_pure pat credit:"H"`: Perform one pure reduction step. `pat` optionally
+  defines the pattern that the redex has to match; it defaults to `_` (any
+  redex). The `credit:` argument is optional, too; when present, a later credit
+  will be generated in a fresh hypothesis named `"H"`.
+  Pure steps are defined by the `PureExec` typeclass and include beta reduction,
+  projections, constructors, as well as unary and binary arithmetic operators.
 - `wp_pures`: Perform as many pure reduction steps as possible. This
   tactic will **not** reduce lambdas/recs that are hidden behind a definition.
   If the computation reaches a value, the `WP` will be entirely removed and the

iris_heap_lang/proofmode.v

@@ -153,6 +153,8 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
   | _ => fail "wp_pure: not a 'wp'"
   end.
+Tactic Notation "wp_pure" :=
+  wp_pure _.
 
 Tactic Notation "wp_pure" open_constr(efoc) "credit:" constr(H) :=
   iStartProof;

tests/heap_lang.ref

@@ -185,10 +185,11 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
+  P : iProp Σ
   ============================
   "Hcred" : £ 1
   --------------------------------------∗
-  |={⊤}=> True
+  |={⊤}=> ▷ P ={∅}=∗ P
 "test_wp_pure_credit_fail"
      : string
 The command has indeed failed with message:

tests/heap_lang.v

@@ -16,7 +16,7 @@ Section tests.
     ⌜(10 = 4 + 6)%nat⌝ -∗
     WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, ⌜v = #1⌝ }}.
   Proof.
-    iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
+    iIntros "?". wp_alloc l. repeat wp_pure || wp_load || wp_store.
     match goal with
     | |- context [ (10 = 4 + 6)%nat ] => done
     end.
@@ -44,8 +44,8 @@ Section tests.
   Lemma heap_e2_spec E : ⊢ WP heap_e2 @ E [{ v, ⌜v = #2⌝ }].
   Proof.
     iIntros "". rewrite /heap_e2.
-    wp_alloc l as "Hl". Show. wp_alloc l'.
-    wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
+    wp_alloc l as "Hl". Show. wp_alloc l'. do 2 wp_pure.
+    wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
     wp_store. wp_load. done.
   Qed.
 
@@ -338,10 +338,11 @@ Section tests.
   Abort.
 
   Check "test_wp_pure_credit_succeed".
-  Lemma test_wp_pure_credit_succeed :
-    ⊢ WP #42 + #420 {{ v, True }}.
+  Lemma test_wp_pure_credit_succeed P :
+    ⊢ WP #42 + #420 {{ v, ▷ P ={∅}=∗ P }}.
   Proof.
-    wp_pure credit: "Hcred". Show. done.
+    wp_pure credit:"Hcred". Show.
+    iIntros "!> HP". iMod (lc_fupd_elim_later with "Hcred HP"). auto.
   Qed.
 
   Check "test_wp_pure_credit_fail".
@@ -349,7 +350,7 @@ Section tests.
     ⊢ True -∗ WP #42 + #420 {{ v, True }}.
   Proof.
     iIntros "Hcred".
-    Fail wp_pure credit: "Hcred".
+    Fail wp_pure credit:"Hcred".
   Abort.
 
 End tests.