build/opam-pins.sh

-#!/bin/bash
-set -e
-## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
-## Usage:
-##   ./opam-pins.sh < opam.pins
-
-if ! which curl >/dev/null; then
-    echo "opam-pins needs curl. Please install curl and try again."
-    exit 1
-fi
-
-# Process stdin
-while read PACKAGE URL HASH; do
-    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
-        echo "[opam-pins] Recursing into $URL"
-        # an MPI URL -- try doing recursive pin processing
-        curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
-    fi
-    if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
-        echo "[opam-pins] $PACKAGE already at commit $HASH"
-    else
-        echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
-        opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
-        echo
-    fi
-done

coq-iris-deprecated.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "Deprecated Iris libraries"
+description: """
+This package contains libraries that have been deprecated from Iris, and are planned to be
+entirely removed at some point.
+"""
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_deprecated" "-j%{jobs}%"]
+install: ["./make-package" "iris_deprecated" "install"]

coq-iris-heap-lang.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "The canonical example language for Iris"
+description: """
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
+"""
+tags: [
+  "logpath:iris.heap_lang"
+]
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
+install: ["./make-package" "iris_heap_lang" "install"]

coq-iris-unstable.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "Unfinished Iris libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in Iris, but more
+work is needed before they are ready for this.
+"""
+
+depends: [
+  "coq-iris" {= version}
+  "coq-iris-heap-lang" {= version}
+]
+
+build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
+install: ["./make-package" "iris_unstable" "install"]

coq-iris.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+description: """
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
+"""
+tags: [
+  "logpath:iris.prelude"
+  "logpath:iris.algebra"
+  "logpath:iris.si_logic"
+  "logpath:iris.bi"
+  "logpath:iris.proofmode"
+  "logpath:iris.base_logic"
+  "logpath:iris.program_logic"
+]
+
+depends: [
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2025-03-30.0.9274984b") | (= "dev") }
+]
+
+build: ["./make-package" "iris" "-j%{jobs}%"]
+install: ["./make-package" "iris" "install"]

coq-lint.sh

+#!/bin/bash
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
+    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
+    echo "Please add 'Global' or 'Local' as appropriate."
+    echo
+    exit 1
+fi

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q iris iris
+-Q _build/default/iris iris
+-Q iris_heap_lang iris.heap_lang
+-Q _build/default/iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q _build/default/iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+-Q _build/default/iris_deprecated iris.deprecated
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build iris/prelude/options.vo`. To build
+only the `iris` folder, you can do `dune build iris`.

docs/editor.md

+Here we collect some information on how to set up your editor to properly input
+and output the unicode characters used throughout Iris.
+
+If you really want to, you can also avoid having to type unicode characters by
+importing `iris.bi.ascii`.  That enables parsing-only ASCII alternatives to many
+unicode notations. (Feel free to report an issue when you notice that a notation
+is missing.)  The easiest way to learn the ASCII syntax is to
+[read this file](../iris/bi/ascii.v).
+Note however that this will make your code harder to read and work on for Iris
+developers that are used to our default unicode notation---generally, our
+recommendation is to use the unicode syntax whenever possible. In particular,
+Unicode syntax is required for MRs to Iris itself and other Iris-managed
+repositories.
+
+## General: Unicode Fonts
+
+Most editors will just use system fonts for rendering unicode characters and do
+not need further configuration once the fonts are installed.  Here are some
+combinations of fonts that are known to give readable results (i.e., each of
+these sets of fonts covers all the required characters):
+
+* Fira Mono, DejaVu Mono, Symbola
+
+## Emacs
+
+### Unicode Input
+
+First, install `math-symbol-lists` by doing `M-x package-install math-symbol-lists`.
+
+Next, add the following to your `~/.emacs` to configure an input method based
+on the math symbol list, and with some custom aliases for symbols used a lot in Iris:
+```
+;; Input of unicode symbols
+(require 'math-symbol-lists)
+; Automatically use math input method for Coq files
+(add-hook 'coq-mode-hook (lambda () (set-input-method "math")))
+; Input method for the minibuffer
+(defun my-inherit-input-method ()
+  "Inherit input method from `minibuffer-selected-window'."
+  (let* ((win (minibuffer-selected-window))
+         (buf (and win (window-buffer win))))
+    (when buf
+      (activate-input-method (buffer-local-value 'current-input-method buf)))))
+(add-hook 'minibuffer-setup-hook #'my-inherit-input-method)
+; Define the actual input method
+(quail-define-package "math" "UTF-8" "Ω" t)
+(quail-define-rules ; add whatever extra rules you want to define here...
+ ("\\fun"    ?λ)
+ ("\\mult"   ?⋅)
+ ("\\ent"    ?⊢)
+ ("\\valid"  ?✓)
+ ("\\diamond" ?◇)
+ ("\\box"    ?□)
+ ("\\bbox"   ?■)
+ ("\\later"  ?▷)
+ ("\\pred"   ?φ)
+ ("\\and"    ?∧)
+ ("\\or"     ?∨)
+ ("\\comp"   ?∘)
+ ("\\ccomp"  ?◎)
+ ("\\all"    ?∀)
+ ("\\ex"     ?∃)
+ ("\\to"     ?→)
+ ("\\sep"    ?∗)
+ ("\\lc"     ?⌜)
+ ("\\rc"     ?⌝)
+ ("\\Lc"     ?⎡)
+ ("\\Rc"     ?⎤)
+ ("\\lam"    ?λ)
+ ("\\empty"  ?∅)
+ ("\\Lam"    ?Λ)
+ ("\\Sig"    ?Σ)
+ ("\\-"      ?∖)
+ ("\\aa"     ?●)
+ ("\\af"     ?◯)
+ ("\\auth"   ?●)
+ ("\\frag"   ?◯)
+ ("\\iff"    ?↔)
+ ("\\gname"  ?γ)
+ ("\\incl"   ?≼)
+ ("\\latert" ?▶)
+ ("\\update" ?⇝)
+
+ ;; accents (for iLöb)
+ ("\\\"o" ?ö)
+
+ ;; subscripts and superscripts
+ ("^^+" ?⁺) ("__+" ?₊) ("^^-" ?⁻)
+ ("__0" ?₀) ("__1" ?₁) ("__2" ?₂) ("__3" ?₃) ("__4" ?₄)
+ ("__5" ?₅) ("__6" ?₆) ("__7" ?₇) ("__8" ?₈) ("__9" ?₉)
+
+ ("__a" ?ₐ) ("__e" ?ₑ) ("__h" ?ₕ) ("__i" ?ᵢ) ("__k" ?ₖ)
+ ("__l" ?ₗ) ("__m" ?ₘ) ("__n" ?ₙ) ("__o" ?ₒ) ("__p" ?ₚ)
+ ("__r" ?ᵣ) ("__s" ?ₛ) ("__t" ?ₜ) ("__u" ?ᵤ) ("__v" ?ᵥ) ("__x" ?ₓ)
+)
+(mapc (lambda (x)
+        (if (cddr x)
+            (quail-defrule (cadr x) (car (cddr x)))))
+      ; need to reverse since different emacs packages disagree on whether
+      ; the first or last entry should take priority...
+      ; see <https://mattermost.mpi-sws.org/iris/pl/46onxnb3tb8ndg8b6h1z1f7tny> for discussion
+      (reverse (append math-symbol-list-basic math-symbol-list-extended)))
+```
+
+### Font Configuration
+
+Even when usable fonts are installed, Emacs tends to pick bad fonts for some
+symbols like universal and existential quantifiers.  The following configuration
+results in a decent choice for the symbols used in Iris:
+
+```
+;; Fonts
+(set-face-attribute 'default nil :height 110) ; height is in 1/10pt
+(dolist (ft (fontset-list))
+  ; Main font
+  (set-fontset-font ft 'unicode (font-spec :name "Monospace"))
+  ; Fallback font
+  ; Appending to the 'unicode list makes emacs unbearably slow.
+  ;(set-fontset-font ft 'unicode (font-spec :name "DejaVu Sans Mono") nil 'append)
+  (set-fontset-font ft nil (font-spec :name "DejaVu Sans Mono"))
+)
+; Fallback-fallback font
+; If we 'append this to all fontsets, it picks Symbola even for some cases where DejaVu could
+; be used. Adding it only to the "t" table makes it Do The Right Thing (TM).
+(set-fontset-font t nil (font-spec :name "Symbola"))
+```
+
+### Automated Indentation
+
+The default indentation configuration of company-coq is not compatible with the Iris syntax.
+As a result, automatic indentation will indent lines incorrectly.
+
+To solve some of these indentation errors you can add the following line to your Emacs
+initialisation file:
+```
+(setq coq-smie-user-tokens
+   '(("," . ":=")
+	("∗" . "->")
+	("-∗" . "->")
+	("∗-∗" . "->")
+	("==∗" . "->")
+	("=∗" . "->") 			;; Hack to match ={E1,E2}=∗
+	("|==>" . ":=")
+	("⊢" . "->")
+	("⊣⊢" . "->")
+	("↔" . "->")
+	("←" . "<-")
+	("→" . "->")
+	("=" . "->")
+	("==" . "->")
+	("/\\" . "->")
+	("⋅" . "->")
+	(":>" . ":=")
+	("by" . "now")
+	("forall" . "now")              ;; NB: this breaks current ∀ indentation.
+   ))
+```
+This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the
+closely related Coq symbols (e.g. `->`).
+Note that `->` is used in many places, as its indentation behaviour is:
+```
+  P ->
+  Q
+```
+This is the indentation behaviour is what we want, e.g. for `∗`:
+```
+  P ∗
+  Q
+```
+Note that this configuration has some caveats.
+Notably, the change to `forall` (which gives good behavior to e.g.
+`iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation
+behavior to universal quantification:
+```
+  ∀ x,
+  P x
+```
+This is not what we want; the second line should be indented by 2 spaces.
+
+## CoqIDE 8.9 and earlier on Linux (ibus-m17n)
+
+On Linux with old versions of CoqIDE you can use the Intelligent
+Input Bus (IBus) framework to input Unicode symbols. First, install `ibus-m17n`
+via your system's package manager. Next, create a file `~/.m17n.d/coq.mim` to
+configure an input method based on the math symbol list, and with some custom
+aliases for symbols used a lot in Iris as defined [here](ibus).
+
+To use this input method, you should:
+
+1. Enable the "Coq" input using your system settings or using the IBus
+   configuration tool. The Coq input method typically appears in the category
+   "other".
+2. On some systems: In CoqIDE, you have to enable the input method by performing
+   a right click on the text area, and selecting "System (IBus)" under "input
+   method".
+
+## CoqIDE 8.10+ Unicode input
+
+Instead of configuring the input system-wide, you can use CoqIDE's support for
+inputting Unicode symbols (introduced in Coq v8.10). To input a symbol, type a
+LaTeX-like escape sequence, for example `\alpha` and then type
+`<Shift>-<Space>`, which will expand it into `α`. Expansion will work on a
+prefix of the command as well. You can also customize the expansion keyboard
+shortcut, which is under Tools/LaTeX-to-unicode.
+
+This system is configurable by adding a Unicode bindings file with additional
+expansion sequences. On Linux this file should go in
+`~/.config/coq/coqide.bindings` while on macOS it should go in
+`~/Library/Application Support/Coq/coqide.bindings` (or under `$XDG_CONFIG_HOME`
+if you have that set).
+
+Here is a `coqide.bindings` file for a variety of symbols used in Iris:
+
+```
+# LaTeX-like sequences are natively supported (eg, \forall, \mapsto)
+# Iris-specific abbreviations
+\fun            λ
+\mult           ⋅ 1
+\ent            ⊢ 1
+\valid          ✓
+\diamond        ◇
+\box            □ 1
+\bbox           ■
+\later          ▷
+\pred           φ
+\and            ∧
+\or             ∨
+\comp           ∘ 1
+\ccomp          ◎
+\all            ∀
+\ex             ∃
+\to             →
+\sep            ∗
+\lc             ⌜ 1
+\rc             ⌝ 1
+\Lc             ⎡ 1
+\Rc             ⎤ 1
+\lam            λ
+\empty          ∅
+\Lam            Λ
+\Sig            Σ
+\-              ∖ 1
+\aa             ● 1
+\af             ◯ 1
+\auth           ●
+\frag           ◯
+\iff            ↔ 1
+\gname          γ
+\incl           ≼
+\latert         ▶
+\update         ⇝
+# accents
+\"o             ö
+\Lob            Löb
+# subscripts and superscripts
+\^+             ⁺
+\_+             ₊
+\^-             ⁻
+\_0             ₀
+\_1             ₁
+\_2             ₂
+\_3             ₃
+\_4             ₄
+\_5             ₅
+\_6             ₆
+\_7             ₇
+\_8             ₈
+\_9             ₉
+\_a             ₐ
+\_e             ₑ
+\_h             ₕ
+\_i             ᵢ
+\_k             ₖ
+\_l             ₗ
+\_m             ₘ
+\_n             ₙ
+\_o             ₒ
+\_p             ₚ
+\_r             ᵣ
+\_s             ₛ
+\_t             ₜ
+\_u             ᵤ
+\_v             ᵥ
+\_x             ₓ
+```
+
+## Visual Studio Code
+
+### VSCoq setup
+
+The recommended extension as of December 2019 is [Maxime Dénès's
+VSCoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
+Press `Ctrl Shift P` or `Cmd Shift P` and then type "coq" to see the list of Coq
+commands and keyboard shortcuts.
+
+### Font setup
+
+To use unicode you need a font that supports all the symbols, such as [Fira
+Code](https://github.com/tonsky/FiraCode/wiki/Installing). Download and install
+the font, and in VS Code press `Cmd ,` or `Ctrl ,` to go to the settings, search
+for "font", and use "FiraCode-Retina" on macOS or "Fira Code Retina" on Linux as the font-family and optionally enable
+ligatures.
+
+### Unicode input setup
+
+Install the [Generic input method
+extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-input-method).
+To insert a symbol, type the code for a symbol such as `\to` and then press
+`Space` or `Tab`. To enable Iris unicode input support, open your user settings,
+press `Cmd ,` or `Ctrl ,`, type "generic-input-methods.input-methods", and then
+click on "Edit in settings.json" and add the contents of [this file](vscode).
+
+## Vim
+
+The [Coqtail](https://github.com/whonore/coqtail) plugin can be used to develop Coq code in `vim` (install it with your favorite plugin manager).
+Follow the installation instructions in Coqtail's README to setup your keybinds and find out about its usage.
+
+### Unicode support
+For Unicode support, make sure that your terminal emulator supports Unicode and configure it to use a font with Unicode support.
+
+For entering Unicode symbols, one option is the plugin [latex-unicoder](https://github.com/joom/latex-unicoder.vim).
+Install it with your favorite plugin manager.
+To enter a Unicode symbol, hit `C-l` in normal or insert mode. For more details on the usage, see its README.
+
+latex-unicoder comes with a large set of pre-configured symbols known from LaTeX, but you can also add your own by adding (and adapting) the following to your `.vimrc`:
+```
+let g:unicode_map = {
+  \ "\\fun"     :   "λ",
+  \ "\\mult"    :   "⋅",
+  \ "\\ent"     :   "⊢",
+  \ "\\valid"   :   "✓",
+  \ "\\diamond" :   "◇",
+  \ "\\box"     :   "□",
+  \ "\\bbox"   	:   "■",
+  \ "\\later"  	:   "▷",
+  \ "\\pred"   	:   "φ",
+  \ "\\and"    	:   "∧",
+  \ "\\or"     	:   "∨",
+  \ "\\comp"   	:   "∘",
+  \ "\\ccomp"  	:   "◎",
+  \ "\\all"    	:   "∀",
+  \ "\\ex"     	:   "∃",
+  \ "\\to"     	:   "→",
+  \ "\\sep"    	:   "∗",
+  \ "\\lc"     	:   "⌜",
+  \ "\\rc"     	:   "⌝",
+  \ "\\Lc"     	:   "⎡",
+  \ "\\Rc"     	:   "⎤",
+  \ "\\lam"    	:   "λ",
+  \ "\\empty"  	:   "∅",
+  \ "\\Lam"    	:   "Λ",
+  \ "\\Sig"    	:   "Σ",
+  \ "\\-"      	:   "∖",
+  \ "\\aa"     	:   "●",
+  \ "\\af"     	:   "◯",
+  \ "\\auth"   	:   "●",
+  \ "\\frag"   	:   "◯",
+  \ "\\iff"    	:   "↔",
+  \ "\\gname"  	:   "γ",
+  \ "\\incl"   	:   "≼",
+  \ "\\latert" 	:   "▶",
+  \ "\\update" 	:   "⇝",
+  \ "\\\"o"     :   "ö",
+  \ "_a"        :   "ₐ",
+  \ "_e"        :   "ₑ",
+  \ "_h"        :   "ₕ",
+  \ "_i"        :   "ᵢ",
+  \ "_k"        :   "ₖ",
+  \ "_l"        :   "ₗ",
+  \ "_m"        :   "ₘ",
+  \ "_n"        :   "ₙ",
+  \ "_o"        :   "ₒ",
+  \ "_p"        :   "ₚ",
+  \ "_r"        :   "ᵣ",
+  \ "_s"        :   "ₛ",
+  \ "_t"        :   "ₜ",
+  \ "_u"        :   "ᵤ",
+  \ "_v"        :   "ᵥ",
+  \ "_x"        :   "ₓ",
+\ }
+```
+
+
+Alternatively, you can use snippets using [UltiSnips](https://github.com/SirVer/ultisnips).
+
+Install it with your favorite plugin manager, and register a completion key in your configuration:
+```
+let g:UltiSnipsExpandTrigger="<c-l>"
+```
+To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `<c-l>` while still in insert mode.
+
+To register most common unicode characters, put [this file](vim_ultisnips) either at `~/.vim/UltiSnips/coq_unicode.snippets` or `~/.config/nvim/UltiSnips/coq_unicode.snippets`, depending on your preferred variant of Vim.

docs/equalities_and_entailments.md

+# Equalities in Iris
+
+Using std++ and Iris involves dealing with a few subtly different equivalence and equality
+relations, especially among propositions.
+This document summarizes these relations and the subtle distinctions among them.
+This is not a general introduction to Iris: instead, we discuss the different
+Iris equalities and the interface to their Coq implementation. In particular, we
+discuss:
+- Equality ("=") in the *on-paper* Iris metatheory
+- Coq's Leibniz equality (`=`) and std++'s setoid equivalence (`≡`);
+- Iris `n`-equivalence on OFEs (`≡{n}≡`);
+- Iris internal equality (`≡` in `bi_scope`);
+- Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
+
+We use `code font` for Coq notation and "quotes" for paper notation.
+
+## Leibniz equality and setoids
+
+First off, in the metalogic (Coq) we have both the usual propositional (or
+Leibniz) equality `=`, and setoid equality `equiv` / `≡` (defined in `stdpp`).
+Both of these are metalogic connectives from the perspective of Iris, and as
+such are declared in Coq scope `stdpp_scope`.
+
+Setoid equality for a type `A` is defined by the instance of `Equiv A`.  This
+should be accompanied by an `Equivalence` instance which proves that the given
+relation indeed is an equivalence relation.  The handling of setoidsis based on
+Coq's
+[generalized rewriting](https://coq.inria.fr/refman/addendum/generalized-rewriting.html)
+facilities.
+
+Setoid equality can coincide with Leibniz equality, which is reflected by the
+`LeibnizEquiv` typeclass. We say that types with this property are "Leibniz
+types". `equivL` provides a convenient way to define a setoid with Leibniz
+equality. The tactics `fold_leibniz` and `unfold_leibniz` can be used to
+automatically turn all equalities of Leibniz types into `≡` or `=`.
+
+Given setoids `A` and `B` and a function `f : A → B`, an instance `Proper ((≡)
+==> (≡)) f` declares that `f` respects setoid equality, as usual in Coq. Such
+instances enable rewriting with setoid equalities.
+
+Here, stdpp adds the following facilities:
+- `solve_proper` for automating proofs of `Proper` instances.
+- `f_equiv` generalizes `f_equal` to setoids (and indeed arbitrary relations
+  registered with Coq's generalized rewriting). It will for instance turn the
+  goal `f a ≡ f b` into `a ≡ b` given an appropriate `Proper` instance (here,
+  `Proper ((≡) ==> (≡)) f`).
+
+## Defining Proper instances
+
+- For each function `f` that could be used in generalized rewriting (e.g., has
+  setoid, ofe, ordered arguments), there should be a `Params f n` instance. This
+  instance forces Coq's setoid rewriting mechanism not to rewrite in the first
+  `n` arguments of the function `f`. This significantly reduces backtracking
+  during `Proper` search and thus improves performance/avoids failing instance
+  searches that diverge. These first arguments typically include type variables
+  (`A : Type` or `B : A → Type`), type class parameters (`C A`), and Leibniz
+  arguments (`i : nat` or `i : Z`), so they cannot be rewritten or do not need
+  setoid rewriting.
+  Examples:
+  + For `cons : ∀ A, A → list A → list A` we have `Params (@cons) 1`,
+    indicating that the type argument named `A` is not up to rewriting.
+  + For `replicate : ∀ A, nat → A → list A` we have `Params (@replicate) 2`
+    indicating that the type argument `A` is not up to rewriting and that the
+    `nat`-typed argument also does not show up as rewriteable in the `Proper`
+    instance (because rewriting with `=` doesn't need such an instance).
+  + For `lookup : ∀ {Lookup K A M}, K → M → option A` we have
+    `Params (@lookup) 5`: there are 3 Type parameters, 1 type class, and a key
+    (which is Leibniz for all instances).
+- Consequenently, `Proper .. f` instances are always written in such a way
+  that `f` is partially applied with the first `n` arguments from `Params f n`.
+  Note that implicit arguments count here.
+  Further note that `Proper` instances never start with `(=) ==>`.
+  Examples:
+  + `Proper ((≡@{A}) ==> (≡@{list A}) ==> (≡@{list A})) cons`,
+    where `cons` is `@cons A`, matching the 1 in `Params`.
+  + `Proper ((≡@{A}) ==> (≡@{list A})) (replicate n)`,
+    where `replicate n` is `@replicate A n`.
+  + `Proper ((≡@{M}) ==> (≡@{option A})) (lookup k)`,
+    where `lookup k` is `@lookup K A M _ k`, so 5 parameters are fixed, matching
+    the `Params` instance.
+- Lemmas about higher-order functions often need `Params` premises.
+  These are also written using the convention above. Example:
+  ```coq
+  Lemma set_fold_ind `{FinSet A C} {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
+    (∀ x, Proper ((≡) ==> impl) (P x)) → ...
+  ```
+- For premises involving predicates (such as `P` in `set_fold_ind` above), we
+  always write the weakest `Proper`: that is, use `impl` instead of `iff` (and
+  in Iris, write `(⊢)` instead of `(⊣⊢)`). For "simple" `P`s, there should be
+  instances to solve both `impl` and `iff` using `solve_proper`, and for more
+  complicated cases where `solve_proper` fails, an `impl` is much easier to
+  prove by hand than an `iff`.
+
+## Equivalences on OFEs
+
+On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,
+equality "=" is formalized as setoid equality, written `≡` or `equiv`, as before;
+distance "=_n" is formalized as relation `dist n`, also written `≡{n}≡`.
+Tactics `solve_proper` and `f_equiv` also support distance. There is no
+correspondence to Coq's `=` on paper.
+
+Some OFE constructors choose interesting equalities.
+- `discreteO` constructs discrete OFEs (where distance coincides with setoid equality).
+- `leibnizO` constructs discrete OFEs (like `discreteO`) but using `equivL`, so
+  that both distance and setoid equality coincide with Leibniz equality. This
+  should only be used for types that do not have a setoid equality registered.
+
+Given OFEs `A` and `B`, non-expansive functions from `A` to `B` are functions
+`f : A → B` with a proof of `NonExpansive f` (which is notation for `∀ n, Proper
+(dist n ==> dist n) f`).
+
+The type `A -n> B` packages a function with a non-expansiveness proof. This is
+useful because `A -n> B` is itself an OFE, but should be avoided whenever
+possible as it requires the caller to specifically package up function and proof
+(which works particularly badly for lambda expressions).
+
+When an OFE structure on a function type is required but the domain is discrete,
+one can use the type `A -d> B`.  This has the advantage of not bundling any
+proofs, i.e., this is notation for a plain Coq function type. See the
+`discrete_fun` documentation in [`iris.algebra.ofe`](../iris/algebra/ofe.v)
+for further details.
+
+In both OFE function spaces (`A -n> B` and `A -d> B`), setoid equality is
+defined to be pointwise equality, so that functional extensionality holds for `≡`.
+
+## Inside the Iris logic
+
+Next, we introduce notions internal to the Iris logic. Such notions often
+overload symbols used for external notions; however, those overloaded notations
+are declared in scope `bi_scope`. When writing `(P)%I`, notations in `P` are
+resolved in `bi_scope`; this is done implicitly for the arguments of all
+variants of Iris entailments.
+
+The Iris logic has an internal concept of equality: if `a` and `b` are Iris
+terms of type `A`, then their internal equality is written (on paper) "a =_A b";
+in Coq, that's written `(a ≡@{A} b)%I` (notation for `bi_internal_eq` in scope
+`bi_scope`). You can leave away the `@{A}` to let Coq infer the type.
+
+As shown in the Iris appendix, an internal equality `(a ≡ b)%I` is interpreted using
+OFE distance at the current step-index. Many types have `_equivI` lemmas
+characterizing internal equality on them. For instance, if `f, g : A -d> B`,
+lemma `discrete_fun_equivI` shows that `(f ≡ g)%I` is equivalent to
+`(∀ x, f x ≡ g x)%I`.
+
+An alternative to internal equality is to embed Coq equality into the Iris logic
+using `⌜ _ ⌝%I`.  For discrete types, `(a ≡ b)%I` is equivalent to `⌜a ≡ b⌝%I`,
+and the latter can be moved into the Coq context, making proofs more convenient.
+For types with Leibniz equality, we can even equivalently write `⌜a = b⌝%I`, so
+no `Proper` is needed for rewriting.  Note that there is no on-paper equivalent
+to using these embedded Coq equalities for types that are not discrete/Leibniz.
+
+## Relations among Iris propositions
+
+In this section, we discuss relations among internal propositions, and in particular equality/equivalence of propositions themselves.
+Even though some of these notes generalize to all internal logics (other
+`bi`s), we focus on Iris propositions (`iProp`), to discuss both their proof
+theory and their model.
+As Iris propositions form a separation logic, we assume some familiarity with
+separation logics, connectives such as `-∗`, `∗`, `emp` and `→`, and the idea
+that propositions in separation logics are interpreted with predicates over
+resources (see for instance Sec. 2.1 of the MoSEL paper).
+
+In the metalogic, Iris defines the entailment relation between uniform
+predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P`
+implies `Q` on _every_ resource and at all step-indices (for details see Iris appendix [Sec. 6]).
+Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`: the former is
+a Coq-level statement of type `Prop`, the latter an Iris-level statement of type
+`iProp`.  However, the two are closely related: `P ⊢ Q` is equivalent to `emp ⊢
+P -∗ Q` (per Iris lemmas `entails_wand` and `wand_entails`).  Iris also defines
+a "unary" form of entailment, `⊢ P`, which is short for `emp ⊢ P`.
+We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` hold.
+
+On paper, uniform predicates are defined by quotienting by an equivalence
+relation ([Iris appendix, Sec. 3.3]); in Coq, that relation is chosen as the
+setoid equivalent for the type of Iris propositions.
+This equivalence is actually equivalent to bi-entailment, per lemma `equiv_spec`:
+```coq
+Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+```
+Relying on this equivalence, bi-entailment `P ⊣⊢ Q` is defined as notation for `≡`.
+
+## Internal equality of Iris propositions
+
+Inside the logic, we can use internal equality `(≡)%I` on any type, including
+propositions themselves.  However, there is a pitfall here: internal equality
+`≡` is in general strictly stronger than `∗-∗` (the bidirectional version of the
+magic wand), because `Q1 ≡ Q2` means that `Q1` and `Q2` are equivalent
+_independently of the available resources_. This makes `≡` even stronger than `□
+(_ ∗-∗ _)`, because `□` does permit the usage of some resources (namely, the RA
+core of the available resources can still be used).
+
+The two notions of internal equivalence and equality of propositions are related
+by the following law of propositional extensionality:
+```coq
+Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+```
+This uses the plainly modality `■` to reflect that equality corresponds to
+equivalence without any resources available: `■ R` says that `R` holds
+independent of any resources that we might own (but still taking into account
+the current step-index).

docs/ghost-state.tex

-\section{Extensions of the Base Logic}
-
-In this section we discuss some additional constructions that we define within and on top of the base logic.
-These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.
-
-\subsection{Derived rules about base connectives}
-We collect here some important and frequently used derived proof rules.
-\begin{mathparpagebreakable}
-  \infer{}
-  {\prop \Ra \propB \proves \prop \wand \propB}
-
-  \infer{}
-  {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}
-
-  \infer{}
-  {\prop * \All\var.\propB \proves \All\var. \prop * \propB}
-
-  \infer{}
-  {\always(\prop*\propB) \provesIff \always\prop * \always\propB}
-
-  \infer{}
-  {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}
-
-  \infer{}
-  {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}
-
-  \infer{}
-  {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
-
-  \infer{}
-  {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}
-
-  \infer{}
-  {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
-
-  \infer{}
-  {\prop \proves \later\prop}
-\end{mathparpagebreakable}
-
-\subsection{Persistent assertions}
-We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
-These are assertions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic assertions.
-
-Of course, $\always\prop$ is persistent for any $\prop$.
-Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $\TRUE$, $\FALSE$, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$ and $\mval(\melt)$ are persistent.
-Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification and $\later$.
-
-
-
-\subsection{Timeless assertions and except-0}
-
-One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
-It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
-\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
-
-This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
-\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop  \]
-In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless assertions.
-
-The following rules can be derived about except-0:
-\begin{mathpar}
-  \inferH{ex0-mono}
-  {\prop \proves \propB}
-  {\diamond\prop \proves \diamond\propB}
-
-  \axiomH{ex0-intro}
-  {\prop \proves \diamond\prop}
-
-  \axiomH{ex0-idem}
-  {\diamond\diamond\prop \proves \diamond\prop}
-
-\begin{array}[c]{rMcMl}
-  \diamond{(\prop * \propB)} &\provesIff& \diamond\prop * \diamond\propB \\
-  \diamond{(\prop \land \propB)} &\provesIff& \diamond\prop \land \diamond\propB \\
-  \diamond{(\prop \lor \propB)} &\provesIff& \diamond\prop \lor \diamond\propB
-\end{array}
-
-\begin{array}[c]{rMcMl}
-  \diamond{\All x. \prop} &\provesIff& \All x. \diamond{\prop}   \\
-  \diamond{\Exists x. \prop} &\provesIff& \Exists x. \diamond{\prop} \\
-  \diamond\always{\prop} &\provesIff& \always\diamond{\prop} \\
-  \diamond\later\prop &\proves& \later{\prop}
-\end{array}
-\end{mathpar}
-
-The following rules identify the class of timeless assertions:
-\begin{mathparpagebreakable}
-\infer
-{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop \land \propB}}
-
-\infer
-{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop \lor \propB}}
-
-\infer
-{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop * \propB}}
-
-\infer
-{\vctx \proves \timeless{\prop}}
-{\vctx \proves \timeless{\always\prop}}
-
-\infer
-{\vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop \Ra \propB}}
-
-\infer
-{\vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop \wand \propB}}
-
-\infer
-{\vctx,\var:\type \proves \timeless{\prop}}
-{\vctx \proves \timeless{\All\var:\type.\prop}}
-
-\infer
-{\vctx,\var:\type \proves \timeless{\prop}}
-{\vctx \proves \timeless{\Exists\var:\type.\prop}}
-
-\axiom{\timeless{\TRUE}}
-
-\axiom{\timeless{\FALSE}}
-
-\infer
-{\text{$\term$ or $\term'$ is a discrete OFE element}}
-{\timeless{\term =_\type \term'}}
-
-\infer
-{\text{$\melt$ is a discrete OFE element}}
-{\timeless{\ownM\melt}}
-
-\infer
-{\text{$\melt$ is an element of a discrete CMRA}}
-{\timeless{\mval(\melt)}}
-\end{mathparpagebreakable}
-
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "iris"
-%%% End:

docs/heap_lang.md

+# HeapLang overview
+
+HeapLang is the example language that gets shipped with Iris.  It is not the
+only language you can reason about with Iris, but meant as a reasonable demo
+language for simple examples.
+
+## Language
+
+HeapLang is a lambda-calculus with operations to allocate individual locations,
+`load`, `store`, `CmpXchg` (compare-and-exchange) and `FAA` (fetch-and-add). Moreover,
+it has a `fork` construct to spawn new threads.  In terms of values, we have
+integers, booleans, unit, heap locations, as well as (binary) sums and products.
+
+Recursive functions are the only binders, so the sum elimination (`Case`)
+expects both branches to be of function type and passes them the data component
+of the sum.
+
+For technical reasons, the only terms that are considered values are those that
+begin with the `Val` expression former.  This means that, for example, `Pair
+(Val a) (Val b)` is *not* a value -- it reduces to `Val (PairV a b)`, which is.
+This leads to some administrative redexes, and to a distinction between "value
+pairs", "value sums", "value closures" and their "expression" counterparts.
+
+However, this also makes values syntactically uniform, which we exploit in the
+definition of substitution which just skips over `Val` terms, because values
+should be closed and hence not affected by substitution.  As a consequence, we
+can entirely avoid even talking about "closed terms", that notion just does not
+have to come up anywhere.  We also exploit this when writing specifications,
+because we can just write lemmas involving terms of the form `Val ?v` and Coq
+can determine `?v` by unification (because all values start with the `Val`
+constructor).
+
+## Notation
+
+Notation for writing HeapLang terms is defined in
+[`notation.v`](../iris_heap_lang/notation.v).  There are two scopes, `%E` for
+expressions and `%V` for values.  For example, `(a, b)%E` is an expression pair
+and `(a, b)%V` a value pair.  The `e` of a `WP e {{ Q }}` is implicitly in `%E`
+scope.
+
+We define a whole lot of short-hands, such as non-recursive functions (`λ:`),
+let-bindings, sequential composition, and a more conventional `match:` that has
+binders in both branches.
+
+The widely used `#` is a short-hand to turn a basic literal (an integer, a
+location, a boolean literal or a unit value) into a value.  Since values coerce
+to expressions, `#` is widely used whenever a Coq value needs to be placed into
+a HeapLang term.
+
+## Tactics
+
+HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang
+programs as part of proving a weakest precondition.  All of these tactics assume
+that the current goal is of the shape `WP e @ E {{ Q }}`.
+
+Tactics to take one or more pure program steps:
+
+- `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
+  postcondition becomes the new goal.
+- `wp_rec`, `wp_lam`: Perform a beta reduction.  Unlike `wp_pure`, this will
+  also reduce lambdas that are hidden behind a definition.
+- `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition.
+- `wp_proj`: Reduce a projection.
+- `wp_if_true`, `wp_if_false`, `wp_if`: Reduce a conditional expression. The
+  discriminant must already be `true` or `false`.
+- `wp_unop`, `wp_binop`, `wp_op`: Reduce a unary, binary or either kind of
+  arithmetic operator.
+- `wp_case`, `wp_match`: Reduce `Case`/`match:` constructs.
+- `wp_inj`, `wp_pair`, `wp_closure`: Reduce constructors that turn expression
+  sums/pairs/closures into their value counterpart.
+
+Tactics for the heap:
+
+- `wp_alloc l as "H"`: Reduce an allocation instruction and call the new
+  location `l` (in the Coq context) and the points-to assertion `H` (in the
+  spatial context).  You can leave out the `as "H"` to introduce it as an
+  anonymous assertion, which is equivalent to `as "?"`.
+- `wp_load`: Reduce a load operation.  This automatically finds the points-to
+  assertion in the spatial context, and fails if it cannot be found.
+- `wp_store`: Reduce a store operation.  This automatically finds the points-to
+  assertion in the spatial context, and fails if it cannot be found.
+- `wp_cmpxchg_suc`, `wp_cmpxchg_fail`: Reduce a succeeding/failing CmpXchg.  This
+  automatically finds the points-to assertion.  It also automatically tries to
+  solve the (in)equality to show that the CmpXchg succeeds/fails, and opens a new
+  goal if it cannot prove this goal.
+- `wp_cmpxchg as H1 | H2`: Reduce a CmpXchg, performing a case distinction over whether
+  it succeeds or fails.  This automatically finds the points-to assertion.  The
+  proof of equality in the first new subgoal will be called `H1`, and the proof
+  of the inequality in the second new subgoal will be called `H2`.
+- `wp_faa`: Reduce a FAA.  This automatically finds the points-to assertion.
+
+Further tactics:
+
+- `wp_bind pat`: Apply the bind rule to "focus" the term matching `pat`.  For
+  example, `wp_bind (!_)%E` focuses a load operation.  This is useful in
+  particular when accessing invariants, which is only possible when the `WP` in
+  the goal is for a single, atomic operation -- `wp_bind` can be used to bring
+  the goal into the right shape.
+- `wp_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  Apply a lemma whose conclusion is a `WP`, automatically applying `wp_bind` as
+  needed. The `as` clause is optional and can be used to introduce the
+  postcondition; this works particularly well for Texan triples. See the
+  [ProofMode docs](./proof_mode.md) for an explanation of `pm_trm` and `ipat`.
+- `wp_smart_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  like `wp_apply`, but also performs pure reduction steps to reveal a redex that
+  matches `pm_trm`. To be precise, if applying the lemma fails, `wp_smart_apply`
+  will perform a step of pure reduction (via `wp_pure`), and repeat. (This means
+  that `wp_smart_apply` is not the same as `wp_pures; wp_apply`.)
+
+There is no tactic for `Fork`, just do `wp_apply wp_fork`.
+
+To verify a recursive function, use `iLöb`.  Make sure you do `wp_pures` before
+running `iLöb`; otherwise the induction hypothesis will likely not be applicable
+when you need it.  (This makes sure that all administrative redexes are reduced
+in your induction hypothesis, just like we state our `WP` specifications with
+all of the redexes reduced.)
+
+## Notation and lemmas for derived notions involving a thunk
+
+Sometimes, it is useful to define a derived notion in HeapLang that involves
+thunks.  For example, the parallel composition `e1 ||| e2` is definable in
+HeapLang, but that requires thunking `e1` and `e2` before passing them to
+`par`. (This is defined in [`par.v`](../iris_heap_lang/lib/par.v).)  However,
+this is somewhat subtle because of the distinction between expression lambdas
+and value lambdas.
+
+The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want
+`e1` and `e2` to behave normal under substitution (which they would not in a
+value lambda).  However, the *specification* for parallel composition should use
+value lambdas, because prior to applying it the term will be reduced as much as
+possible to achieve a normal form.  To facilitate this, we define a copy of the
+`e1 ||| e2` notation in the value scope that uses value lambdas.
+This is not actually a value, but we still put it in the value scope to
+differentiate from the other notation that uses expression lambdas.  (In the
+future, we might decide to add a separate scope for this.)  Then, we write the
+canonical specification using the notation in the value scope.
+
+This works very well for non-recursive notions.  For `while` loops, the
+situation is unfortunately more complex and proving the desired specification
+will likely be more involved than expected, see this [discussion].
+
+[discussion]: https://gitlab.mpi-sws.org/iris/iris/merge_requests/210#note_32842

docs/ibus

+;; Usage: copy to ~/.m17n.d/coq.mim
+
+(input-method t coq)
+(description "Input method for Coq")
+(title "Coq")
+
+(map (trans
+
+;; Standard LaTeX math notations
+  ("\\forall"         "∀")
+  ("\\exists"         "∃")
+  ("\\lam"            "λ")
+  ("\\not"            "¬")
+  ("\\/"              "∨")
+  ("/\\"              "∧")
+  ("->"               "→")
+  ("<->"              "↔")
+  ("\\<-"             "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
+  ("\\=="             "≡")
+  ("\\/=="            "≢")
+  ("/="               "≠")
+  ("<="               "≤")
+  ("\\in"             "∈")
+  ("\\notin"          "∉")
+  ("\\cup"            "∪")
+  ("\\cap"            "∩")
+  ("\\setminus"       "∖")
+  ("\\subset"         "⊂")
+  ("\\subseteq"       "⊆")
+  ("\\sqsubseteq"     "⊑")
+  ("\\sqsubseteq"     "⊑")
+  ("\\notsubseteq"    "⊈")
+  ("\\meet"           "⊓")
+  ("\\join"           "⊔")
+  ("\\top"            "⊤")
+  ("\\bottom"         "⊥")
+  ("\\vdash"          "⊢")
+  ("\\dashv"          "⊣")
+  ("\\Vdash"          "⊨")
+  ("\\infty"          "∞")
+  ("\\comp"           "∘")
+  ("\\prf"            "↾")
+  ("\\bind"           "≫=")
+  ("\\mapsto"         "↦")
+  ("\\hookrightarrow" "↪")
+  ("\\uparrow"        "↑")
+
+;; Iris specific
+  ("\\fun"            "λ")
+  ("\\mult"           "⋅")
+  ("\\ent"            "⊢")
+  ("\\valid"          "✓")
+  ("\\diamond"        "◇")
+  ("\\box"            "□")
+  ("\\bbox"           "■")
+  ("\\later"          "▷")
+  ("\\pred"           "φ")
+  ("\\and"            "∧")
+  ("\\or"             "∨")
+  ("\\comp"           "∘")
+  ("\\ccomp"          "◎")
+  ("\\all"            "∀")
+  ("\\ex"             "∃")
+  ("\\to"             "→")
+  ("\\sep"            "∗")
+  ("\\lc"             "⌜")
+  ("\\rc"             "⌝")
+  ("\\Lc"             "⎡")
+  ("\\Rc"             "⎤")
+  ("\\empty"          "∅")
+  ("\\Lam"            "Λ")
+  ("\\Sig"            "Σ")
+  ("\\-"              "∖")
+  ("\\aa"             "●")
+  ("\\af"             "◯")
+  ("\\auth"           "●")
+  ("\\frag"           "◯")
+  ("\\iff"            "↔")
+  ("\\gname"          "γ")
+  ("\\incl"           "≼")
+  ("\\latert"         "▶")
+  ("\\update"         "⇝")
+  ("\\bind"           "≫=")
+
+;; accents (for iLöb)
+  ("\\\"o" "ö")
+
+;; subscripts and superscripts
+  ("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
+  ("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
+  ("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
+
+  ("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
+  ("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
+  ("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
+
+;; Greek alphabet
+  ("\\Alpha"  "Α")   ("\\alpha"  "α")
+  ("\\Beta"   "Β")   ("\\beta"   "β")
+  ("\\Gamma"  "Γ")   ("\\gamma"  "γ")
+  ("\\Delta"  "Δ")   ("\\delta"  "δ")
+  ("\\Epsilon"  "Ε") ("\\epsilon"  "ε")
+  ("\\Zeta"   "Ζ")   ("\\zeta"   "ζ")
+  ("\\Eta"  "Η")     ("\\eta"  "η")
+  ("\\Theta"  "Θ")   ("\\theta"  "θ")
+  ("\\Iota"   "Ι")   ("\\iota"   "ι")
+  ("\\Kappa"  "Κ")   ("\\kappa"  "κ")
+  ("\\Lamda"  "Λ")   ("\\lamda"  "λ")
+  ("\\Lambda"   "Λ") ("\\lambda"   "λ")
+  ("\\Mu"   "Μ")     ("\\mu"   "μ")
+  ("\\Nu"   "Ν")     ("\\nu"   "ν")
+  ("\\Xi"   "Ξ")     ("\\xi"   "ξ")
+  ("\\Omicron"  "Ο") ("\\omicron"  "ο")
+  ("\\Pi"   "Π")     ("\\pi"   "π")
+  ("\\Rho"  "Ρ")     ("\\rho"  "ρ")
+  ("\\Sigma"  "Σ")   ("\\sigma"  "σ")
+  ("\\Tau"  "Τ")     ("\\tau"  "τ")
+  ("\\Upsilon"  "Υ") ("\\upsilon"  "υ")
+  ("\\Phi"  "Φ")     ("\\phi"  "φ")
+  ("\\Chi"  "Χ")     ("\\chi"  "χ")
+  ("\\Psi"  "Ψ")     ("\\psi"  "ψ")
+  ("\\Omega"  "Ω")   ("\\omega"  "ω")
+))
+(state (init (trans)))

docs/proof_guide.md

+# Iris Proof Guide
+
+This work-in-progress document serves to explain how Iris proofs are typically
+carried out in Coq: what are the common patterns and conventions, what are the
+common pitfalls.  This complements the tactic documentation for the
+[proof mode](./proof_mode.md) and [HeapLang](./heap_lang.md).
+
+## Order of `Requires`
+
+In Coq, declarations in modules imported later may override the
+previous definition. Therefore, in order to make sure the most
+relevant declarations and notations always take priority, we recommend
+importing dependencies from the furthest to the closest.
+
+In particular, when importing Iris, Stdpp and Coq stdlib modules, we
+recommend importing in the following order:
+- Coq
+- stdpp
+- iris.algebra
+- iris.bi
+- iris.proofmode
+- iris.base_logic
+- iris.program_logic
+- iris.heap_lang
+
+## Resolving mask mismatches
+
+Sometimes, `fupd` masks are not exactly what they need to be to make progress.
+There are two situations to distinguish here.
+
+#### Eliminating a [fupd] with a mask smaller than the current one
+
+When your goal is `|={E,_}=> _` and you want to do `iMod` on an `|={E',_}=> _`, Coq will complain even if `E' ⊆ E`.
+To resolve this, you first need to explicitly weaken your mask from `E` to `E'` by doing:
+```coq
+iMod (fupd_mask_subseteq E') as "Hclose".
+{ (* Resolve subset sidecondition. *) }
+```
+Later, you can `iMod "Hclose" as "_"` to restore the mask back from `E'` to `E`.
+
+Notice that this will make the invariants in `E' ∖ E` unavailable until you use `Hclose`.
+Usually this is not a problem, but there are theoretical situations where using `fupd_mask_subseteq` like this can prevent you from proving a goal.
+In that case, you will have to experiment with rules like `fupd_mask_frame`, but those are not very convenient to use.
+
+#### Introducing a [fupd] when the masks are not yet the same
+
+When your goal is `|={E,E'}=> _` and you want to do `iModIntro`, Coq will complain even if `E' ⊆ E`.
+This arises, for example, in clients of TaDA-style logically atomic specifications.
+To resolve this, do:
+```coq
+iApply fupd_mask_intro.
+{ (* Resolve subset sidecondition. *) }
+iIntros "Hclose".
+```
+Later, you can `iMod "Hclose" as "_"` to restore the mask back from `E'` to `E`.
+
+## Canonical structures and type classes
+
+In Iris, we use both canonical structures and type classes, and some careful
+tweaking is necessary to make the two work together properly.  The details of
+this still need to be written up properly, but here is some background material:
+
+* [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/math-classes/mscs.pdf)
+* [Canonical Structures for the working Coq user](https://hal.inria.fr/hal-00816703v1/document)
+
+## Implicit generalization
+
+We often use the implicit generalization feature of Coq, triggered by a backtick:
+`` `{!term A B}`` means that an implicit argument of type `term A B` is added,
+and if any of the identifiers that are used here is not yet bound, it gets added
+as well.  Usually, `term` will be some existing type class or similar, and we
+use this syntax to also generalize over `A` and `B`; then the above is
+equivalent to `{A B} {Hterm: term A B}`.  The `!` in front of the term disables
+an even stronger form of generalization, where if `term` is a type class then
+all missing arguments get implicitly generalized as well.  This is sometimes
+useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C,
+!Countable C}``.  However, generally it is more important to be aware of the
+assumptions you are making, so implicit generalization without `!` should be
+avoided.
+
+## Type class resolution control
+
+When you are writing a module that exports some Iris term for others to use
+(e.g., `join_handle` in the [spawn module](../iris_heap_lang/lib/spawn.v)), be
+sure to mark these terms as opaque for type class search at the *end* of your
+module (and outside any section):
+```coq
+Typeclasses Opaque join_handle.
+```
+This makes sure that the proof mode does not "look into" your definition when it
+is used by clients.
+
+## Library type class assumptions
+
+When a parameterized library needs to make some type class assumptions about its
+parameters, it is convenient to add those to the `libG` class that the library
+will likely need anyway (see the [resource algebra docs](resource_algebras.md)
+for further details on `libG` classes).  For example, the STS library is
+parameterized by an STS and assumes that the STS state space is inhabited:
+```coq
+Class stsG Σ (sts : stsT) := {
+  #[local] sts_inG :: inG Σ (stsR sts);
+  sts_inhabited :> Inhabited (sts.state sts);
+}.
+```
+In this case, the `Instance` for this `libG` class has more than just a `subG`
+assumption:
+```coq
+Instance subG_stsΣ Σ sts :
+  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
+Proof. solve_inG. Qed.
+```
+
+One subtle detail here is that the `subG` assumption comes first in
+`subG_stsΣ`, i.e., it appears before the `Inhabited`.  This is important because
+otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
+type class search diverge.
+
+## Notations
+
+Notations starting with `(` or `{` should be left at their default level (`0`),
+and inner subexpressions that are bracketed by delimiters should be left at
+their default level (`200`).
+
+Moreover, correct parsing of notations sometimes relies on Coq's automatic
+left-factoring, which can require coordinating levels of certain "conflicting"
+notations and their subexpressions.  For instance, to disambiguate `(⊢@{ PROP
+})` and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`,
+but it can only do so if all occurrences of `⊢@{ PROP }` agree on the
+precedences for all subexpressions. This also requires using the same
+tokenization in all cases, i.e., the notation has to consistently be declared as
+`(⊢@{` or `('⊢@{'`, but not a mixture of the two. The latter form of using
+explicit tokenization with `'` is preferred to avoid relying on Coq's default.
+
+For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules).
+
+## Naming conventions for variables/arguments/hypotheses
+
+### small letters
+
+* a : A = cmra or ofe
+* b : B = cmra or ofe
+* c
+* d
+* e : expr = expressions
+* f = some generic function
+* g = some generic function
+* h : heap
+* i
+* j
+* k
+* l
+* m* = prefix for option ("maybe")
+* n
+* o
+* p
+* q
+* r : iRes = (global) resources inside the Iris model
+* s = state (STSs)
+* s = stuckness bits
+* t
+* u
+* v : val = values of language
+* w
+* x
+* y
+* z 
+
+### capital letters
+
+* A : Type, cmra or ofe
+* B : Type, cmra or ofe
+* C
+* D
+* E : coPset = mask of fancy update or WP
+* F = a functor
+* G
+* H = hypotheses
+* I = indexing sets
+* J
+* K : ectx = evaluation contexts
+* K = keys of a map
+* L
+* M = maps / global CMRA
+* N : namespace
+* O 
+* P : uPred, iProp or Prop
+* Q : uPred, iProp or Prop
+* R : uPred, iProp or Prop
+* S : set state = state sets in STSs
+* T : set token = token sets in STSs
+* U
+* V
+* W
+* X : sets
+* Y : sets
+* Z : sets
+
+### small greek letters
+
+* γ : gname = name of ghost state instance
+* σ : state = state of language
+* φ : Prop = pure proposition embedded into uPred or iProp
+
+### capital greek letters
+
+* Φ : general predicate (in uPred, iProp or Prop)
+* Ψ : general predicate (in uPred, iProp or Prop)
+
+## Naming conventions for algebraic classes
+
+### Suffixes
+
+* O: OFEs
+* R: cameras
+* UR: unital cameras or resources algebras
+* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
+* G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
+* GS: global singleton (a `*G` type class with extra data that needs to be unique in a proof)
+* GpreS: collecting preconditions to instantiate the corresponding `*GS`
+* I: bunched implication logic (of type `bi`)
+* SI: step-indexed bunched implication logic (of type `sbi`)
+* T: canonical structures for algebraic classes (for example ofe for OFEs, cmra for cameras)
+* Σ: global camera functor management (`gFunctors`; see the [resource algebra docs](resource_algebras.md))

docs/proof_mode.md

+Tactic overview
+===============
+
+This reference manual defines a few different syntaxes that are used
+pervasively. These are defined in dedicated sections in this manual.
+
+- An "[introduction pattern][ipat]" `ipat` like `"H"` or `"[H1 H2]"` is used to
+  _destruct_ a hypothesis (sometimes called _eliminating_ a hypothesis). This is
+  directly used by `iDestruct` and `iIntros`, but many tactics also integrate
+  support for `ipat`s to combine some other work with destructing, such as
+  `iMod`. The name "introduction pattern" comes from a similar term in Coq which
+  is used in tactics like `destruct` and `intros`.
+- A "[selection pattern][selpat]" `selpat` like `"H1 H2"` or `"#"` names a collection of
+  hypotheses. Most commonly used in `iFrame`.
+- A "[specialization pattern][spat]" `spat` like `H` or `[$H1 H2]` is used to specialize
+  a wand to some hypotheses along with specifying framing. Commonly used as part
+  of proof mode terms (described just below).
+- A "[proof mode term][pm-trm]" `pm_trm` like `lemma with spat` or `"H" $! x with spat`
+  allows to specialize a wand (which can be either a Gallina lemma or a
+  hypothesis) on the fly, as an argument to `iDestruct` for example.
+
+Many of the tactics below apply to more goals than described in this document
+since the behavior of these tactics can be tuned via instances of the type
+classes in the file [proofmode/classes](../iris/proofmode/classes.v). Most notably, many
+of the tactics can be applied when the connective to be introduced or to be eliminated
+appears under a later, an update modality, or in the conclusion of a
+weakest precondition.
+
+[ipat]: #introduction-patterns-ipat
+[selpat]: #selection-patterns-selpat
+[spat]: #specialization-patterns-spat
+[pm-trm]: #proof-mode-terms-pm_trm
+
+Starting and stopping the proof mode
+------------------------------------
+
+- `iStartProof` : start the proof mode by turning a Coq goal into a proof
+  mode entailment. This tactic is performed implicitly by all proof mode tactics
+  described in this file, and thus should generally not be used by hand.
+  + `iStartProof PROP` : explicitly specify which BI logic `PROP : bi` should be
+    used. This is useful to drop down in a layered logic, e.g. to drop down from
+    `monPred PROP` to `PROP`.
+- `iStopProof` : turn the proof-mode entailment into an ordinary Coq goal
+  `big star of context ⊢ proof mode goal`.
+
+Applying hypotheses and lemmas
+------------------------------
+
+- `iExact "H"`  : finish the goal if the conclusion matches the hypothesis `H`
+- `iAssumption` : finish the goal if the conclusion matches any hypothesis in
+  either the proofmode or the Coq context. Only hypotheses in the Coq context
+  that are _syntactically_ of the shape `⊢ P` are recognized by this tactic
+  (this means that assumptions of the shape `P ⊢ Q` are not recognized).
+- `iApply pm_trm` : match the conclusion of the current goal against the
+  conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
+  [proof mode terms][pm-trm] below.
+  If the applied term has more premises than given specialization patterns, the
+  pattern is extended with `[] ... []`. As a consequence, all unused spatial
+  hypotheses move to the last premise.
+
+Context management
+------------------
+
+- `iIntros (x1 ... xn) "ipat1 ... ipatn"` : introduce universal quantifiers
+  using Coq introduction patterns `x1 ... xn` and implications/wands using proof
+  mode [introduction patterns][ipat] `ipat1 ... ipatn`.
+- `iClear (x1 ... xn) "selpat"` : clear the hypotheses given by the [selection
+  pattern][selpat] `selpat` and the Coq level hypotheses/variables `x1 ... xn`.
+- `iClear select (pat)%I` : clear the last hypothesis of the intuitionistic
+  or spatial context that matches pattern `pat`.
+- `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the [selection
+  pattern][selpat] `selpat` into wands, and the Coq level hypotheses/variables
+  `x1 ... xn` into universal quantifiers. Intuitionistic hypotheses are wrapped
+  into the intuitionistic modality.
+- `iRevert select (pat)%I` : revert the last hypothesis of the intuitionistic
+  or spatial context that matches pattern `pat`.
+- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
+- `iRename select (pat)%I into "H"` : rename the last hypothesis of the
+  intuitionistic or spatial context that matches pattern `pat` into `H`. This
+  is particularly useful to give a name to an anonymous hypothesis.
+- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
+  implications/wands of a hypothesis `pm_trm`. See [proof mode terms][pm-trm] below.
+- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
+  implications/wands of a hypothesis `pm_trm` whose conclusion is persistent.
+  All hypotheses can be used for proving the premises of `pm_trm`, as well as
+  for the resulting main goal.
+- `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
+  destruct it using the [introduction pattern][ipat] `ipat`. This tactic is
+  essentially the same as `iDestruct` with the difference that `pm_trm` is not
+  thrown away if possible.
+- `iAssert (P)%I with "spat" as "H"` : generate a new subgoal `P` and add the
+  hypothesis `P` to the current goal as `H`. The [specialization pattern][spat] `spat`
+  specifies which hypotheses will be consumed by proving `P`.
+  + `iAssert (P)%I with "spat" as "ipat"` : like the above, but immediately destruct
+    the generated hypothesis using the [introduction pattern][ipat] `ipat`. If `ipat`
+    is "intuitionistic" (most commonly, it starts with `#` or `%`), then all spatial
+    hypotheses are available in both the subgoal for `P` as well as the current
+    goal. An `ipat` is considered intuitionistic if all branches start with a
+    `#` (which causes `P` to be moved to the intuitionistic context) or with a
+    `%` (which causes `P` to be moved to the pure Coq context).
+  + `iAssert (P)%I as %cpat` : assert `P` and destruct it using the Coq introduction
+    pattern `cpat`. All hypotheses can be used for proving `P` as well as for
+    proving the current goal.
+- `iSelect (pat)%I tac` : run the tactic `tac H`, where `H` is the name of the
+  last hypothesis in the intuitionistic or spatial hypothesis context that
+  matches pattern `pat`. There is no backtracking to select the next hypothesis
+  in case `tac H` fails.
+
+Introduction of logical connectives
+-----------------------------------
+
+- `iPureIntro` : turn a pure goal, typically of the form `⌜φ⌝`, into a Coq
+  goal. This tactic also works for goals of the shape `a ≡ b` on discrete
+  OFEs, and `✓ a` on discrete cameras.
+- `iLeft` : prove a disjunction `P ∨ Q` by proving the left side `P`.
+- `iRight` : prove a disjunction `P ∨ Q` by proving the right side `Q`.
+- `iSplitL "H1 ... Hn"` : split a conjunction `P ∗ Q` into two proofs. The
+  hypotheses `H1 ... Hn` are used for the left conjunct, and the remaining ones
+  for the right conjunct. Intuitionistic hypotheses are always available in both
+  proofs. Also works on `P ∧ Q`, although in that case you can use `iSplit` and
+  retain all the hypotheses in both goals.
+- `iSplitR "H0 ... Hn"` : symmetric version of the above, using the hypotheses
+  `H1 ... Hn` for the right conjunct. Note that the goals are still ordered
+  left-to-right; you can use `iSplitR "..."; last
+  first` to reverse the generated goals.
+- `iSplit` : split a conjunction `P ∧ Q` into two goals. Also works for
+  separating conjunction `P ∗ Q` provided one of the operands is persistent (and both
+  proofs may use the entire spatial context).
+- `iExists t1, .., tn` : provide a witness for an existential quantifier `∃ x, ...`. `t1
+  ... tn` can also be underscores, which are turned into evars. (In fact they
+  can be arbitrary terms with holes, or `open_constr`s, and all of the
+  holes will be turned into evars.)
+
+Elimination of logical connectives
+----------------------------------
+
+- `iExFalso` : change the goal to proving `False`.
+- `iDestruct` is an important enough tactic to describe several special cases:
+  + `iDestruct "H1" as (x1 ... xn) "H2"` : eliminate a series of existential
+    quantifiers in hypothesis `H1` using Coq introduction patterns `x1 ... xn`
+    and name the resulting hypothesis `H2`. The Coq introduction patterns can
+    also be used for pure conjunctions; for example we can destruct
+    `∃ x, ⌜v = x⌝ ∗ l ↦ x` using `iDestruct "H" as (x Heq) "H"` to immediately
+    put `Heq: v = x` in the Coq context. This variant of the tactic will always
+    throw away the original hypothesis `H1`.
+  + `iDestruct pm_trm as "ipat"` : specialize the [proof-mode term][pm-trm] (see
+    below) and destruct it using the [introduction pattern][ipat] `ipat`. If
+    `pm_trm` starts with a hypothesis, and that hypothesis resides in the
+    intuitionistic context, it will not be thrown away.
+  + `iDestruct pm_trm as (x1 ... xn) "ipat"` : combine the above, first
+    specializing `pm_trm`, then eliminating existential quantifiers (and pure
+    conjuncts) with `x1 ... xn`, and finally destructing the resulting term
+    using the [introduction pattern][ipat] `ipat`.
+  + `iDestruct pm_trm as %cpat` : destruct the pure conclusion of a term
+    `pr_trm` using the Coq introduction pattern `cpat`. When using this tactic,
+    all hypotheses can be used for proving the premises of `pm_trm`, as well as
+    for proving the resulting goal.
+  + `iDestruct num as (x1 ... xn) "ipat"` / `iDestruct num as %cpat` :
+    introduce `num : nat` hypotheses and destruct the last introduced hypothesis.
+  + `iDestruct select (pat)%I as ...` is the same as `iDestruct "H" as ...`,
+    where `H` is the name of the last hypothesis of the intuitionistic or
+    spatial context matching pattern `pat`.
+
+  In case all branches of `ipat` start with a `#` (which causes the hypothesis
+  to be moved to the intuitionistic context), with an `%` (which causes the
+  hypothesis to be moved to the pure Coq context), or with an `->`/`<-` (which
+  performs a rewrite), then one can use all hypotheses for proving the premises
+  of `pm_trm`, as well as for proving the resulting goal. Note that in this case
+  the hypotheses still need to be subdivided among the spatial premises.
+
+Separation logic-specific tactics
+---------------------------------
+
+- `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
+  `t1 ... tn` and Iris hypotheses given by [`selpat`][selpat] in the goal. The constructs
+  of the selection pattern have the following meaning:
+  + `%` : repeatedly frame hypotheses from the Coq context.
+  + `#` : repeatedly frame hypotheses from the intuitionistic context.
+  + `∗` : frame as much of the spatial context as possible. (N.B: this
+          is the unicode symbol `∗`, not the regular asterisk `*`.)
+  Notice that framing spatial hypotheses makes them disappear, but framing Coq
+  or intuitionistic hypotheses does not make them disappear.
+  This tactic solves the goal if everything in the conclusion has been framed.
+- `iFrame select (pat)%I` : cancel the last hypothesis of the intuitionistic
+  of spatial context that matches pattern `pat`.
+- `iCombine "H1 H2" as "ipat"` : combine `H1 : P1` and `H2 : P2` into `H: P1 ∗
+  P2` or something simplified but equivalent, then `destruct` the combined
+  hypothesis using `ipat`. Some examples of simplifications `iCombine` knows
+  about are to combine `own γ x` and `own γ y` into `own γ (x ⋅ y)`, and to
+  combine `l ↦{1/2} v` and `l ↦{1/2} v` into `l ↦ v`.
+- `iCombine "H1 H2" gives "ipat"` : from `H1 : P1` and `H2 : P2`, find
+  persistent consequences of `P1 ∗ P2`, then `destruct` this consequence with
+  `ipat`. Some examples of persistent consequences `iCombine` knows about are
+  that `own γ x` and `own γ y` gives `✓ (x ⋅ y)`, and that
+  `l ↦{#q1} v1` and `l ↦{#q2} v2` gives `⌜(q1 + q2 ≤ 1) ∧ v1 = v2⌝`.
+- `iCombine "H1 H2" as "ipat1" gives "ipat2"` combines the two functionalities
+  of `iCombine` described above.
+- `iAccu` : solve a goal that is an evar by instantiating it with all
+  hypotheses from the spatial context joined together with a separating
+  conjunction (or `emp` in case the spatial context is empty). Not commonly
+  used, but can be extremely useful when combined with automation.
+
+Modalities
+----------
+
+- `iModIntro` : introduce a modality in the goal. The type class `FromModal` is
+  used to specify which modalities this tactic should introduce, and how
+  introducing that modality affects the hypotheses. Instances of
+  that type class include: later, except 0, basic update and fancy update,
+  intuitionistically, persistently, affinely, plainly, absorbingly, objectively,
+  and subjectively.
+  + `iModIntro mod` (rarely used): introduce a specific modality named by
+  `mod`,  which is a term pattern (i.e., a term with holes as underscores).
+  `iModIntro mod` will find a subterm matching `mod`, and try introducing its
+  topmost modality. For instance, if the goal is `⎡|==> P⎤`, using `iModIntro
+  ⎡|==> P⎤%I` or `iModIntro ⎡_⎤%I` would introduce `⎡_⎤` and produce goal `|==>
+  P`, while `iModIntro (|==> _)%I` would introduce `|==>` and produce goal
+  `⎡P⎤`.
+  + `iNext` : an alias of `iModIntro (▷^_ _)` (that is, introduce the later
+    modality). This eliminates a later in the goal, and in exchange also strips
+    one later from all the hypotheses.
+  + `iNext n` : an alias of `iModIntro (▷^n _)` (that is, introduce the `▷^n`
+    modality).
+  + `iAlways` : a deprecated alias of `iModIntro` (intended to introduce the `□`
+    modality).
+- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
+  an instance of the `ElimModal` type class, and destruct the resulting
+  hypothesis using `ipat`. Instances include: later, except 0,
+  basic update `|==>` and fancy update `|={E}=>`.
+  + `iMod "H"` : equivalent to `iMod "H" as "H"` (eliminates the modality and
+    keeps the name of the hypothesis).
+  + `iMod pm_trm` : equivalent to `iMod pm_term as "?"` (the resulting
+    hypothesis will be introduced anonymously).
+
+Induction
+---------
+
+- `iLöb as "IH"` : perform Löb induction by
+  generating a hypothesis `IH : ▷ goal`.
+  + `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction,
+  generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
+  the selection pattern `selpat`, and the spatial context as usual.
+- `iInduction x as cpat` : perform induction on the Coq term `x`. The
+  Coq introduction pattern `cpat` is used to name the introduced variables,
+  including the induction hypotheses which are introduced into the proof mode
+  context. Note that induction hypotheses should not be put into string
+  quotation marks `".."`, e.g., use `iInduction n as [|n IH]` to perform
+  induction on a natural number `n`. An implementation caveat is that the names
+  of the induction hypotheses should be fresh in both the Coq context and the
+  proof mode context.
+  + `iInduction x as cpat forall (x1 ... xn) "selpat"` : perform induction,
+    generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
+    the selection pattern `selpat`, and the spatial context.
+  + `iInduction x as cpat using t` : perform induction using the induction
+    scheme `t`. Common examples of induction schemes are `map_ind`, `set_ind_L`,
+    and `gmultiset_ind` for `gmap`, `gset`, and `gmultiset`.
+  + `iInduction x as cpat using t forall (x1 ... xn) "selpat"` : the above
+    variants combined.
+  + `iInduction x as cpat "IH" "selpat"` : ignore the names of the induction
+    hypotheses from `cpat` and call them `IH`, `IH1`, `IH2`, etc. Here "IH" is
+    a string (in string quotation marks). This is *legacy* syntax that might be
+    deprecated in the future. Similar legacy syntax exists for all variants above.
+
+Rewriting / simplification
+--------------------------
+
+- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
+  equality in the proof mode goal / hypothesis `H`.
+- `iRewrite -pm_trm` / `iRewrite -pm_trm in "H"` : rewrite in reverse direction
+  using an internal equality in the proof mode goal / hypothesis `H`.
+- `iEval (tac)` / `iEval (tac) in "selpat"` : perform a tactic `tac`
+  on the proof mode goal / hypotheses given by the selection pattern
+  `selpat`. Using `%` as part of the selection pattern is unsupported.
+  The tactic `tac` should be a reduction or rewriting tactic like
+  `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar`
+  where `P` is the proof goal / a hypothesis given by `selpat`. After
+  running `tac`, `?evar` is unified with the resulting `P`, which in
+  turn becomes the new proof mode goal / a hypothesis given by
+  `selpat`. Note that parentheses around `tac` are needed.
+- `iSimpl` / `iSimpl in "selpat"` : perform `simpl` on the proof mode
+  goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (simpl)`.
+- `iUnfold xs` / `iUnfold xs in "selpat"` : perform `unfold xs` on the proof
+  mode goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (unfold xs)`. Similar to Coq's `unfold`, the argument
+  `xs` should be a comma-separated non-empty list.
+
+Iris
+----
+
+- `iInv H as (x1 ... xn) "ipat"` : open an invariant in hypothesis H. The result
+  is destructed using the Coq intro patterns `x1 ... xn` (for existential
+  quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
+  + `iInv H with "selpat" as (x1 ... xn) "ipat" "Hclose"` : generate an update
+  for closing the invariant and put it in a hypothesis named `Hclose`.
+  + `iInv H with "selpat" as (x1 ... xn) "ipat"` : supply a selection pattern
+  `selpat`, which is used for any auxiliary assertions needed to open the
+  invariant (e.g. for cancelable or non-atomic invariants).
+  + `iInv N as (x1 ... xn) "ipat"` : identify the invariant to be opened with a
+    namespace `N` rather than giving a specific hypothesis.
+  + `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : combine all the
+    above, where `S` is either a proof-mode identifier or a namespace.
+
+Miscellaneous
+-------------
+
+- The tactic `done` of [std++](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v)
+  (which solves "trivial" goals using `intros`, `reflexivity`, `symmetry`,
+  `eassumption`, `trivial`, `split`, `discriminate`, `contradiction`, etc.) is
+  extended so that it also, among other things:
+  + performs `iAssumption`,
+  + introduces `∀`, `→`, and `-∗` in the proof mode,
+  + introduces pure goals `⌜ φ ⌝` using `iPureIntro` and calls `done` on `φ`, and,
+  + solves other trivial proof mode goals, such as `emp`, `x ≡ x`, big operators
+    over the empty list/map/set/multiset.
+
+  (Note that ssreflect also has a `done` tactic. Although Iris uses ssreflect,
+  it overrides ssreflect's `done` tactic with std++'s.)
+- The proof mode adds hints to the core `eauto` database so that `eauto`
+  automatically introduces: conjunctions and disjunctions, universal and
+  existential quantifiers, implications and wand, plainness, persistence, later
+  and update modalities, and pure connectives.
+
+Selection patterns (`selpat`)
+=============================
+
+Selection patterns are used to select hypotheses in the tactics `iRevert`,
+`iClear`, `iFrame`, `iLöb` and `iInduction`. The proof mode supports the
+following _selection patterns_:
+
+- `H` : select the hypothesis named `H`.
+- `%` : select the entire pure/Coq context.
+- `#` : select the entire intuitionistic context.
+- `∗` : select the entire spatial context. (N.B: this
+        is the unicode symbol `∗`, not the regular asterisk `*`.)
+
+Introduction patterns (`ipat`)
+==============================
+
+Introduction patterns are used to perform introductions and eliminations of
+multiple connectives on the fly. The proof mode supports the following
+_introduction patterns_:
+
+- `H` : create a hypothesis named `H`.
+- `?` : create an anonymous hypothesis.
+- `_` : clear the hypothesis.
+- `$` : frame the hypothesis in the goal.
+- `[ipat1 ipat2]` : (separating) conjunction elimination. In order to destruct
+  conjunctions `P ∧ Q` in the spatial context, one of the following conditions
+  should hold:
+  + Either the proposition `P` or `Q` should be persistent.
+  + Either `ipat1` or `ipat2` should be `_`, which results in one of the
+    conjuncts to be thrown away.
+- `[%x ipat]`/`[% ipat]` : existential elimination, naming the witness `x` or
+  keeping it anonymous. Falls back to (separating) conjunction elimination in
+  case the hypothesis is not an existential, so this pattern also works for
+  (separating) conjunctions with a pure left-hand side.
+- `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
+  to destruct nested (separating) conjunctions.
+- `[ipat1|ipat2]` : disjunction elimination.
+- `[]` : false elimination.
+- `%H` : move the hypothesis to the pure Coq context, and name it `H`.
+- `%` : move the hypothesis to the pure Coq context (anonymously). Note that if
+  `%` is followed by an identifier, and not another token, a space is needed
+  to disambiguate from `%H` above.
+- `->` and `<-` : rewrite using a pure Coq equality
+- `# ipat` : move the hypothesis into the intuitionistic context. The tactic
+  will fail if the hypothesis is not intuitionistic. On success, the tactic will
+  strip any number of intuitionistic and persistence modalities. If the
+  hypothesis is already in the intuitionistic context, the tactic will still
+  strip intuitionistic and persistence modalities (it is a no-op if the
+  hypothesis does not contain such modalities).
+- `-# ipat` (uncommon) : move the hypothesis into the spatial context. This can
+  move a hypothesis from the intuitionistic context to the spatial context, or
+  can explicitly specify the spatial context when the intuitionistic context
+  could be used (e.g., because a hypothesis was proven without using spatial
+  hypotheses). If the hypothesis is already in the spatial context, the tactic
+  is a no-op. If the hypothesis is not affine, an `<affine>` modality is added
+  to the hypothesis.
+- `> ipat` : eliminate a modality (if the goal permits); commonly used to strip
+  a later from the hypothesis when it is timeless and the goal is either a `WP`
+  or an update modality `|={E}=>`.
+
+Apart from this, there are the following introduction patterns that can only
+appear at the top level:
+
+- `{selpat}` : clear the hypotheses given by the selection pattern `selpat`.
+  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 a modality by calling `iModIntro`.
+- `!#` : introduce a modality by calling `iModIntro` (deprecated).
+- `/=` : perform `simpl`.
+- `//` : perform `try done` on all goals.
+- `//=` : syntactic sugar for `/= //`
+- `*` : introduce all universal quantifiers. (N.B.: this is the asterisk `*` and
+  not the separating conjunction `∗`)
+- `**` : introduce all universal quantifiers, as well as all arrows and wands.
+
+For example, given:
+
+        ∀ x, <affine> ⌜ x = 0 ⌝ ⊢
+          □ (P → False ∨ □ (Q ∧ ▷ R) -∗
+          P ∗ ▷ (R ∗ Q ∧ ⌜ x = pred 2 ⌝)).
+
+You can write
+
+        iIntros (x Hx) "!> $ [[] | #[HQ HR]] /= !>".
+
+which results in:
+
+        x : nat
+        Hx : x = 0
+        ______________________________________(1/1)
+        "HQ" : Q
+        "HR" : R
+        --------------------------------------□
+        R ∗ Q ∧ x = 1
+
+
+Specialization patterns (`spat`)
+================================
+
+Since we are reasoning in a spatial logic, when eliminating a lemma or
+hypothesis of type ``P_0 -∗ ... -∗ P_n -∗ R``, one has to specify how the
+hypotheses are split between the premises. The proof mode supports the following
+_specialization patterns_ to express splitting of hypotheses:
+
+- `H` : use the hypothesis `H`, which should match the premise exactly. If `H` is
+  spatial, it will be consumed.
+- `(H spat1 .. spatn)` : first recursively specialize the hypothesis `H` using
+  the specialization patterns `spat1 .. spatn`, and finally use the result of
+  the specialization of `H`, which should match the premise exactly. If `H` is
+  spatial, it will be consumed.
+- `[H1 .. Hn]` and `[H1 .. Hn //]` : generate a goal for the premise with the
+  (spatial) hypotheses `H1 ... Hn` and all intuitionistic hypotheses. The
+  spatial hypotheses among `H1 ... Hn` will be consumed, and will not be
+  available for subsequent goals. Hypotheses prefixed with a `$` will be framed
+  in the goal for the premise. The pattern can be terminated with a `//`, which
+  causes `done` to be called to close the goal (after framing).
+- `[-H1 ... Hn]` and `[-H1 ... Hn //]` : the negated forms of the above
+  patterns, where the goal for the premise will have all spatial premises except
+  `H1 .. Hn`.
+- `[> H1 ... Hn]` and `[> H1 ... Hn //]` : like the above patterns, but these
+  patterns can only be used if the goal is a modality `M`, in which case
+  the goal for the premise will be wrapped in the modality `M`.
+- `[> -H1 ... Hn]` and `[> -H1 ... Hn //]` : the negated forms of the above
+  patterns.
+- `[# $H1 .. $Hn]` and `[# $H1 .. $Hn //]` : generate a goal for a persistent
+  premise in which all hypotheses are available. This pattern does not consume
+  any hypotheses; all hypotheses are available in the goal for the premise as
+  well in the subsequent goal. The hypotheses `$H1 ... $Hn` will be framed in
+  the goal for the premise. These patterns can be terminated with a `//`, which
+  causes `done` to be called to close the goal (after framing).
+- `[%]` and `[% //]` : generate a Coq goal for a pure premise. This pattern
+  does not consume any hypotheses. The pattern can be terminated with a `//`
+  which causes `done` to be called to close the goal.
+- `[$]` : solve the premise by framing. It will first repeatedly frame and
+  consume the spatial hypotheses, and then repeatedly frame the intuitionistic
+  hypotheses. Spatial hypotheses that are not framed are carried over to the
+  subsequent goal.
+- `[> $]` : like the above pattern, but this pattern can only be used if the
+  goal is a modality `M`, in which case the goal for the premise will be wrapped
+  in the modality `M` before framing.
+- `[# $]` : solve the persistent premise by framing. It will first repeatedly
+  frame the spatial hypotheses, and then repeatedly frame the intuitionistic
+  hypotheses. This pattern does not consume any hypotheses.
+
+For example, given:
+
+        H : □ P -∗ P 2 -∗ R -∗ x = 0 -∗ Q1 ∗ Q2
+
+One can write:
+
+        iDestruct ("H" with "[#] [H1 $H2] [$] [% //]") as "[H4 H5]".
+
+
+Proof mode terms (`pm_trm`)
+===========================
+
+Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
+take both hypotheses and lemmas, and allow one to instantiate universal
+quantifiers and implications/wands of these hypotheses/lemmas on the fly.
+
+The syntax for the arguments of these tactics, called _proof mode terms_, is:
+
+        (H $! t1 ... tn with "spat1 .. spatn")
+
+Here, `H` can be either a hypothesis or a Coq lemma whose conclusion is
+of the shape `P ⊢ Q`. In the above, `t1 ... tn` are arbitrary Coq terms used
+for instantiation of universal quantifiers, and `spat1 .. spatn` are
+[specialization patterns][spat] to eliminate implications and wands.
+
+Proof mode terms can be written down using the following shorthand syntaxes, too:
+
+        (H with "spat1 .. spatn")
+        (H $! t1 ... tn)
+        H
+
+HeapLang tactics
+================
+
+If you came here looking for the `wp_` tactics, those are described in the
+[HeapLang documentation](./heap_lang.md).

docs/resource_algebras.md

+## Global resource algebra management
+
+The type of Iris propositions `iProp Σ` is parameterized by a *global* list `Σ:
+gFunctors` of resource algebras that the proof may use.  (Actually this list
+contains functors instead of resource algebras, but you only need to worry about
+that when dealing with higher-order ghost state -- see "Camera functors" below.)
+
+In our proofs, we always keep the `Σ` universally quantified to enable composition of proofs.
+Each proof just assumes that some particular resource algebras are contained in that global list.
+This is expressed via the `inG Σ R` typeclass, which roughly says that `R ∈ Σ`
+("`R` is in the `G`lobal list of RAs `Σ` -- hence the `G`).
+
+Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
+not have to expose to clients what exactly their resource algebras are. For
+example, in the [one-shot example](../tests/one_shot.v), we have:
+```coq
+Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
+Local Existing Instances one_shot_inG.
+```
+Here, the projection `one_shot_inG` is registered as an instance for type-class
+resolution. If you need several resource algebras, just add more `inG` fields.
+If you are using another module as part of yours, add a field like
+`one_shot_other : otherG Σ`. All of these fields should be added to the
+`Local Existing Instances` command.
+
+The code above enables these typeclass instances only in the surrounding file
+where they are used to define the new abstractions by the library. The
+interface of these abstractions will only depend on the `one_shotG` class.
+Since `one_shot_inG` will be hidden from clients, they will not accidentally
+rely on it in their code.
+
+Having defined the type class, we need to provide a way to instantiate it.  This
+is an important step, as not every resource algebra can actually be used: if
+your resource algebra refers to `Σ`, the definition becomes recursive.  That is
+actually legal under some conditions (see "Camera functors" below), but for now
+we will ignore that case.  We have to define a list that contains all the
+resource algebras we need:
+```coq
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
+```
+This time, there is no `Σ` in the context, so we cannot accidentally introduce a
+bad dependency.  If you are using another module as part of yours, add their
+`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`.  (The
+`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
+other; together with a coercion from a single functor to a singleton list, this
+means lists can be nested arbitrarily.)
+
+Now we can define the one and only instance that our type class will ever need:
+```coq
+Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Proof. solve_inG. Qed.
+```
+The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
+global list `Σ`.  Typically, this should be the only assumption your instance
+needs, showing that the assumptions of the module (and all the modules it
+uses internally) can trivially be satisfied by picking the right `Σ`.
+
+Now you can add `one_shotG` as an assumption to all your module definitions and
+proofs.  We typically use a section for this:
+```coq
+Section proof.
+Context `{!heapGS Σ, !one_shotG Σ}.
+```
+Notice that besides our own assumptions `one_shotG`, we also assume `heapGS`,
+which are assumptions that every HeapLang proof makes (they are related to
+defining the `↦` connective as well as the basic Iris infrastructure for
+invariants and WP).  For this purpose, `heapGS` contains not only assumptions
+about `Σ`, it also contains some ghost names to refer to particular ghost state
+(see "global ghost state instances" below).
+
+The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
+generalize the `Σ`.  When adding assumptions with backtick, you should most of
+the time also add a `!` in front of every assumption.  If you do not then Coq
+will also automatically generalize all indices of type-classes that you are
+assuming.  This can easily lead to making more assumptions than you are aware
+of, and often it leads to duplicate assumptions which breaks type class
+resolutions.
+
+## Resource algebra combinators
+
+Defining a new resource algebra `one_shotR` for each new proof and verifying all
+the algebra laws would be quite cumbersome, so instead Iris provides a rich set
+of resource algebra combinators that one can use to build up the desired
+resource algebras. For example, `one_shotR` is defined as follows:
+
+```coq
+Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
+```
+
+The suffixes `R` and `O` indicate that we are not working on the level of Coq
+types here, but on the level of `R`esource algebras and `O`FEs,
+respectively. Unfortunately this means we cannot use Coq's usual type notation
+(such as `*` for products and `()` for the unit type); we have to spell out the
+underlying OFE or resource algebra names instead.
+
+## Obtaining a closed proof
+
+To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
+`inG`, you have to assemble a list of functors of all the involved modules,
+and if your proof relies on some singleton (most do, at least indirectly; also
+see the next section), you have to call the respective initialization or
+adequacy lemma.  [For example](../tests/one_shot.v):
+```coq
+Section client.
+  Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
+
+  Lemma client_safe : WP client {{ _, True }}%I.
+  (* ... *)
+End client.
+
+(** Assemble all functors needed by the [client_safe] proof. *)
+Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
+
+(** Apply [heap_adequacy] with this list of all functors. *)
+Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
+Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+```
+
+## Advanced topic: Ghost state singletons
+
+Some Iris modules involve a form of "global state".  For example, defining the
+`↦` for HeapLang involves a piece of ghost state that matches the current
+physical heap.  The `gname` of that ghost state must be picked once when the
+proof starts, and then globally known everywhere.  Hence `gen_heapGS`, the type
+class for the generalized heap module, bundles the usual `inG` assumptions
+together with the `gname`:
+```coq
+Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
+}.
+
+Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
+  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
+  gen_heap_name : gname;
+}.
+```
+The trailing `S` here is for "singleton", because the idea is that only one
+instance of `gen_heapGS` ever exists. This is important, since two instances
+might have different `gname`s, so `↦` based on these two distinct instances
+would be incompatible with each other.
+
+The `gen_heapGpreS` typeclass (without the singleton data) is relevant for
+initialization, i.e., to create an instance of `gen_heapGS`. This is happening as
+part of [`heap_adequacy`](../iris_heap_lang/adequacy.v) using the
+initialization lemma for `gen_heapGS` from
+[`gen_heap_init`](../iris/base_logic/lib/gen_heap.v):
+```coq
+Lemma gen_heap_init `{gen_heapGpreS L V Σ} σ :
+  (|==> ∃ _ : gen_heapGS L V Σ, gen_heap_ctx σ)%I.
+```
+These lemmas themselves only make assumptions the way normal modules (those
+without global state) do. Just like in the normal case, `somethingGpreS` type
+classes have an `Instance` showing that a `subG` is enough to instantiate them:
+```coq
+Global Instance subG_gen_heapGpreS {Σ L V} `{Countable L} :
+  subG (gen_heapΣ L V) Σ → gen_heapGpreS L V Σ.
+Proof. solve_inG. Qed.
+```
+The initialization lemma then shows that the `somethingGpreS` type class is
+enough to create an instance of the main `somethingGS` class *below a view
+shift*.  This is written with an existential quantifier in the lemma because the
+statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
+an instance of `gen_heapGS` in the context.
+
+Given that these global ghost state instances are singletons, they must be
+assumed explicitly everywhere.  Bundling `heapGS` in a (non-singleton) module
+type class like `one_shotG` would lose track of the fact that there exists just
+one `heapGS` instance that is shared by everyone.
+
+## Advanced topic: Camera functors and higher-order ghost state
+
+As we already alluded to, `Σ` actually consists of functors, not resource
+algebras. This enables you to use *higher-order ghost state*: ghost state that
+recursively refers to `iProp`.
+
+**Background: Iris Model.** To understand how this works, we have to dig a bit
+into the model of Iris. In Iris, the type of propositions `iProp` is described
+by the solution to the recursive domain equation:
+
+```coq
+iProp ≅ uPred (F (iProp))
+```
+
+Here, `uPred M` describes "propositions with resources of type `M`".  The
+peculiar aspect of this definition is that the notion of resources can itself
+refer to the set propositions that we are just defining; that dependency is
+expressed by `F`.  `F` is a user-chosen locally contractive bifunctor from COFEs
+to unital Cameras (a step-indexed generalization of unital resource
+algebras). Having just a single fixed `F` would however be rather inconvenient,
+so instead we have a list `Σ`, and then we define the global functor `F_global`
+roughly as follows:
+
+```coq
+F_global X := Π_{F ∈ Σ} gmap nat (F X)
+```
+
+In other words, each functor in `Σ` is applied to the recursive argument `X`,
+wrapped in a finite partial function, and then we take a big product of all of
+that.  The product ensures that all `F ∈ Σ` are available, and the `gmap` is
+needed to provide the proof rule `own_alloc`, which lets you create new
+instances of the given type of resource any time.
+
+However, this on its own would be too restrictive, as it requires all
+occurrences of `X` to be in positive positions (otherwise the functor laws
+would not hold for `F`).  To mitigate this, we instead work with "bifunctors":
+functors that take two arguments, `X` and `X⁻`, where `X⁻` is used for
+negative positions.  This leads us to the following domain equation:
+
+```coq
+iProp ≅ uPred (F_global (iProp,iProp))
+F_global (X,X⁻) := Π_{F ∈ Σ} gmap nat (F (X,X⁻))
+```
+
+To make this equation well-defined, the bifunctors `F ∈ Σ` need to be "contractive".
+For further details, see §7.4 of
+[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.3.pdf); here we
+describe the user-side Coq aspects of this approach.
+
+Below, when we say "functor", we implicitly mean "bifunctor".
+
+**Higher-order ghost state.** To use higher-order ghost state, you need to give
+a functor whose "hole" will later be filled with `iProp` itself. For example,
+let us say you would like to have ghost state of type `gmap K (agree (nat *
+later iProp))`, using the "type-level" `later` operator which ensures
+contractivity.  Then you will have to define a functor such as:
+
+```coq
+F (X,X⁻) := gmap K (agree (nat * ▶ X))
+```
+
+To make it convenient to construct such functors and prove their contractivity,
+we provide a number of abstractions:
+
+- [`oFunctor`](../iris/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](../iris/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](../iris/algebra/cmra.v): functors from COFEs to unital
+  cameras.
+
+Besides, there are the classes `oFunctorContractive`, `rFunctorContractive`, and
+`urFunctorContractive` which describe the subset of the above functors that are
+contractive.
+
+To compose these functors, we provide a number of combinators, e.g.:
+
+- `constOF (A : ofe) : oFunctor            := λ (B,B⁻), A `
+- `idOF : oFunctor                         := λ (B,B⁻), B`
+- `prodOF (F1 F2 : oFunctor) : oFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
+- `ofe_morOF (F1 F2 : oFunctor) : oFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
+- `laterOF (F : oFunctor) : oFunctor       := λ (B,B⁻), later (F (B,B⁻))`
+- `agreeRF (F : oFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
+- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
+
+Note in particular how the functor for the function space, `ofe_morOF`, swaps
+`B` and `B⁻` for the functor `F1` describing the domain.  This reflects the fact
+that that functor is used in a negative position.
+
+Using these combinators, one can easily construct bigger functors in point-free
+style and automatically infer their contractivity, e.g:
+
+```coq
+F := gmapURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
+```
+
+which effectively defines the desired example functor
+`F := λ (B,B⁻), gmap K (agree (nat * later B))`.
+
+To make it a little bit more convenient to write down such functors, we make
+the constant functors (`constOF`, `constRF`, and `constURF`) a coercion, and
+provide the usual notation for products, etc. So the above functor can be
+written as follows:
+
+```coq
+F := gmapRF K (agreeRF (natO * ▶ ∙))
+```
+
+Basically, the functor can be written "as if" you were writing a resource
+algebra, except that there need to be extra "F" suffixes to indicate that we are
+working with functors, and the desired recursive `iProp` is replaced by the
+"hole" `∙`.
+
+Putting it all together, the `libG` typeclass and `libΣ` list of functors for
+your example would look as follows:
+
+```coq
+Class libG Σ :=
+  { #[local] lib_inG :: inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+
+Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
+Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
+Proof. solve_inG. Qed.
+```
+
+It is instructive to remove the `▶` and see what happens: the `libG` class still
+works just fine, but `libΣ` complains that the functor is not contractive. This
+demonstrates the importance of always defining a `libΣ` alongside the `libG` and
+proving their relation.

docs/style_guide.md

+# Iris proof style
+
+**Warning:** this document is still in development and rather incomplete.
+If you run across a question of style (for example, something comes
+up in an MR) and it's not on this list, please do reach out to us on Mattermost
+so we can add it.
+
+## Basic syntax
+
+### Binders
+
+This applies to Context, Implicit Types, and definitions.
+
+- **Put a space on both sides of the colon.**
+
+  Good: `(a : B)` <br>
+  Bad: `(a:B)`, `(a: B)`
+
+- **Prefer `(a : B)` to `a : B`.** (TODO)
+
+
+### Patterns
+
+#### Disjunctions & branches
+
+- **Always mark the disjuncts when destructuring a disjunctive pattern, even if you don't bind anything, to indicate that the proof branches.**
+
+  Good:
+  ```coq
+  Lemma foo : ∀ b : bool, b = true ∨ b = false.
+  Proof.
+    intros [|].
+    ...
+  ```
+
+  Bad:
+  ```coq
+  Lemma foo : ∀ b : bool, b = true ∨ b = false.
+  Proof.
+    intros [].
+    ...
+  ```
+
+#### Uncategorized
+
+- **Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`.** (TODO)
+
+### Unicode
+
+- **Always use Unicode variants of forall, exists, ->, <=, >=.**
+
+  Good: `∀ ∃ → ≤ ≥`<br>
+  Bad: `forall exists -> <= >=`
+
+### Equivalent vernacular commands
+
+- **Use `Context`, never `Variable`.**
+
+- **Use `Implicit Types`, never `Implicit Type`.** (TODO)
+
+- **Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`, `Remark`)**.
+
+- **Always add `Global` or `Local` to `Hint`, `Arguments`, and `Instance`.** (TODO)
+
+### `Require`
+
+- **Never put `Require` in the middle of a file.** All `Require` must be at the top.
+If you only want to *import* a certain module in some specific place (for instance, in a `Section` or other `Module`), you can do something like:
+
+  ```coq
+  From lib Require component.
+  
+  (* ... *)
+  
+  Import component.
+  ```
+
+### Ltac
+
+- **Prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."`.** This is better because the latter will fail if `t1` doesn't make progress. See https://gitlab.mpi-sws.org/iris/iris/-/issues/216. Note that `first [ t1 | fail "..."]` is simply incorrect; the failure message will never show up and will be replaced with a generic failure.
+
+### Coqdoc comments
+
+- **Module-level comments (covering the entire file) go at the top of the file, before the `Require`.**
+
+### Uncategorized
+
+- **Indent the body of a match by one space.**
+
+  Good:
+  ```coq
+  match foo with
+  | Some x =>
+     long line here using 
+  ```
+  
+  *RJ*: This is odd, usually everything is in (multiples of) 2 spaces, I think.
+  
+  *Tej*: https://gitlab.mpi-sws.org/iris/iris/-/blob/920bc3d97b8830139045e1780f2aff4d05b910cd/iris_heap_lang/proofmode.v#L194
+
+- **Avoid using the extra square brackets around an Ltac match.**
+
+  Good:
+  ```coq
+  match goal with
+  | |- ?g => idtac g
+  
+  ```
+  
+  Bad:
+  ```coq
+  match goal with
+  | [ |- ?g ] => idtac g
+  
+  ```
+
+- **Use coqdoc syntax in comments for Coq identifiers and inline code, e.g. `[cmraT]`.**
+
+- **Put proofs either all on one line (`Proof. reflexivity. Qed.`) or split up the usual way with indentation.**
+
+  Bad:
+  
+  ```coq
+  Lemma foo : 2 + 2 = 4 ∧ 1 + 2 = 3.
+  Proof. split.
+    - reflexivity.
+    - done.
+  Qed.
+  ```
+
+- **Put the entire theorem statement on one line or one premise per line, indented by 2 spaces.**
+
+  Bad:
+  
+  ```coq
+  Lemma foo x y z :
+      x < y → y < z →
+      x < z.
+  ```
+  
+  Good:
+  
+  ```coq
+  Lemma foo x y z : x < y → y < z → x < z.
+  ```
+  
+  Good: (particularly if premises are longer)
+  
+  ```coq
+  Lemma foo x y z :
+    x < y →
+    y < z →
+    x < z.
+  ```
+
+- **If the parameters before the `:` become too long, indent later lines by 4 spaces and always have a newline after `:`.**
+
+  Bad:
+  
+  ```coq
+  Lemma foo (very_long_name : has_a_very_long_type)
+  (even_longer_name : has_an_even_longer_type) : x < y → y < z →
+    x < z.
+  ```
+  
+  Good:
+  
+  ```coq
+  Lemma foo (very_long_name : has_a_very_long_type)
+      (even_longer_name : has_an_even_longer_type) :
+    x < y → y < z → x < z.
+  ```
+
+- **For definitions that don't fit into one line, put `:=` before the linebreak, not after.**
+
+  Bad:
+  
+  ```coq
+  Definition foo (arg1 arg2 arg3 : name_of_the_type)
+    := the body that is very long.
+  ```
+  
+  Good:
+  
+  ```coq
+  Definition foo (arg1 arg2 arg3 : name_of_the_type) :=
+    the body that is very long.
+  ```
+
+- **For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.**
+
+- **For long `t1; t2; t3` and `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces.**
+
+  Good:
+  ```coq
+  t;
+    [t1
+    |t2
+    |t3].
+  ```
+  
+  ```coq
+  t;
+    t1;
+    t2.
+  ```
+
+
+
+## File organization
+theories/algebra is for primitive ofe/RA/CMRA constructions
+theories/algebra/lib is for derived constructions
+theories/base_logic/lib is for constructions in the base logic (using own)
+
+## Naming
+* `*_ctx` for persistent facts (often an invariant) needed by everything in a library
+* `*_interp` for a function from some representation to iProp
+* If you have lemma `foo` which is an iff and you want single direction versions, name them `foo_1` (forward) and `foo_2` (backward)
+* If you have a lemma `foo` parametrized by an equivalence relation, you might want a version specialized to Leibniz equality for better rewrite support; name that version `foo_L` and state it with plain equality (e.g., `dom_empty_L` in stdpp). You might take an assumption `LeibnizEquiv A` if the original version took an equivalence (say the OFE equivalence) to assume that the provided equivalence is plain equality.
+* Lower-case theorem names, lower-case types, upper-case constructors
+* **TODO:** how should `f (g x) = f' (g' x)` be named?
+* `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
+* Operations that "extract" from the data structure (`lookup`, `elem_of`, ...) should come before operations that "alter" the data structure (`filter`, `insert`, `union`, `fmap`). For example, use `map_lookup_filter` instead of `map_filter_lookup`.
+* Injectivity theorems are instances of `Inj` and then are used with `inj`
+* Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant).
+* Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
+  these since the name doesn't convey how `foo'` is related to `foo`.
+* Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work.
+* For lemmas involving modalities, we usually follow this naming scheme:
+    ```
+    M1_into_M2: M1 P ⊢ M2 P
+    M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
+    M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
+    M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
+    ```
+* Monotonicity lemmas where the relation can be ambiguous are called `<f>_<relation>_mono`, e.g. `Some_included_mono`.
+* For lemmas `f x = g ...` that give a definition of function `f` in terms of `g`, we use `f_as_g`. For example, `map_compose_as_omap : m ∘ₘ n = omap (m !!.) n`.
+
+### Naming algebra libraries
+
+**TODO:** describe any conclusions we came to with the `mono_nat` library
+
+## Parameter order and implicitness for lemmas
+
+* Parameter order is usually from more higher-order to less higher-order (types, functions, plain values), and otherwise follows the order in which variables appear in the lemma statement.
+* In new lemmas, arguments should be marked as implicit when they can be inferred by unification in all intended usage scenarios. (If an argument can *sometimes* be inferred, we do not have a clear guideline yet -- consider on a case-by-case basis, for now.)
+
+## Lemma statements
+
+### Iris lemmas: `-∗` vs `⊢`
+
+* For low-level lemmas, in particular if there is a high likelihood someone would want to rewrite with it / use them in non-proofmode goals (e.g. modality intro rules), use `⊢`
+  * `P ⊢ |==£> P`
+  * `(|==£> |==£> P) ⊢ |==£> P`
+  * `▷ own γ a ⊢ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b)`
+  * `(P -∗ Q) i ⊢ (P i -∗ Q i)`
+* If a lemma is a Coq implication of Iris entailments (where the entailments are visible, not hidden behind e.g. `Persistent`), then use `⊢`
+  * `(P1 ⊢ P2) → recv l P1 ⊢ recv l P2`
+* Else use -∗
+  * `a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'` (curried and hence not rewrite-friendly)
+
+## Metavariables
+**TODO:** move these to the right place
+
+* `P` `Q` for bi:PROP (or specifically `iProp Σ`)
+* `Φ` and `Ψ` for (?A -> iProp), like postconditions
+* `φ` and `ψ` for `Prop`
+* `A` `B` for types, ofeT, or cmraT
+
+Suffixes like O, R, UR (already documented)

docs/vim_ultisnips

+snippet \forall "" i
+∀
+endsnippet
+snippet \exists "" i
+∃
+endsnippet
+snippet \lam "" i
+λ
+endsnippet
+snippet \not "" i
+¬
+endsnippet
+snippet \lor "" i
+∨
+endsnippet
+snippet \land "" i
+∧
+endsnippet
+snippet \/ "" i
+∨
+endsnippet
+snippet /\ "" i
+∧
+endsnippet
+snippet \rightarrow "" i
+→
+endsnippet
+snippet \implies "" i
+→
+endsnippet
+snippet -> "" i
+→
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet <-> "" i
+↔
+endsnippet
+snippet \<- "" i
+←
+endsnippet
+snippet \cong "" i
+≡
+endsnippet
+snippet \== "" i
+≡
+endsnippet
+snippet \/== "" i
+≢
+endsnippet
+snippet \neq "" i
+≠
+endsnippet
+snippet /= "" i
+≠
+endsnippet
+snippet \less "" i
+≤
+endsnippet
+snippet \le "" i
+≤
+endsnippet
+snippet <= "" i
+≤
+endsnippet
+snippet \in "" i
+∈
+endsnippet
+snippet \notin "" i
+∉
+endsnippet
+snippet \cup "" i
+∪
+endsnippet
+snippet \cap "" i
+∩
+endsnippet
+snippet \setminus "" i
+∖
+endsnippet
+snippet \subset "" i
+⊂
+endsnippet
+snippet \subseteq "" i
+⊆
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \notsubseteq "" i
+⊈
+endsnippet
+snippet \meet "" i
+⊓
+endsnippet
+snippet \join "" i
+⊔
+endsnippet
+snippet \true "" i
+⊤
+endsnippet
+snippet \top "" i
+⊤
+endsnippet
+snippet \false "" i
+⊥
+endsnippet
+snippet \bottom "" i
+⊥
+endsnippet
+snippet \vdash "" i
+⊢
+endsnippet
+snippet \dashv "" i
+⊣
+endsnippet
+snippet \vDash "" i
+⊨
+endsnippet
+snippet \Vdash
+⊩
+endsnippet
+snippet \infty "" i
+∞
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \prf "" i
+↾
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+snippet \mapsto "" i
+↦
+endsnippet
+snippet \hookrightarrow "" i
+↪
+endsnippet
+snippet \up "" i
+↑
+endsnippet
+snippet \uparrow "" i
+↑
+endsnippet
+
+snippet \fun "" i
+λ
+endsnippet
+snippet \mult "" i
+⋅
+endsnippet
+snippet \ent "" i
+⊢
+endsnippet
+snippet \valid "" i
+✓
+endsnippet
+snippet \diamond "" i
+◇
+endsnippet
+snippet \box "" i
+□
+endsnippet
+snippet \bbox "" i
+■
+endsnippet
+snippet \eval "" i
+▷
+endsnippet
+snippet \rhd "" i
+▷
+endsnippet
+snippet \later "" i
+▷
+endsnippet
+snippet \pred "" i
+φ
+endsnippet
+snippet \and "" i
+∧
+endsnippet
+snippet \or "" i
+∨
+endsnippet
+snippet \circ "" i
+∘
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \ccomp "" i
+◎
+endsnippet
+snippet \pound "" i
+£
+endsnippet
+snippet \all "" i
+∀
+endsnippet
+snippet \ex "" i
+∃
+endsnippet
+snippet \to "" i
+→
+endsnippet
+snippet \ast "" i
+∗
+endsnippet
+snippet \sep "" i
+∗
+endsnippet
+snippet \ulc "" i
+⌜
+endsnippet
+snippet \urc "" i
+⌝
+endsnippet
+snippet \lc "" i
+⌜
+endsnippet
+snippet \rc "" i
+⌝
+endsnippet
+snippet \Lc "" i
+⎡
+endsnippet
+snippet \Rc "" i
+⎤
+endsnippet
+snippet \varnothing "" i
+∅
+endsnippet
+snippet \empty "" i
+∅
+endsnippet
+snippet \Lam "" i
+Λ
+endsnippet
+snippet \Sig "" i
+Σ
+endsnippet
+snippet \- "" i
+∖
+endsnippet
+snippet \aa "" i
+●
+endsnippet
+snippet \af "" i
+◯
+endsnippet
+snippet \auth "" i
+●
+endsnippet
+snippet \frag "" i
+◯
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet \gname "" i
+γ
+endsnippet
+snippet \incl "" i
+≼
+endsnippet
+snippet \latert "" i
+▶
+endsnippet
+snippet \update "" i
+⇝
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+
+
+snippet ^^+ "" i
+⁺
+endsnippet
+snippet __+ "" i
+₊
+endsnippet
+snippet ^^- "" i
+⁻
+endsnippet
+snippet __0 "" i
+₀
+endsnippet
+snippet __1 "" i
+₁
+endsnippet
+snippet __2 "" i
+₂
+endsnippet
+snippet __3 "" i
+₃
+endsnippet
+snippet __4 "" i
+₄
+endsnippet
+snippet __5 "" i
+₅
+endsnippet
+snippet __6 "" i
+₆
+endsnippet
+snippet __7 "" i
+₇
+endsnippet
+snippet __8 "" i
+₈
+endsnippet
+snippet __9 "" i
+₉
+endsnippet
+
+snippet __a "" i
+ₐ
+endsnippet
+snippet __e "" i
+ₑ
+endsnippet
+snippet __h "" i
+ₕ
+endsnippet
+snippet __i "" i
+ᵢ
+endsnippet
+snippet __k "" i
+ₖ
+endsnippet
+snippet __l "" i
+ₗ
+endsnippet
+snippet __m "" i
+ₘ
+endsnippet
+snippet __n "" i
+ₙ
+endsnippet
+snippet __o "" i
+ₒ
+endsnippet
+snippet __p "" i
+ₚ
+endsnippet
+snippet __r "" i
+ᵣ
+endsnippet
+snippet __s "" i
+ₛ
+endsnippet
+snippet __t "" i
+ₜ
+endsnippet
+snippet __u "" i
+ᵤ
+endsnippet
+snippet __v "" i
+ᵥ
+endsnippet
+snippet __x "" i
+ₓ
+endsnippet
+
+snippet \Alpha "" i
+Α
+endsnippet
+snippet \alpha "" i
+α
+endsnippet
+snippet \Beta "" i
+Β
+endsnippet
+snippet \beta "" i
+β
+endsnippet
+snippet \Gamma "" i
+Γ
+endsnippet
+snippet \gamma "" i
+γ
+endsnippet
+snippet \Delta "" i
+Δ
+endsnippet
+snippet \delta "" i
+δ
+endsnippet
+snippet \Epsilon "" i
+Ε
+endsnippet
+snippet \epsilon "" i
+ε
+endsnippet
+snippet \Zeta "" i
+Ζ
+endsnippet
+snippet \zeta "" i
+ζ
+endsnippet
+snippet \Eta "" i
+Η
+endsnippet
+snippet \eta "" i
+η
+endsnippet
+snippet \Theta "" i
+Θ
+endsnippet
+snippet \theta "" i
+θ
+endsnippet
+snippet \Iota "" i
+Ι
+endsnippet
+snippet \iota "" i
+ι
+endsnippet
+snippet \Kappa "" i
+Κ
+endsnippet
+snippet \kappa "" i
+κ
+endsnippet
+snippet \Lamda "" i
+Λ
+endsnippet
+snippet \lamda "" i
+λ
+endsnippet
+snippet \Lambda "" i
+Λ
+endsnippet
+snippet \lambda "" i
+λ
+endsnippet
+snippet \Mu "" i
+Μ
+endsnippet
+snippet \mu "" i
+μ
+endsnippet
+snippet \Nu "" i
+Ν
+endsnippet
+snippet \nu "" i
+ν
+endsnippet
+snippet \Xi "" i
+Ξ
+endsnippet
+snippet \xi "" i
+ξ
+endsnippet
+snippet \Omicron "" i
+Ο
+endsnippet
+snippet \omicron "" i
+ο
+endsnippet
+snippet \Pi "" i
+Π
+endsnippet
+snippet \pi "" i
+π
+endsnippet
+snippet \Rho "" i
+Ρ
+endsnippet
+snippet \rho "" i
+ρ
+endsnippet
+snippet \Sigma "" i
+Σ
+endsnippet
+snippet \sigma "" i
+σ
+endsnippet
+snippet \Tau "" i
+Τ
+endsnippet
+snippet \tau "" i
+τ
+endsnippet
+snippet \Upsilon "" i
+Υ
+endsnippet
+snippet \upsilon "" i
+υ
+endsnippet
+snippet \Phi "" i
+Φ
+endsnippet
+snippet \phi "" i
+ϕ
+endsnippet
+snippet \varphi "" i
+φ
+endsnippet
+snippet \Chi "" i
+Χ
+endsnippet
+snippet \chi "" i
+χ
+endsnippet
+snippet \Psi "" i
+Ψ
+endsnippet
+snippet \psi "" i
+ψ
+endsnippet
+snippet \Omega "" i
+Ω
+endsnippet
+snippet \omega "" i
+ω
+endsnippet

docs/vscode

+  "generic-input-methods.input-methods": [
+        {
+            "name": "Iris Math",
+            "commandName": "text.math",
+            "languages": [
+                "coq"
+            ],
+            "triggers": [
+                "\\"
+            ],
+            "dictionary": [
+                // Standard LaTeX math notations
+                { "label": "forall", "body": "∀", "description": "∀" },
+                { "label": "exists", "body": "∃", "description": "∃" },
+                { "label": "lam", "body": "λ", "description": "λ" },
+                { "label": "not", "body": "¬", "description": "¬" },
+                { "label": "->", "body": "→", "description": "→" },
+                { "label": "<->", "body": "↔", "description": "↔" },
+                { "label": "<-", "body": "←", "description": "←" },
+                { "label": "==", "body": "≡", "description": "≡" },
+                { "label": "/==", "body": "≢", "description": "≢" },
+                { "label": "/=", "body": "≠", "description": "≠" },
+                { "label": "neq", "body": "≠", "description": "≠" },
+                { "label": "nequiv", "body": "≢", "description": "≢" },
+                { "label": "<=", "body": "≤", "description": "≤" },
+                { "label": "leq", "body": "≤", "description": "≤" },
+                { "label": "in", "body": "∈", "description": "∈" },
+                { "label": "notin", "body": "∉", "description": "∉" },
+                { "label": "cup", "body": "∪", "description": "∪" },
+                { "label": "cap", "body": "∩", "description": "∩" },
+                { "label": "setminus", "body": "∖", "description": "∖" },
+                { "label": "subset", "body": "⊂", "description": "⊂" },
+                { "label": "subseteq", "body": "⊆", "description": "⊆" },
+                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
+                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
+                { "label": "notsubseteq", "body": "⊈", "description": "⊈" },
+                { "label": "meet", "body": "⊓", "description": "⊓" },
+                { "label": "join", "body": "⊔", "description": "⊔" },
+                { "label": "top", "body": "⊤", "description": "⊤" },
+                { "label": "bottom", "body": "⊥", "description": "⊥" },
+                { "label": "vdash", "body": "⊢", "description": "⊢" },
+                { "label": "|-", "body": "⊢", "description": "⊢" },
+                { "label": "dashv", "body": "⊣", "description": "⊣" },
+                { "label": "Vdash", "body": "⊨", "description": "⊨" },
+                { "label": "infty", "body": "∞", "description": "∞" },
+                { "label": "comp", "body": "∘", "description": "∘" },
+                { "label": "prf", "body": "↾", "description": "↾" },
+                { "label": "bind", "body": "≫=", "description": "≫=" },
+                { "label": "mapsto", "body": "↦", "description": "↦" },
+                { "label": "hookrightarrow", "body": "↪", "description": "↪" },
+                { "label": "uparrow", "body": "↑", "description": "↑" },
+
+                // Iris specific
+                { "label": "fun", "body": "λ", "description": "λ" },
+                { "label": "mult", "body": "⋅", "description": "⋅" },
+                { "label": "ent", "body": "⊢", "description": "⊢" },
+                { "label": "valid", "body": "✓", "description": "✓" },
+                { "label": "diamond", "body": "◇", "description": "◇" },
+                { "label": "box", "body": "□", "description": "□" },
+                { "label": "bbox", "body": "■", "description": "■" },
+                { "label": "later", "body": "▷", "description": "▷" },
+                { "label": "pred", "body": "φ", "description": "φ" },
+                { "label": "and", "body": "∧", "description": "∧" },
+                { "label": "or", "body": "∨", "description": "∨" },
+                { "label": "comp", "body": "∘", "description": "∘" },
+                { "label": "ccomp", "body": "◎", "description": "◎" },
+                { "label": "all", "body": "∀", "description": "∀" },
+                { "label": "ex", "body": "∃", "description": "∃" },
+                { "label": "to", "body": "→", "description": "→" },
+                { "label": "sep", "body": "∗", "description": "∗" },
+                { "label": "star", "body": "∗", "description": "∗" },
+                { "label": "lc", "body": "⌜", "description": "⌜" },
+                { "label": "rc", "body": "⌝", "description": "⌝" },
+                { "label": "Lc", "body": "⎡", "description": "⎡" },
+                { "label": "Rc", "body": "⎤", "description": "⎤" },
+                { "label": "empty", "body": "∅", "description": "∅" },
+                { "label": "Lam", "body": "Λ", "description": "Λ" },
+                { "label": "Sig", "body": "Σ", "description": "Σ" },
+                { "label": "-", "body": "∖", "description": "∖" },
+                { "label": "aa", "body": "●", "description": "●" },
+                { "label": "af", "body": "◯", "description": "◯" },
+                { "label": "auth", "body": "●", "description": "●" },
+                { "label": "frag", "body": "◯", "description": "◯" },
+                { "label": "iff", "body": "↔", "description": "↔" },
+                { "label": "gname", "body": "γ", "description": "γ" },
+                { "label": "incl", "body": "≼", "description": "≼" },
+                { "label": "latert", "body": "▶", "description": "▶" },
+                { "label": "update", "body": "⇝", "description": "⇝" },
+                { "label": "bind", "body": "≫=", "description": "≫=" },
+
+                // accents (for iLöb)
+                { "label": "\"o", "body": "ö", "description": "ö" },
+
+                // subscripts and superscripts
+                { "label": "^^+", "body": "⁺", "description": "⁺" },
+                { "label": "__+", "body": "₊", "description": "₊" },
+                { "label": "^^-", "body": "⁻", "description": "⁻" },
+                { "label": "__0", "body": "₀", "description": "₀" },
+                { "label": "__1", "body": "₁", "description": "₁" },
+                { "label": "__2", "body": "₂", "description": "₂" },
+                { "label": "__3", "body": "₃", "description": "₃" },
+                { "label": "__4", "body": "₄", "description": "₄" },
+                { "label": "__5", "body": "₅", "description": "₅" },
+                { "label": "__6", "body": "₆", "description": "₆" },
+                { "label": "__7", "body": "₇", "description": "₇" },
+                { "label": "__8", "body": "₈", "description": "₈" },
+                { "label": "__9", "body": "₉", "description": "₉" },
+                { "label": "__a", "body": "ₐ", "description": "ₐ" },
+                { "label": "__e", "body": "ₑ", "description": "ₑ" },
+                { "label": "__h", "body": "ₕ", "description": "ₕ" },
+                { "label": "__i", "body": "ᵢ", "description": "ᵢ" },
+                { "label": "__k", "body": "ₖ", "description": "ₖ" },
+                { "label": "__l", "body": "ₗ", "description": "ₗ" },
+                { "label": "__m", "body": "ₘ", "description": "ₘ" },
+                { "label": "__n", "body": "ₙ", "description": "ₙ" },
+                { "label": "__o", "body": "ₒ", "description": "ₒ" },
+                { "label": "__p", "body": "ₚ", "description": "ₚ" },
+                { "label": "__r", "body": "ᵣ", "description": "ᵣ" },
+                { "label": "__s", "body": "ₛ", "description": "ₛ" },
+                { "label": "__t", "body": "ₜ", "description": "ₜ" },
+                { "label": "__u", "body": "ᵤ", "description": "ᵤ" },
+                { "label": "__v", "body": "ᵥ", "description": "ᵥ" },
+                { "label": "__x", "body": "ₓ", "description": "ₓ" },
+
+                // Greek alphabet
+                { "label": "Alpha", "body": "Α", "description": "Α" },
+                { "label": "alpha", "body": "α", "description": "α" },
+                { "label": "Beta", "body": "Β", "description": "Β" },
+                { "label": "beta", "body": "β", "description": "β" },
+                { "label": "Gamma", "body": "Γ", "description": "Γ" },
+                { "label": "gamma", "body": "γ", "description": "γ" },
+                { "label": "Delta", "body": "Δ", "description": "Δ" },
+                { "label": "delta", "body": "δ", "description": "δ" },
+                { "label": "Epsilon", "body": "Ε", "description": "Ε" },
+                { "label": "epsilon", "body": "ε", "description": "ε" },
+                { "label": "Zeta", "body": "Ζ", "description": "Ζ" },
+                { "label": "zeta", "body": "ζ", "description": "ζ" },
+                { "label": "Eta", "body": "Η", "description": "Η" },
+                { "label": "eta", "body": "η", "description": "η" },
+                { "label": "Theta", "body": "Θ", "description": "Θ" },
+                { "label": "theta", "body": "θ", "description": "θ" },
+                { "label": "Iota", "body": "Ι", "description": "Ι" },
+                { "label": "iota", "body": "ι", "description": "ι" },
+                { "label": "Kappa", "body": "Κ", "description": "Κ" },
+                { "label": "kappa", "body": "κ", "description": "κ" },
+                { "label": "Lamda", "body": "Λ", "description": "Λ" },
+                { "label": "lamda", "body": "λ", "description": "λ" },
+                { "label": "Lambda", "body": "Λ", "description": "Λ" },
+                { "label": "lambda", "body": "λ", "description": "λ" },
+                { "label": "Mu", "body": "Μ", "description": "Μ" },
+                { "label": "mu", "body": "μ", "description": "μ" },
+                { "label": "Nu", "body": "Ν", "description": "Ν" },
+                { "label": "nu", "body": "ν", "description": "ν" },
+                { "label": "Xi", "body": "Ξ", "description": "Ξ" },
+                { "label": "xi", "body": "ξ", "description": "ξ" },
+                { "label": "Omicron", "body": "Ο", "description": "Ο" },
+                { "label": "omicron", "body": "ο", "description": "ο" },
+                { "label": "Pi", "body": "Π", "description": "Π" },
+                { "label": "pi", "body": "π", "description": "π" },
+                { "label": "Rho", "body": "Ρ", "description": "Ρ" },
+                { "label": "rho", "body": "ρ", "description": "ρ" },
+                { "label": "Sigma", "body": "Σ", "description": "Σ" },
+                { "label": "sigma", "body": "σ", "description": "σ" },
+                { "label": "Tau", "body": "Τ", "description": "Τ" },
+                { "label": "tau", "body": "τ", "description": "τ" },
+                { "label": "Upsilon", "body": "Υ", "description": "Υ" },
+                { "label": "upsilon", "body": "υ", "description": "υ" },
+                { "label": "Phi", "body": "Φ", "description": "Φ" },
+                { "label": "phi", "body": "φ", "description": "φ" },
+                { "label": "Chi", "body": "Χ", "description": "Χ" },
+                { "label": "chi", "body": "χ", "description": "χ" },
+                { "label": "Psi", "body": "Ψ", "description": "Ψ" },
+                { "label": "psi", "body": "ψ", "description": "ψ" },
+                { "label": "Omega", "body": "Ω", "description": "Ω" },
+                { "label": "omega", "body": "ω", "description": "ω" }
+            ]
+        }
+    ]

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -notation-overridden
+     -w -redundant-canonical-projection
+     -w -unknown-warning
+     -w -argument-scope-delimiter
+     -w -notation-incompatible-prefix
+)))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)