Merge branch 'gen_proofmode' into 'master'

Generalized proofmode

Closes #91, #198, #193, #190, #187, #182, #156, #177, #176, #147, #146, and #154

See merge request FP/iris-coq!66

.gitignore

@@ -9,6 +9,7 @@
 .\#*
 *~
 *.bak
+.coqdeps.d
 .coq-native/
 build-dep/
 Makefile.coq

.gitlab-ci.yml

@@ -18,7 +18,7 @@ variables:
     paths:
     - opamroot/
   only:
-  - master
+  - gen_proofmode
   - /^ci/
   except:
   - triggers
@@ -32,36 +32,28 @@ build-coq.dev:
     OPAM_PINS: "coq version dev"
     VALIDATE: "1"
 
-build-coq.8.8.0:
+build-coq.8.8.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.8.0"
+    OPAM_PINS: "coq version 8.8.dev"
 
-build-coq.8.7.2:
+build-coq.8.8.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.2"
+    OPAM_PINS: "coq version 8.8.0"
     OPAM_PKG: "coq-iris"
+    OPAM_PKG_BRANCH: "gen_proofmode"
     TIMING_PROJECT: "iris"
-    TIMING_CONF: "coq-8.7.2"
+    TIMING_CONF: "coq-8.8.0"
   tags:
   - fp-timing
 
-build-coq.8.7.1:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.7.1"
-
-build-coq.8.7.0:
+build-coq.8.7.2:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.0"
+    OPAM_PINS: "coq version 8.7.2"
 
-build-stdpp.dev:
+build-coq.8.7.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.2   coq-stdpp.dev git https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/#$STDPP_REV"
-  except:
-  only:
-  - triggers
-  - schedules
+    OPAM_PINS: "coq version 8.7.1"

CHANGELOG.md

@@ -7,12 +7,54 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 Changes in and extensions of the theory:
 
+* [#] Change in the definition of WP, so that there is a fancy update between
+  the quantification over the next states and the later modality. This makes it
+  possible to prove more powerful lifting lemmas: The new versions feature an
+  "update that takes a step".
+* [#] Weaken the semantics of CAS in heap_lang to be efficiently implementable:
+  CAS may only be used to compare "unboxed" values that can be represented in a
+  single machine word.
 * [#] Add weakest preconditions for total program correctness.
 * [#] "(Potentially) stuck" weakest preconditions are no longer considered
   experimental.
+* [#] The Löb rule is now a derived rule; it follows from later-intro, later
+  being contractive and the fact that we can take fixpoints of contractive
+  functions.
 
 Changes in Coq:
 
+* An all-new generalized proof mode that abstracts away from Iris!  See
+  <http://iris-project.org/mosel/> for the corresponding paper.  Major new
+  features:
+  - The proof mode can now be used with logics derived from Iris (like iGPS),
+    with non-step-indexed logics and even with non-affine (i.e., linear) logics.
+  - `iModIntro` is more flexible and more powerful, it now also subsumes
+    `iNext` and `iAlways`.
+  - General infrastructure for deriving a logic for monotone predicates over
+    an existing logic (see the paper for more details).
+
+    Developments instantiating the proof mode typeclasses may need significant
+  changes.  For developments just using the proof mode tactics, porting should
+  not be too much effort.  Notable things to port are:
+  - All the BI laws moved from the `uPred` module to the `bi` module.  For
+    example, `uPred.later_equivI` became `bi.later_equivI`.
+  - Big-ops are automatically imported, imports of `iris.base_logic.big_op` have
+    to be removed.
+  - The ⊢ notation can sometimes infer different (but convertible) terms when
+    seraching for the BI to use, which (due to Coq limitations) can lead to
+    failing rewrites, in particular when rewriting at function types.
+* The `iInv` tactic can now be used without the second argument (the name for
+  the closing update).  It will then instead add the obligation to close the
+  invariant to the goal.
+* Added support for defining derived connectives involving n-ary binders using
+  telescopes.
+* The proof mode now more consistently "prettifies" the goal after each tactic.
+  Prettification also simplifies some BI connectives, like conditional
+  modalities and telescope quantifiers.
+* Improved pretty-printing of Iris connectives (in particular WP and fancy
+  updates) when Coq has to line-wrap the output.  This goes hand-in-hand with an
+  improved test suite that also tests pretty-printing.
+* Added a `gmultiset` RA.
 * Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
 * The CMRA axiom `cmra_extend` is now stated in `Type`, using `sigT` instead of
   in `Prop` using `exists`. This makes it possible to define the function space
@@ -28,6 +70,8 @@ Changes in Coq:
   - `cmra_opM_assoc_L` → `cmra_op_opM_assoc_L`
   - `cmra_opM_assoc'` → `cmra_opM_opM_assoc`
 * `namespaces` has been moved to std++.
+* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
+  changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

Makefile.coq.local

+# run tests with main build
+real-all: test
+
+# the test suite
+TESTFILES=$(wildcard tests/*.v)
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.9" > /dev/null && echo 1)
+
+# Can't use pipes because that discards error codes and dash provides no way to control that.
+# Also egrep errors if it doesn't match anything, we have to ignore that.
+# Oh Unix...
+REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
+	$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  TMPFILE="$$(mktemp)" && \
+	  $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
+	  $(if $(MAKE_REF), \
+	    mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
+	    $(if $(COQ_BROKEN), \
+	      true, \
+	      diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
+            ) \
+          ) && \
+	  rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
+	  touch $@

Naming.md

@@ -15,6 +15,7 @@
 * k
 * l
 * m : iGst = ghost state
+* m* = prefix for option
 * n
 * o
 * p

ProofMode.md

@@ -41,8 +41,8 @@ Context management
   the resulting goal.
 - `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
   eliminates it. This tactic is essentially the same as `iDestruct` with the
-  difference that when `pm_trm` is a non-univerisally quantified persistent
-  hypothesis, it will not throw away the hypothesis.
+  difference that when `pm_trm` is a non-universally quantified intuitionistic
+  hypothesis, it will not throw the hypothesis away.
 - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
   hypothesis `P` to the current goal. The specialization pattern `spat`
   specifies which hypotheses will be consumed by proving `P`. The introduction
@@ -108,41 +108,32 @@ Separating logic specific tactics
 
   This tactic finishes the goal in case everything in the conclusion has been
   framed.
-- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
-  `H : P1 ∗ P2`.
+- `iCombine "H1" "H2" as "pat"` : turns `H1 : P1` and `H2 : P2` into
+  `P1 ∗ P2`, on which `iDetruct ... as pat` is called.
 
 Modalities
 ----------
 
-- `iModIntro` : introduction of a modality that is an instance of the
-  `FromModal` type class. Instances include: later, except 0, basic update and
-  fancy update.
+- `iModIntro mod` : introduction of a modality. The type class `FromModal` is
+  used to specify which modalities this tactic should introduce. Instances of
+  that type class include: later, except 0, basic update and fancy update,
+  persistently, affinely, plainly, absorbingly, objectively, and subjectively.
+  The optional argument `mod` can be used to specify what modality to introduce
+  in case of ambiguity, e.g. `⎡|==> P⎤`.
+- `iAlways` : a deprecated alias of `iModIntro`.
+- `iNext n` : an alias of `iModIntro (▷^n P)`.
+- `iNext` : an alias of `iModIntro (▷^1 P)`.
 - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
 
-The persistence and plainness modalities
-----------------------------------------
-
-- `iAlways` : introduce a persistence or plainness modality and the spatial
-  context. In case of a plainness modality, the tactic will prune all persistent
-  hypotheses that are not plain.
-
-The later modality
-------------------
+Induction
+---------
 
-- `iNext n` : introduce `n` laters by stripping that number of laters from all
-  hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
-  conjunct is of the shape `▷^n P`.
 - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
   generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq
   level variables `x1 ... xn`, the hypotheses given by the selection pattern
   `selpat`, and the spatial context.
-
-Induction
----------
-
 - `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
   the Coq term `x`. The Coq introduction pattern is used to name the introduced
   variables. The induction hypotheses are inserted into the persistent context
@@ -170,8 +161,11 @@ Rewriting / simplification
 Iris
 ----
 
-- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
-  for closing the invariant is put in a hypothesis named `Hclose`.
+- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
+   a namespace N or an identifier "H". Open the invariant indicated by S.  The
+   selection pattern `selpat` is used for any auxiliary assertions needed to
+   open the invariant (e.g. for cancelable or non-atomic invariants). The update
+   for closing the invariant is put in a hypothesis named `Hclose`.
 
 Miscellaneous
 -------------
@@ -226,8 +220,8 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an persistence or plainness modality (by calling `iAlways`).
-- `!>` : introduce a modality (by calling `iModIntro`).
+- `!>` : introduce a modality by calling `iModIntro`.
+- `!#` : introduce a modality by calling `iModIntro` (deprecated).
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
 - `//=` : syntactic sugar for `/= //`

README.md

@@ -2,11 +2,17 @@
 
 This is the Coq development of the [Iris Project](http://iris-project.org).
 
-## Prerequisites
+A LaTeX version of the core logic definitions and some derived forms is
+available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
+document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
+
+## Building Iris
+
+### Prerequisites
 
 This version is known to compile with:
 
- - Coq 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0
+ - Coq 8.7.1 / 8.7.2 / 8.8.0
  - A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
 
 For a version compatible with Coq 8.6, have a look at the
@@ -14,7 +20,7 @@ For a version compatible with Coq 8.6, have a look at the
 If you need to work with Coq 8.5, please check out the
 [iris-3.0 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0).
 
-## Working *with* Iris
+### Working *with* Iris
 
 To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or
 newer).  To obtain the latest stable release, you have to add the Coq opam
@@ -31,7 +37,7 @@ Either way, you can now do `opam install coq-iris`.  To fetch updates later, run
 backwards-compatibility, so upgrading Iris may break your Iris-using
 developments.
 
-## Working *on* Iris
+### Working *on* Iris
 
 To work on Iris itself, you need to install its build-dependencies.  Again we
 recommend you do that with opam (1.2.2 or newer).  This requires the following
@@ -65,9 +71,12 @@ followed by `make build-dep`.
   to build Iris, the program logic.   This includes weakest preconditions that
   are defined for any language satisfying some generic axioms, and some derived
   constructions that work for any such language.
-* The folder [proofmode](theories/proofmode) contains the Iris proof mode, which
-  extends Coq with contexts for persistent and spatial Iris assertions. It also
-  contains tactics for interactive proofs in Iris. Documentation can be found in
+* The folder [bi](theories/bi) contains the BI++ laws, as well as derived
+  connectives, laws and constructions that are applicable for general BIS.
+* The folder [proofmode](theories/proofmode) contains
+  [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
+  intuitionistic and spatial BI++ assertions. It also contains tactics for
+  interactive proofs. Documentation can be found in
   [ProofMode.md](ProofMode.md).
 * The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
   language
@@ -79,16 +88,6 @@ followed by `make build-dep`.
   infrastructure. Users of the Iris Coq library should *not* depend on these
   modules; they may change or disappear without any notice.
 
-## Further Documentation
-
-* A LaTeX version of the core logic definitions and some derived forms is
-  available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
-  document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
-* Information on how to set up your editor for unicode input and output is
-  collected in [Editor.md](Editor.md).
-* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md).
-* Naming conventions are documented at [Naming.md](Naming.md).
-
 ## Case Studies
 
 The following is a (probably incomplete) list of case studies that use Iris, and
@@ -101,7 +100,14 @@ that should be compatible with this version:
 * [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
   formalization of logically atomic triples in Iris.
 
-## For Developers: How to update the std++ dependency
+## Notes for Iris Developers
+
+* Information on how to set up your editor for unicode input and output is
+  collected in [Editor.md](Editor.md).
+* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md).
+* Naming conventions are documented at [Naming.md](Naming.md).
+
+### How to update the std++ dependency
 
 * Do the change in std++, push it.
 * Wait for CI to publish a new std++ version on the opam archive, then run
@@ -110,3 +116,13 @@ that should be compatible with this version:
 * Run `make build-dep` (in Iris) to install the new version of std++.
   You may have to do `make clean` as Coq will likely complain about .vo file
   mismatches.
+
+### How to write/update test cases
+
+The files in `tests/` are test cases.  Each of the `.v` files comes with a
+matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
+in selected places in the proofs makes `coqc` print the current goal state.
+This is used to make sure the proof mode prints goals and reduces terms the way
+we expect it to.  You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
+this is useful after adding or removing `Show.` from a test.  If you do this,
+make sure to check the diff for any unexpected changes in the output!

_CoqProject

@@ -25,17 +25,33 @@ theories/algebra/gset.v
 theories/algebra/gmultiset.v
 theories/algebra/coPset.v
 theories/algebra/deprecated.v
+theories/algebra/proofmode_classes.v
+theories/bi/notation.v
+theories/bi/interface.v
+theories/bi/derived_connectives.v
+theories/bi/derived_laws_bi.v
+theories/bi/derived_laws_sbi.v
+theories/bi/plainly.v
+theories/bi/big_op.v
+theories/bi/updates.v
+theories/bi/bi.v
+theories/bi/tactics.v
+theories/bi/monpred.v
+theories/bi/embedding.v
+theories/bi/weakestpre.v
+theories/bi/telescopes.v
+theories/bi/lib/counter_examples.v
+theories/bi/lib/fixpoint.v
+theories/bi/lib/fractional.v
+theories/bi/lib/laterable.v
+theories/bi/lib/atomic.v
+theories/bi/lib/core.v
 theories/base_logic/upred.v
-theories/base_logic/primitive.v
+theories/base_logic/bi.v
 theories/base_logic/derived.v
+theories/base_logic/proofmode.v
 theories/base_logic/base_logic.v
-theories/base_logic/tactics.v
-theories/base_logic/big_op.v
-theories/base_logic/hlist.v
-theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
-theories/base_logic/deprecated.v
-theories/base_logic/fixpoint.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
@@ -48,10 +64,7 @@ theories/base_logic/lib/sts.v
 theories/base_logic/lib/boxes.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
-theories/base_logic/lib/counter_examples.v
-theories/base_logic/lib/fractional.v
 theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/core.v
 theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
@@ -66,10 +79,14 @@ theories/program_logic/ectx_lifting.v
 theories/program_logic/ownp.v
 theories/program_logic/total_lifting.v
 theories/program_logic/total_ectx_lifting.v
+theories/program_logic/atomic.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
 theories/heap_lang/notation.v
+theories/heap_lang/proofmode.v
+theories/heap_lang/adequacy.v
+theories/heap_lang/total_adequacy.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
 theories/heap_lang/lib/assert.v
@@ -77,24 +94,23 @@ theories/heap_lang/lib/lock.v
 theories/heap_lang/lib/spin_lock.v
 theories/heap_lang/lib/ticket_lock.v
 theories/heap_lang/lib/counter.v
-theories/heap_lang/proofmode.v
-theories/heap_lang/adequacy.v
-theories/heap_lang/total_adequacy.v
+theories/heap_lang/lib/atomic_heap.v
+theories/heap_lang/lib/increment.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
+theories/proofmode/ltac_tactics.v
 theories/proofmode/environments.v
+theories/proofmode/reduction.v
 theories/proofmode/intro_patterns.v
 theories/proofmode/spec_patterns.v
 theories/proofmode/sel_patterns.v
 theories/proofmode/tactics.v
 theories/proofmode/notation.v
 theories/proofmode/classes.v
-theories/proofmode/class_instances.v
-theories/tests/heap_lang.v
-theories/tests/one_shot.v
-theories/tests/proofmode.v
-theories/tests/list_reverse.v
-theories/tests/tree_sum.v
-theories/tests/ipm_paper.v
-theories/tests/algebra.v
+theories/proofmode/class_instances_bi.v
+theories/proofmode/class_instances_sbi.v
+theories/proofmode/frame_instances.v
+theories/proofmode/monpred.v
+theories/proofmode/modalities.v
+theories/proofmode/modality_instances.v

opam

@@ -10,6 +10,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
-  "coq" { (>= "8.7.0" & < "8.9~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-06-25.1.0eb9a89b") | (= "dev") }
+  "coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-06-30.1.1a21e908") | (= "dev") }
 ]

theories/tests/algebra.v → tests/algebra.v

@@ -8,3 +8,19 @@ Section tests.
   Solve Obligations with solve_proper.
 
 End tests.
+
+(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
+    Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
+    we cannot [1].  So at least we try to make sure the first solution found
+    is the right one, to not pay performance in the success case [2].
+
+    [1] https://github.com/coq/coq/issues/7916
+    [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
+*)
+Lemma test_setoid_rewrite :
+  exists R, @Reflexive Prop R /\ R = iff.
+Proof.
+  eexists. split.
+  - apply _.
+  - reflexivity.
+Qed.

tests/heap_lang.ref

+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  E : coPset
+  ============================
+  --------------------------------------∗
+  WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  E : coPset
+  l : loc
+  ============================
+  _ : l ↦ #1
+  --------------------------------------∗
+  WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  E : coPset
+  l : loc
+  ============================
+  "Hl" : l ↦ #1
+  --------------------------------------∗
+  WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
+  @ E [{ v, ⌜v = #2⌝ }]
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  l : loc
+  ============================
+  "Hl1" : l ↦{1 / 2} #0
+  "Hl2" : l ↦{1 / 2} #0
+  --------------------------------------∗
+  True
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  l : loc
+  ============================
+  --------------------------------------∗
+  True
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{ _, True }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  Φ : language.val heap_lang → iPropI Σ
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
+  {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  Φ : language.val heap_lang → iPropI Σ
+  E : coPset
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
+  @ E {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    let: "val2" := fun2 "val1" in
+    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
+"not_cas"
+     : string
+The command has indeed failed with message:
+Ltac call to "wp_cas_suc" failed.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.

theories/tests/heap_lang.v → tests/heap_lang.v

-(** This file is essentially a bunch of testcases. *)
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import adequacy.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import lang adequacy proofmode notation.
+(* Import lang *again*. This used to break notation. *)
+From iris.heap_lang Require Import lang.
 Set Default Proof Using "Type".
 
-Section LiftingTests.
+Section tests.
   Context `{heapG Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val → iProp Σ.
@@ -20,13 +19,16 @@ Section LiftingTests.
     end.
   Qed.
 
+  Definition val_scope_test_1 := SOMEV (#(), #()).
+
   Definition heap_e : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
 
   Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
   Proof.
-    iIntros "". rewrite /heap_e.
-    wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
+    iIntros "". rewrite /heap_e. Show.
+    wp_alloc l as "?". wp_let. wp_load. Show.
+    wp_op. wp_store. by wp_load.
   Qed.
 
   Definition heap_e2 : expr :=
@@ -37,7 +39,7 @@ Section LiftingTests.
   Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, ⌜v = #2⌝ }]%I.
   Proof.
     iIntros "". rewrite /heap_e2.
-    wp_alloc l.