...
 
Commits (2526)
*.v gitlab-language=coq
*.vo
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
......@@ -8,6 +9,10 @@
.\#*
*~
*.bak
.coqdeps.d
.coq-native/
build-dep/
Makefile.coq
Makefile.coq.conf
*.crashcoqide
.env
image: coq:8.5
image: ralfjung/opam-ci:opam2
buildjob:
stages:
- build
variables:
CPU_CORES: "10"
.template: &template
stage: build
tags:
- coq
- fp
script:
- coqc -v
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'fgrep Axiom build-log.txt && exit 1'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- make validate
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
only:
- master
- timing
artifacts:
paths:
- build-time.txt
- /^ci/
except:
- triggers
- schedules
- api
## Build jobs
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1"
build-coq.8.10.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.dev"
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.1"
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
<!--
When reporting a bug, please always include the version of Iris you are using.
If you are using opam, you can determine your Iris version by running
opam show coq-iris -f version
-->
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
This diff is collapsed.
# Contributing to the Iris Coq Development
Here you can find some how-tos for various thing sthat might come up when doing
Iris development.
## How to submit a merge request
To contribute code, you need an [MPI-SWS GitLab account][account] (use the
"Register" tab). Please send your MPI-SWS GitLab username to [Ralf Jung][jung]
to enable personal projects for your account. Then you can fork the
[Iris git repository][iris], make your changes in your fork, and create a merge
request.
Please do *not* use the master branch of your fork, that might confuse CI. Use
a feature branch instead.
[account]: https://gitlab.mpi-sws.org/users/sign_in
[jung]: https://gitlab.mpi-sws.org/jung
[iris]: https://gitlab.mpi-sws.org/iris/iris
## How to update the std++ dependency
* Do the change in std++, push it.
* Wait for CI to publish a new std++ version on the opam archive, then run
`opam update iris-dev`.
* In Iris, change the `opam` file to depend on the new version.
* Run `make build-dep` (in Iris) to install the new version of std++.
You may have to do `make clean` as Coq will likely complain about .vo file
mismatches.
## How to write/update test cases
The files in `tests/` are test cases. Each of the `.v` files comes with a
matching `.ref` file containing the expected output of `coqc`. Adding `Show.`
in selected places in the proofs makes `coqc` print the current goal state.
This is used to make sure the proof mode prints goals and reduces terms the way
we expect it to. You can run `make MAKE_REF=1` to re-generate all the `.ref` files;
this is useful after adding or removing `Show.` from a test. If you do this,
make sure to check the diff for any unexpected changes in the output!
Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
Coq-8.8-specific `.ref` file). If you change one of these, remember to update
*all* the `.ref` files.
## How to measure the timing effect on a reverse dependency
So say you did a change in Iris, and want to know how it affects [lambda-rust]
or the [examples]. To do this, check out the respective project and change its
`.gitlab-ci.yml` to contain only one build job, which should look like
```
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0 coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
```
You will have to adjust this a bit: you should use the same Coq version as
whatever the master branch uses for its timing job, which you can determine by
checking its `.gitlab-ci.yml`. If you change the Coq version, remember to do it
in both places (`OPAM_PINS` and `TIMING_CONF`). You will also have to adjust
the Iris branch being used, which is determined after the `#` in `OPAM_PINS`.
If you are in doubt, ask on Mattermost *before* pushing your branch. Please
double-check that the job name is `build-iris.dev` to avoid polluting the caches
of regular CI builds! This way, you are going to share the cache with the
nightly builds, which is fine.
Once you are confident with your CI configuration, push this to a new branch
whose name starts with `ci/`. It should usually be of the form
`ci/yourname/feature`. You should see a pipeline running in GitLab with just a
single job, and you can follow its progress there.
When the job is done, you should be able to see it as a single dot on our
[statistics server][coq-speed] after selecting the right project and branch.
Click on "Coq-Speed" on the top-left corner to switch to another dashboard, and
select "Coq-Compare". Now you can select the project and the two measurements
you want to compare, which would be the SHA of the commit you just created as
"Commit 2", and the SHA of its parent as "Commit 1". Don't forget to also
select the right configuration for both of them. The "Grouping" is a regular
expression that you can use to switch between per-file, per-directory and
per-project grouping of the measurements.
If you changed your Iris branch and want to make another measurement, *do not*
just "Retry" the CI job. That will lead to an error, because you would end up
with two measurements for the same commit. Instead, create an empty commit in
your branch of the to-be-measured project (`git commit --allow-empty -m
"rerun"`), and push that.
[lambda-rust]: https://gitlab.mpi-sws.org/iris/lambda-rust
[examples]: https://gitlab.mpi-sws.org/iris/examples
[coq-speed]: https://coq-speed.mpi-sws.org
Here we collect some information on how to set up your editor to properly input
and output the unicode characters used throughout Iris.
## General: Unicode Fonts
Most editors will just use system fonts for rendering unicode characters and do
not need furhter 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...
("\\mult" ?⋅)
("\\ent" ?⊢)
("\\valid" ?✓)
("\\box" ?□)
("\\later" ?▷)
("\\pred" ?φ)
("\\and" ?∧)
("\\or" ?∨)
("\\comp" ?∘)
("\\ccomp" ?◎)
("\\all" ?∀)
("\\ex" ?∃)
("\\to" ?→)
("\\sep" ?∗)
("\\lc" ?⌜)
("\\rc" ?⌝)
("\\lam" ?λ)
("\\empty" ?∅)
("\\Lam" ?Λ)
("\\Sig" ?Σ)
("\\-" ?∖)
("\\aa" ?●)
("\\af" ?◯)
("\\iff" ?↔)
("\\gname" ?γ)
("\\incl" ?≼)
("\\latert" ?▶)
)
(mapc (lambda (x)
(if (cddr x)
(quail-defrule (cadr x) (car (cddr x)))))
(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"))
```
## CoqIDE
CoqIDE does not have support for unicode itself, but you can use the Intelligent
Input Bus (IBus) framework for multilingual input. 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:
```
;; Usage: copy to ~/.m17n.d/coq.mim
(input-method t coq)
(description "Input method for Coq")
(title "Coq")
(map (trans
;; Standard math notations
("\\forall" "∀")
("\\fun" "λ")
("\\exists" "∃")
("\\not" "¬")
("\\/" "∨")
("/\\" "∧")
("->" "→")
("<->" "↔")
("\\<-" "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
("\\==" "≡")
("\\/==" "≢")
("/=" "≠")
("<=" "≤")
("\\in" "∈")
("\\notin" "∉")
("\\cup" "∪")
("\\cap" "∩")
("\\setminus" "∖")
("\\subset" "⊂")
("\\subseteq" "⊆")
("\\sqsubseteq" "⊑")
("\\sqsubseteq" "⊑")
("\\notsubseteq" "⊈")
("\\empty" "∅")
("\\meet" "⊓")
("\\join" "⊔")
("\\top" "⊤")
("\\bottom" "⊥")
("\\vdash" "⊢")
("\\dashv" "⊣")
("\\Vdash" "⊨")
("\\infty" "∞")
("\\comp" "∘")
("\\prf" "↾")
("\\bind" "≫=")
("\\mapsto" "↦")
("\\hookrightarrow" "↪")
("\\uparrow" "↑")
;; Iris specific
("\\check" "✓")
("\\later" "▷")
("\\latert" "▶")
("\\diamond" "◇")
("\\square" "□")
("\\bsquare" "■")
("\\*" "∗")
("\\included" "≼")
("\\op" "⋅")
("\\update" "⇝")
("\\auth" "●")
("\\frag" "◯")
("\\lc" "⌜")
("\\rc" "⌝")
("\\Lc" "⎡")
("\\Rc" "⎤")
;; Commonly used sub- 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" ?ₓ)
;; Commonly used acents
("\\\"o" "ö")
;; 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)))
```
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".
# 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`, `CAS` (compare-and-swap) 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`](theories/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`: Perform one pure reduction step. Pure steps are defined by the
`PureExec` typeclass and include beta reduction, projections, constructors, as
well as unary and binary arithmetic operators.
- `wp_pures`: Perform as many pure reduction steps as possible. This
tactic will **not** reduce lambdas/recs that are hidden behind a definition.
- `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 away the `as "H"` to introduce it as an
anonymous assertion, i.e., that 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_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This
automatically finds the points-to assertion. It also automatically tries to
solve the (in)equality to show that the CAS succeeds/fails, and opens a new
goal if it cannot prove this goal.
- `wp_cas as H1 | H2`: Reduce a CAS, 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`: Apply a lemma whose conclusion is a `WP`, automatically
applying `wp_bind` as needed. See the [ProofMode docs](ProofMode.md) for an
explanation of `pm_trm`.
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 defineable in
HeapLang, but that requires thunking `e1` and `e2` before passing them to
`par`. (This is defined in [`par.v`](theories/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 but 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
# Determine Coq version
COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
COQ_MAKEFILE_FLAGS ?=
ifeq ($(COQ_VERSION), 8.6)
COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection
endif
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
.PHONY: all
clean: Makefile.coq
+@make -f Makefile.coq clean
find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
@# we want to pass the correct name to coq_makefile or it will be confused
coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp
sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' < Makefile.coq.tmp \
| awk '/^uninstall:/{print "uninstall:";print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ -name \"*.vo\" -print -delete; fi";getline;next}1' > Makefile.coq
rm Makefile.coq.tmp
_CoqProject: ;
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: all clean phony
.PHONY: phony
# Run tests interleaved with main build. They have to be in the same target for this.
real-all: $(if $(NO_TEST),,test)
# the test suite
TESTFILES=$(wildcard tests/*.v)
NORMALIZER=test-normalizer.sed
test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES'
$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
-include tests/.coqdeps.d
# Main test script (comments out-of-line because macOS otherwise barfs?!?)
# - Determine reference file (`REF`).
# - Print user-visible status line.
# - Dump Coq output into a temporary file.
# - Run `sed -i` on that file in a way that works on macOS.
# - Either compare the result with the reference file, or move it over the reference file.
# - Cleanup, and mark as done for make.
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
$(HIDE)TEST="$$(basename -s .v $<)" && \
if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
else \
REF="tests/$$TEST.ref"; \
fi && \
echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
mv "$$TMPFILE".new "$$TMPFILE" && \
$(if $(COQ_OLD),true, \
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
) && \
rm -f "$$TMPFILE" && \
touch $@
This diff is collapsed.
This diff is collapsed.
# IRIS COQ DEVELOPMENT
# IRIS COQ DEVELOPMENT [[coqdoc]](https://plv.mpi-sws.org/coqdoc/iris/)
This is the Coq development of the [Iris Project](http://iris-project.org).
This is the Coq development of the [Iris Project](http://iris-project.org),
which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
for carrying out separation logic proofs in Coq.
## Prerequisites
For using the Coq library, check out the
[API documentation](https://plv.mpi-sws.org/coqdoc/iris/).
For understanding the theory of Iris, a LaTeX version of the core logic
definitions and some derived forms is available in
[docs/iris.tex](docs/iris.tex). A compiled PDF version of this document is
[available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
## Building Iris
### Prerequisites
This version is known to compile with:
- Coq 8.5pl2
- [Ssreflect 1.6](https://github.com/math-comp/math-comp/releases/tag/mathcomp-1.6)
- Coq 8.7.2 / 8.8.2 / 8.9.0 / 8.9.1
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
For a version compatible with Coq 8.6, have a look at the
[iris-3.1 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.1).
If you need to work with Coq 8.5, please check out the
[iris-3.0 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.0).
### Working *with* Iris
To use Iris in your own proofs, we recommend you install Iris via opam (1.2.2 or
newer). To obtain the latest stable release, you have to add the Coq opam
repository:
opam repo add coq-released https://coq.inria.fr/opam/released
To obtain a development version, also add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Either way, you can now do `opam install coq-iris`. To fetch updates later, run
`opam update && opam upgrade`. However, notice that we do not guarnatee
backwards-compatibility, so upgrading Iris may break your Iris-using
developments.
For development, better make sure you have a version of Ssreflect that includes
commit ad273277 (no such version has been released so far, you will have to
fetch the development branch yourself). Iris compiles fine even without this
patch, but proof bullets will only be in 'strict' (enforcing) mode with the
fixed version of Ssreflect. If you are using opam, you can easily get a fixed
version by running
### Working *on* Iris
opam pin add coq-mathcomp-ssreflect https://github.com/math-comp/math-comp.git#ad273277ab38bfe458e9332dea5f3a79e3885567
## Building Instructions
To work on Iris itself, you need to install its build-dependencies. Again we
recommend you do that with opam (1.2.2 or newer). This requires the following
two repositories:
Run the following command to build the full development:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
The development can then be installed as the Coq user contribution `iris` by
running:
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
make install
To update Iris, do `git pull`. After an update, the development may fail to
compile because of outdated dependencies. To fix that, please run `opam update`
followed by `make build-dep`.
## Structure
## Directory Structure
* The folder [prelude](prelude) contains an extended "Standard Library" by
[Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
* The folder [algebra](algebra) contains the COFE and CMRA constructions as well
as the solver for recursive domain equations.
* The folder [base_logic](base_logic) defines the Iris base logic and the
primitive connectives. It also contains derived constructions that are
* The folder [algebra](theories/algebra) contains the COFE and CMRA
constructions as well as the solver for recursive domain equations.
* The folder [base_logic](theories/base_logic) defines the Iris base logic and
the primitive connectives. It also contains derived constructions that are
entirely independent of the choice of resources.
* The subfolder [lib](base_logic/lib) contains some generally useful
* The subfolder [lib](theories/base_logic/lib) contains some generally useful
derived constructions. Most importantly, it defines composeable
dynamic resources and ownership of them; the other constructions depend
on this setup.
* The folder [program_logic](program_logic) specializes the base logic to build
Iris, the program logic. This includes weakest preconditions that are
defined for any language satisfying some generic axioms, and some derived
* The folder [program_logic](theories/program_logic) specializes the base logic
to build Iris, the program logic. This includes weakest preconditions that
are defined for any language satisfying some generic axioms, and some derived
constructions that work for any such language.
* The folder [proofmode](proofmode) contains the Iris proof mode, which extends
Coq with contexts for persistent and spatial Iris assertions. It also contains
tactics for interactive proofs in Iris. Documentation can be found in
* The folder [bi](theories/bi) contains the BI++ laws, as well as derived
connectives, laws and constructions that are applicable for general BIS.
* The folder [proofmode](theories/proofmode) contains
[MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
intuitionistic and spatial BI++ assertions. It also contains tactics for
interactive proofs. Documentation can be found in
[ProofMode.md](ProofMode.md).
* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
* The subfolder [lib](heap_lang/lib) contains a few derived constructions
within this language, e.g., parallel composition.
Most notable here is [lib/barrier](heap_lang/lib/barrier), the implementation
and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
* The folder [tests](tests) contains modules we use to test our infrastructure.
Users of the Iris Coq library should *not* depend on these modules; they may
change or disappear without any notice.
## Documentation
A LaTeX version of the core logic definitions and some derived forms is
available in [docs/iris.tex](docs/iris.tex). A compiled PDF version of this
document is [available online](http://plv.mpi-sws.org/iris/appendix-3.0.pdf).
* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
language
* The subfolder [lib](theories/heap_lang/lib) contains a few derived
constructions within this language, e.g., parallel composition.
For more examples of using Iris and heap_lang, have a look at the
[Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
* The folder [tests](theories/tests) contains modules we use to test our
infrastructure. Users of the Iris Coq library should *not* depend on these
modules; they may change or disappear without any notice.
## Case Studies
The following is a (probably incomplete) list of case studies that use Iris, and
that should be compatible with this version:
* [Iris Examples](https://gitlab.mpi-sws.org/iris/examples) is where we
collect miscellaneous case studies that do not have their own repository.
* [LambdaRust](https://gitlab.mpi-sws.org/iris/lambda-rust) is a Coq
formalization of the core Rust type system.
* [GPFSL](https://gitlab.mpi-sws.org/iris/gpfsl) is a logic for release-acquire
and relaxed memory.
* [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic
built on top of Iris for precise reasoning about resources (such as making
sure there are no memory leaks).
## Further Resources
Getting along with Iris in Coq:
* Iris proof patterns are documented in the [proof guide](ProofGuide.md).
* Syntactic conventions are described in the [style guide](StyleGuide.md).
* The Iris tactics are described in the
[the Iris Proof Mode (IPM) / MoSeL documentation](ProofMode.md) as well as the
[HeapLang documentation](HeapLang.md).
* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
Contacting the developers:
* Discussion about the Iris Coq development happens on the mailing list
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
and in the [Iris Chat](https://mattermost.mpi-sws.org/iris). This is also the
right place to ask questions. The chat requires an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
tab). If you have trouble joining the chat, please contact
[Ralf](https://gitlab.mpi-sws.org/jung).
* If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which also
requires an MPI-SWS GitLab account.
* To contribute to Iris itself, see the [contribution guide](CONTRIBUTING.md).
Miscellaneous:
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
* If you are writing a paper that uses Iris in one way or another, you could use
the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
connectives.
# Iris Style Guide
This document lays down syntactic conventions about how we usually write our
Iris proofs in Coq. It is a work-in-progress. This complements the tactic
documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as
well as the [proof guide](ProofGuide.md).
## Implicit generalization
We often use the implicit generalization feature of Coq, triggered by a backtic:
`` `{!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](theories/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):
```
Typeclasses Opaque join_handle.
```
This makes sure that the proof mode does not "look into" your definition when it
is used by clients.
## Naming conventions for variables/arguments/hypotheses
### small letters
* a : A = cmraT or ofeT
* b : B = cmraT or ofeT
* c
* d
* e : expr = expressions
* f = some generic function
* g = some generic function
* h : heap
* i
* j
* k
* l
* m : iGst = ghost state
* m* = prefix for option
* n
* o
* p
* q
* r : iRes = resources
* s = state (STSs)
* s = stuckness bits
* t
* u
* v : val = values of language
* w
* x
* y
* z
### capital letters
* A : Type, cmraT or ofeT
* B : Type, cmraT or ofeT
* C
* D
* E : coPset = Viewshift masks
* 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 : abstraction of value type in frame shift assertions
* W
* X : sets
* Y : sets
* Z : sets
### small greek letters
* γ : gname
* σ : state = state of language
* φ : interpretation of STS/Auth
### capital greek letters
* Φ : general predicate (over uPred, iProp or Prop)
* Ψ : general predicate (over 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 `ProofGuide.md`)
* I: bunched implication logic (of type `bi`)
* SI: step-indexed bunched implication logic (of type `sbi`)
* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
* Σ: global camera functor management (`gFunctors`; see `ProofGuide.md`)
-Q . iris
prelude/option.v
prelude/fin_map_dom.v
prelude/bset.v
prelude/fin_maps.v
prelude/vector.v
prelude/pmap.v
prelude/stringmap.v
prelude/fin_collections.v
prelude/mapset.v
prelude/proof_irrel.v
prelude/hashset.v
prelude/pretty.v
prelude/countable.v
prelude/orders.v
prelude/natmap.v
prelude/strings.v
prelude/relations.v
prelude/collections.v
prelude/listset.v
prelude/streams.v
prelude/gmap.v
prelude/gmultiset.v
prelude/base.v
prelude/tactics.v
prelude/prelude.v
prelude/listset_nodup.v
prelude/finite.v
prelude/numbers.v
prelude/nmap.v
prelude/zmap.v
prelude/coPset.v
prelude/lexico.v
prelude/set.v
prelude/decidable.v
prelude/list.v
prelude/functions.v
prelude/hlist.v
prelude/sorting.v
algebra/cmra.v
algebra/cmra_big_op.v
algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/gmap.v
algebra/ofe.v
algebra/base.v
algebra/dra.v
algebra/cofe_solver.v
algebra/agree.v
algebra/dec_agree.v
algebra/excl.v
algebra/iprod.v
algebra/frac.v
algebra/csum.v
algebra/list.v
algebra/updates.v
algebra/local_updates.v
algebra/gset.v
algebra/coPset.v
algebra/deprecated.v
base_logic/upred.v
base_logic/primitive.v
base_logic/derived.v
base_logic/base_logic.v
base_logic/tactics.v
base_logic/big_op.v
base_logic/hlist.v
base_logic/soundness.v
base_logic/double_negation.v
base_logic/deprecated.v
base_logic/lib/iprop.v
base_logic/lib/own.v
base_logic/lib/saved_prop.v
base_logic/lib/namespaces.v
base_logic/lib/wsat.v
base_logic/lib/invariants.v
base_logic/lib/fancy_updates.v
base_logic/lib/viewshifts.v
base_logic/lib/auth.v
base_logic/lib/sts.v
base_logic/lib/boxes.v
base_logic/lib/na_invariants.v
base_logic/lib/cancelable_invariants.v
base_logic/lib/counter_examples.v
base_logic/lib/fractional.v
program_logic/adequacy.v
program_logic/lifting.v
program_logic/weakestpre.v
program_logic/hoare.v
program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
heap_lang/lifting.v
heap_lang/derived.v
heap_lang/notation.v
heap_lang/heap.v
heap_lang/lib/spawn.v
heap_lang/lib/par.v
heap_lang/lib/assert.v
heap_lang/lib/lock.v
heap_lang/lib/spin_lock.v
heap_lang/lib/ticket_lock.v
heap_lang/lib/counter.v
heap_lang/lib/barrier/barrier.v
heap_lang/lib/barrier/specification.v
heap_lang/lib/barrier/protocol.v
heap_lang/lib/barrier/proof.v
heap_lang/proofmode.v
heap_lang/adequacy.v
tests/heap_lang.v
tests/one_shot.v
tests/joining_existentials.v
tests/proofmode.v
tests/barrier_client.v
tests/list_reverse.v
tests/tree_sum.v
tests/counter.v
proofmode/strings.v
proofmode/coq_tactics.v
proofmode/environments.v
proofmode/intro_patterns.v
proofmode/spec_patterns.v
proofmode/sel_patterns.v
proofmode/tactics.v
proofmode/notation.v
proofmode/classes.v
proofmode/class_instances.v
-Q theories iris
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
# is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
theories/algebra/monoid.v
theories/algebra/cmra.v
theories/algebra/big_op.v
theories/algebra/cmra_big_op.v
theories/algebra/sts.v
theories/algebra/auth.v
theories/algebra/frac_auth.v
theories/algebra/gmap.v
theories/algebra/ofe.v
theories/algebra/base.v
theories/algebra/dra.v
theories/algebra/cofe_solver.v
theories/algebra/agree.v
theories/algebra/excl.v
theories/algebra/functions.v
theories/algebra/frac.v
theories/algebra/csum.v
theories/algebra/list.v
theories/algebra/vector.v
theories/algebra/updates.v
theories/algebra/local_updates.v
theories/algebra/gset.v
theories/algebra/gmultiset.v
theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v
theories/algebra/namespace_map.v
theories/algebra/ufrac_auth.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
theories/bi/derived_laws_bi.v
theories/bi/derived_laws_sbi.v
theories/bi/plainly.v
theories/bi/big_op.v
theories/bi/updates.v
theories/bi/bi.v
theories/bi/tactics.v
theories/bi/monpred.v
theories/bi/embedding.v
theories/bi/weakestpre.v
theories/bi/telescopes.v
theories/bi/lib/counterexamples.v
theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v
theories/bi/lib/laterable.v
theories/bi/lib/atomic.v
theories/bi/lib/core.v
theories/base_logic/upred.v
theories/base_logic/bi.v
theories/base_logic/derived.v
theories/base_logic/proofmode.v
theories/base_logic/base_logic.v
theories/base_logic/bupd_alt.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v
theories/base_logic/lib/wsat.v
theories/base_logic/lib/invariants.v
theories/base_logic/lib/fancy_updates.v
theories/base_logic/lib/viewshifts.v
theories/base_logic/lib/auth.v
theories/base_logic/lib/sts.v
theories/base_logic/lib/boxes.v
theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/fancy_updates_from_vs.v
theories/base_logic/lib/proph_map.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
theories/program_logic/total_weakestpre.v
theories/program_logic/total_adequacy.v
theories/program_logic/hoare.v
theories/program_logic/language.v
theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v
theories/program_logic/ownp.v
theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
theories/heap_lang/locations.v
theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/array.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
theories/heap_lang/lib/lock.v
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/nondet_bool.v
theories/heap_lang/lib/lazy_coin.v
theories/heap_lang/lib/clairvoyant_coin.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/diverge.v
theories/heap_lang/lib/arith.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
theories/proofmode/ltac_tactics.v
theories/proofmode/environments.v
theories/proofmode/reduction.v
theories/proofmode/intro_patterns.v
theories/proofmode/spec_patterns.v
theories/proofmode/sel_patterns.v
theories/proofmode/tactics.v
theories/proofmode/notation.v
theories/proofmode/classes.v
theories/proofmode/class_instances_bi.v
theories/proofmode/class_instances_sbi.v
theories/proofmode/frame_instances.v
theories/proofmode/monpred.v
theories/proofmode/modalities.v
theories/proofmode/modality_instances.v
This diff is collapsed.
This diff is collapsed.
From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
This diff is collapsed.
From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
Context {A : ucmraT}.
Inductive expr :=
| EVar : nat expr
| EEmpty : expr
| EOp : expr expr expr.
Fixpoint eval (Σ : list A) (e : expr) : A :=
match e with
| EVar n => from_option id (Σ !! n)
| EEmpty =>
| EOp e1 e2 => eval Σ e1 eval Σ e2
end.
Fixpoint flatten (e : expr) : list nat :=
match e with
| EVar n => [n]
| EEmpty => []
| EOp e1 e2 => flatten e1 ++ flatten e2
end.
Lemma eval_flatten Σ e :
eval Σ e big_op ((λ n, from_option id (Σ !! n)) <$> flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
by rewrite fmap_app IH1 IH2 big_op_app.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 eval Σ e1 eval Σ e2.
Proof.
by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
Qed.
Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
Global Instance quote_empty: Quote E1 E1 EEmpty.
Global Instance quote_var Σ1 Σ2 e i:
rlist.QuoteLookup Σ1 Σ2 e i Quote Σ1 Σ2 e (EVar i) | 1000.
Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
Quote Σ1 Σ2 x1 e1 Quote Σ2 Σ3 x2 e2 Quote Σ1 Σ3 (x1 x2) (EOp e1 e2).
End ra_reflection.
Ltac quote :=
match goal with
| |- @included _ _ _ ?x ?y =>
lazymatch type