Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Show changes
......@@ -5,16 +5,30 @@ 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: "Iris is a Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
description: """
This package provides the following Coq modules:
iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
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.11" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-12-10.0.e41e169f") | (= "dev") }
"coq" { (>= "8.19" & < "9.1~") | (= "dev") }
"coq-stdpp" { (= "dev.2025-02-26.0.d2e8771d") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
......
#!/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
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`.
......@@ -5,7 +5,7 @@ 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](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/ascii.v).
[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,
......@@ -96,12 +96,12 @@ on the math symbol list, and with some custom aliases for symbols used a lot in
(mapc (lambda (x)
(if (cddr x)
(quail-defrule (cadr x) (car (cddr x)))))
(append math-symbol-list-basic math-symbol-list-extended))
; 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)))
```
Finally, set your default input method with `M-x customize-set-value`, setting
`default-input-method` to `math`.
### Font Configuration
Even when usable fonts are installed, Emacs tends to pick bad fonts for some
......@@ -125,140 +125,65 @@ results in a decent choice for the symbols used in Iris:
(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:
```
;; 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)))
```
aliases for symbols used a lot in Iris as defined [here](ibus).
To use this input method, you should:
......@@ -364,7 +289,7 @@ Here is a `coqide.bindings` file for a variety of symbols used in Iris:
### VSCoq setup
The recommended extension as of December 2019 is [Maxime Dénès's
VScoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
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.
......@@ -373,7 +298,7 @@ commands and keyboard shortcuts.
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" as the font-family and optionally enable
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
......@@ -382,186 +307,86 @@ 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 ,`, and type "generic-input-methods.input-methods", then
click on "Edit in settings.json" and add the following:
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`:
```
"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": "ω" }
]
}
]
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.
# Equalities in Iris
Using Iris involves dealing with a few subtly different equivalence and equality
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
......@@ -8,7 +8,7 @@ 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 (`≡`);
- N-equivalence on OFEs (`≡{n}≡`);
- Iris `n`-equivalence on OFEs (`≡{n}≡`);
- Iris internal equality (`≡` in `bi_scope`);
- Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
......@@ -45,6 +45,52 @@ Here, stdpp adds the following facilities:
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,
......
......@@ -33,7 +33,7 @@ constructor).
## Notation
Notation for writing HeapLang terms is defined in
[`notation.v`](../theories/heap_lang/notation.v). There are two scopes, `%E` for
[`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.
......@@ -55,9 +55,12 @@ that the current goal is of the shape `WP e @ E {{ Q }}`.
Tactics to take one or more pure program steps:
- `wp_pure`: Perform one pure reduction step. Pure steps are defined by the
`PureExec` typeclass and include beta reduction, projections, constructors, as
well as unary and binary arithmetic operators.
- `wp_pure pat credit:"H"`: Perform one pure reduction step. `pat` optionally
defines the pattern that the redex has to match; it defaults to `_` (any
redex). The `credit:` argument is optional, too; when present, a later credit
will be generated in a fresh hypothesis named `"H"`.
Pure steps are defined by the `PureExec` typeclass and include beta reduction,
projections, constructors, as well as unary and binary arithmetic operators.
- `wp_pures`: Perform as many pure reduction steps as possible. This
tactic will **not** reduce lambdas/recs that are hidden behind a definition.
If the computation reaches a value, the `WP` will be entirely removed and the
......@@ -101,9 +104,16 @@ Further tactics:
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](./proof_mode.md) for an
explanation of `pm_trm`.
- `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`.
......@@ -118,7 +128,7 @@ all of the redexes reduced.)
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`](theories/heap_lang/lib/par.v).) However,
`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.
......
;; 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)))
......@@ -23,6 +23,37 @@ recommend importing in the following order:
- 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
......@@ -50,7 +81,7 @@ 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
(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
......@@ -68,7 +99,7 @@ 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) := {
sts_inG :> inG Σ (stsR sts);
#[local] sts_inG :: inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
```
......@@ -107,8 +138,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
### small letters
* a : A = cmraT or ofeT
* b : B = cmraT or ofeT
* a : A = cmra or ofe
* b : B = cmra or ofe
* c
* d
* e : expr = expressions
......@@ -137,8 +168,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
### capital letters
* A : Type, cmraT or ofeT
* B : Type, cmraT or ofeT
* A : Type, cmra or ofe
* B : Type, cmra or ofe
* C
* D
* E : coPset = mask of fancy update or WP
......@@ -185,7 +216,9 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
* 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 ofeT for OFEs, cmraT for cameras)
* 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))
......@@ -21,7 +21,7 @@ pervasively. These are defined in dedicated sections in this manual.
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
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.
......@@ -55,7 +55,7 @@ Applying hypotheses and lemmas
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
pattern is extended with `[] ... []`. As a consequence, all unused spatial
hypotheses move to the last premise.
Context management
......@@ -66,11 +66,18 @@ Context management
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
......@@ -81,19 +88,23 @@ Context management
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 with "spat" as "H"` : generate a new subgoal `P` and add the
- `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 with "spat" as "ipat"` : like the above, but immediately destruct
+ `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 as %cpat` : assert `P` and destruct it using the Coq introduction
+ `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
-----------------------------------
......@@ -115,7 +126,7 @@ Introduction of logical connectives
- `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).
- `iExist t1, .., tn` : provide a witness for an existential quantifier `∃ x, ...`. `t1
- `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.)
......@@ -138,7 +149,7 @@ Elimination of logical connectives
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
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,
......@@ -146,13 +157,16 @@ Elimination of logical connectives
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) or with an `%` (which causes the
hypothesis to be moved to the pure Coq context), 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.
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
---------------------------------
......@@ -167,12 +181,21 @@ Separation logic-specific tactics
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
hypthesis using `ipat`. Some examples of simplifications `iCombine` knows
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`.
- `iAccu` : solves a goal that is an evar by instantiating it with all
- `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.
......@@ -217,13 +240,26 @@ Induction
+ `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 "IH" "selpat"` : perform induction on
the Coq term `x`. The Coq introduction pattern `cpat` is used to name the introduced
variables. The induction hypotheses are inserted into the intuitionistic
context and given fresh names prefixed `IH`.
+ `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction,
- `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
--------------------------
......@@ -232,7 +268,7 @@ Rewriting / simplification
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"` : performs a tactic `tac`
- `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
......@@ -242,9 +278,13 @@ Rewriting / simplification
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"` : performs `simpl` on the proof mode
- `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
----
......@@ -299,7 +339,7 @@ Introduction patterns (`ipat`)
==============================
Introduction patterns are used to perform introductions and eliminations of
multiple connectives on the fly. The proof mode supports the following
multiple connectives on the fly. The proof mode supports the following
_introduction patterns_:
- `H` : create a hypothesis named `H`.
......@@ -312,16 +352,15 @@ _introduction patterns_:
+ 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`. Support
for the `%H` introduction pattern requires an implementation of the hook
`string_to_ident`. Without an implementation of this hook, the `%H` pattern
will fail. We provide an implementation of the hook using Ltac2, which works
with Coq 8.11 and later, and can be installed with opam; see
[iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
- `%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.
......@@ -340,7 +379,7 @@ _introduction patterns_:
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 hypotheses when it is timeless and the goal is either a `WP`
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
......@@ -419,7 +458,7 @@ _specialization patterns_ to express splitting of hypotheses:
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 hypothesis that are not framed are carried over to the
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
......
......@@ -7,18 +7,27 @@ 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 ∈ Σ`.
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 }.
Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
Local Existing Instances one_shot_inG.
```
The `:>` means that the projection `one_shot_inG` is automatically 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 Σ`.
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
......@@ -50,12 +59,12 @@ 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 `{!heapG Σ, !one_shotG Σ}.
Context `{!heapGS Σ, !one_shotG Σ}.
```
Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
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, `heapG` contains not only assumptions
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).
......@@ -90,10 +99,10 @@ 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):
adequacy lemma. [For example](../tests/one_shot.v):
```coq
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
(* ... *)
......@@ -112,49 +121,51 @@ Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
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 it is added to
`gen_heapG`, the type class for the generalized heap module:
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_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_heap_name : gname
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
#[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
}.
```
Such modules always need some kind of "initialization" to create an instance
of their type class. For example, the initialization for `heapG` is happening
as part of [`heap_adequacy`](iris_heap_lang/adequacy.v); this in turn uses
the initialization lemma for `gen_heapG` from
[`gen_heap_init`](iris/base_logic/lib/gen_heap.v):
```coq
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
(|==> _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
#[local] gen_heap_inG :: gen_heapGpreS L V Σ;
gen_heap_name : gname;
}.
```
These lemmas themselves only make assumptions the way normal modules (those
without global state) do, which are typically collected in a `somethingPreG`
type class (such as `gen_heapPreG`):
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
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
}.
Lemma gen_heap_init `{gen_heapGpreS L V Σ} σ :
(|==> _ : gen_heapGS L V Σ, gen_heap_ctx σ)%I.
```
Just like in the normal case, `somethingPreG` type classes have an `Instance`
showing that a `subG` is enough to instantiate them:
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
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
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 `somethingPreG` type class is
enough to create an instance of the main `somethingG` class *below a view
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_heapG` in the context.
an instance of `gen_heapGS` in the context.
Given that these global ghost state instances are singletons, they must be
assumed explicitly everywhere. Bundling `heapG` in a module type class like
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
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
......@@ -220,23 +231,23 @@ 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:
- [`cFunctor`](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
- [`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 `cFunctorContractive`, `rFunctorContractive`, and
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 : ofeT) : cFunctor := λ (B,B⁻), A `
- `idOF : cFunctor := λ (B,B⁻), B`
- `prodOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
- `ofe_morOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
- `laterOF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻))`
- `agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻))`
- `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
......@@ -247,7 +258,7 @@ Using these combinators, one can easily construct bigger functors in point-free
style and automatically infer their contractivity, e.g:
```coq
F := gmaURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
F := gmapURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
```
which effectively defines the desired example functor
......@@ -271,7 +282,9 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
your example would look as follows:
```coq
Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
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.
......
# 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)
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
"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": "ω" }
]
}
]
(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
)))))
(lang dune 3.8)
(using coq 0.8)
#!/usr/bin/python3
import sys, os, subprocess
import requests, argparse
from datetime import datetime, timezone
from collections import namedtuple
################################################################################
# This script lets you autoamtically trigger some operations on the Iris CI to
# do further test/analysis on a branch (usually an MR).
# Set the GITLAB_TOKEN environment variable to a GitLab access token.
# You can generate such a token at
# <https://gitlab.mpi-sws.org/-/user_settings/personal_access_tokens>.
# Select only the "api" scope.
#
# Set at least one of IRIS_REV or STDPP_REV to control which branches of these
# projects to build against (defaults to default git branch). IRIS_REPO and
# STDPP_REPO can be used to take branches from forks. Setting IRIS to
# "user:branch" will use the given branch on that user's fork of Iris, and
# similar for STDPP.
#
# Supported commands:
# - `./iris-bot build [$filter]`: Builds all reverse dependencies against the
# given branches. The optional `filter` argument only builds projects whose
# names contains that string.
# - `./iris-bot time $project`: Measure the impact of this branch on the build
# time of the given reverse dependency. Only Iris branches are supported for
# now.
################################################################################
PROJECTS = {
'lambda-rust': { 'name': 'lambda-rust', 'branch': 'master', 'timing': True },
'lambda-rust-weak': { 'name': 'lambda-rust', 'branch': 'masters/weak_mem' }, # covers GPFSL and ORC11
'examples': { 'name': 'examples', 'branch': 'master', 'timing': True },
'gpfsl': { 'name': 'gpfsl', 'branch': 'master', 'timing': True }, # need separate entry for timing
'iron': { 'name': 'iron', 'branch': 'master', 'timing': True },
'reloc': { 'name': 'reloc', 'branch': 'master' },
'actris': { 'name': 'actris', 'branch': 'master' },
'simuliris': { 'name': 'simuliris', 'branch': 'master' },
'tutorial-popl20': { 'name': 'tutorial-popl20', 'branch': 'master' },
'tutorial-popl21': { 'name': 'tutorial-popl21', 'branch': 'master' },
}
if not "GITLAB_TOKEN" in os.environ:
print("You need to set the GITLAB_TOKEN environment variable to a GitLab access token.")
print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
print("Make sure you grant access to the 'api' scope.")
sys.exit(1)
GITLAB_TOKEN = os.environ["GITLAB_TOKEN"]
# Pre-processing for branch variables of dependency projects: you can set
# 'PROJECT' to 'user:branch', or set 'PROJECT_REPO' and 'PROJECT_REV'
# automatically.
BUILD_BRANCHES = {}
for project in ['stdpp', 'iris', 'orc11', 'gpfsl']:
var = project.upper()
if var in os.environ:
(repo, rev) = os.environ[var].split(':')
repo = repo + "/" + project
else:
repo = os.environ.get(var+"_REPO", "iris/"+project)
rev = os.environ.get(var+"_REV")
if rev is not None:
BUILD_BRANCHES[project] = (repo, rev)
if not "iris" in BUILD_BRANCHES:
print("Please set IRIS_REV, STDPP_REV, ORC11_REV and GPFSL_REV environment variables to the branch/tag/commit of the respective project that you want to use.")
print("Only IRIS_REV is mandatory, the rest defaults to the default git branch.")
sys.exit(1)
# Useful helpers
def trigger_build(project, branch, vars):
id = "iris%2F{}".format(project)
url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
json = {
'ref': branch,
'variables': [{ 'key': key, 'value': val } for (key, val) in vars.items()],
}
r = requests.post(url, headers={'PRIVATE-TOKEN': GITLAB_TOKEN}, json=json)
r.raise_for_status()
return r.json()
# The commands
def build(args):
# Convert BUILD_BRANCHES into suitable dictionary
vars = {}
for project in BUILD_BRANCHES.keys():
(repo, rev) = BUILD_BRANCHES[project]
var = project.upper()
vars[var+"_REPO"] = repo
vars[var+"_REV"] = rev
if args.coq:
vars["NIGHTLY_COQ"] = args.coq
# Loop over all projects, and trigger build.
for (name, project) in PROJECTS.items():
if args.filter in name:
print("Triggering build for {}...".format(name))
pipeline_url = trigger_build(project['name'], project['branch'], vars)['web_url']
print(" Pipeline running at {}".format(pipeline_url))
TimeJob = namedtuple("TimeJob", "id base_commit base_pipeline test_commit test_pipeline compare")
def time_project(project, iris_repo, iris_rev, test_rev):
# Obtain a unique ID for this experiment
id = datetime.now(timezone.utc).strftime("%Y%m%d-%H%M%S")
# Determine the branch commit to build
subprocess.run(["git", "fetch", "-q", "https://gitlab.mpi-sws.org/{}".format(iris_repo), iris_rev], check=True)
test_commit = subprocess.run(["git", "rev-parse", "FETCH_HEAD"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
# Determine the base commit in master
subprocess.run(["git", "fetch", "-q", "https://gitlab.mpi-sws.org/iris/iris.git", "master"], check=True)
base_commit = subprocess.run(["git", "merge-base", test_commit, "FETCH_HEAD"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
# Trigger the builds
vars = {
'IRIS_REPO': iris_repo,
'IRIS_REV': base_commit,
'TIMING_AD_HOC_ID': id+"-base",
}
base_pipeline = trigger_build(project['name'], project['branch'], vars)
vars = {
'IRIS_REPO': iris_repo,
'IRIS_REV': test_commit,
'TIMING_AD_HOC_ID': id+"-test",
}
if test_rev is None:
# We hope that this repository did not change since the job we created just above...
test_pipeline = trigger_build(project['name'], project['branch'], vars)
else:
test_pipeline = trigger_build(project['name'], args.test_rev, vars)
compare = "https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project={}&var-branch1=@hoc&var-commit1={}&var-config1={}&var-branch2=@hoc&var-commit2={}&var-config2={}".format(project['name'], base_pipeline['sha'], id+"-base", test_pipeline['sha'], id+"-test")
return TimeJob(id, base_commit, base_pipeline['web_url'], test_commit, test_pipeline['web_url'], compare)
def time(args):
# Make sure only 'iris' variables are set.
# One could imagine generalizing to "either Iris or std++", but then if the
# ad-hoc timing jobs honor STDPP_REV, how do we make it so that particular
# deterministic std++ versions are used for Iris timing? This does not
# currently seem worth the effort / hacks.
for project in BUILD_BRANCHES.keys():
if project != 'iris':
print("'time' command only supports Iris branches")
sys.exit(1)
(iris_repo, iris_rev) = BUILD_BRANCHES['iris']
# Special mode: time everything
if args.project == 'all':
if args.test_rev is not None:
print("'time all' does not support '--test-rev'")
sys.exit(1)
for (name, project) in PROJECTS.items():
if not project.get('timing'):
continue
job = time_project(project, iris_repo, iris_rev, None)
print("- [{}]({})".format(name, job.compare))
return
# Get project to test and ensure it supports timing
project_name = args.project
if project_name not in PROJECTS:
print("ERROR: no such project: {}".format(project_name))
sys.exit(1)
project = PROJECTS[project_name]
if not project.get('timing'):
print("ERROR: {} does not support timing".format(project_name))
sys.exit(1)
# Run it!
job = time_project(project, iris_repo, iris_rev, args.test_rev)
print("Triggering timing builds for {} with Iris base commit {} and test commit {} using ad-hoc ID {}...".format(project_name, job.base_commit[:8], job.test_commit[:8], job.id))
print(" Base pipeline running at {}".format(job.base_pipeline))
if args.test_rev is None:
print(" Test pipeline running at {}".format(job.test_pipeline))
else:
print(" Test pipeline (on non-standard branch {}) running at {}".format(args.test_rev, job.test_pipeline))
print(" Once done, timing comparison will be available at {}".format(job.compare))
# Dispatch
if __name__ == "__main__":
parser = argparse.ArgumentParser(description='Iris CI utility')
subparsers = parser.add_subparsers(required=True, title='iris-bot command to execute', description='see "$command -h" for help', metavar="$command")
parser_build = subparsers.add_parser('build', help='Build many reverse dependencies against an Iris branch')
parser_build.set_defaults(func=build)
parser_build.add_argument('--coq', help='the (opam) Coq version to use for these tests')
parser_build.add_argument('filter', nargs='?', default='', help='(optional) restrict build to projects matching the filter')
parser_time = subparsers.add_parser('time', help='Time one reverse dependency against an Iris branch')
parser_time.add_argument("project", help="the project to measure the time of, or 'all' to measure all of them")
parser_time.add_argument("--test-rev", help="use different revision on project for the test build (in case the project requires changes to still build)")
parser_time.set_defaults(func=time)
# Parse, and dispatch to sub-command
args = parser.parse_args()
args.func(args)
From iris.algebra Require Export cmra.
From iris.prelude Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments validN _ _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
......@@ -34,8 +34,8 @@ Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
Arguments agree_car {_} _.
Arguments agree_not_nil {_} _.
Global Arguments agree_car {_} _.
Global Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Definition to_agree {A} (a : A) : agree A :=
......@@ -50,15 +50,15 @@ Proof.
Qed.
Section agree.
Context {A : ofeT}.
Context {SI : sidx} {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
(* OFE *)
Instance agree_dist : Dist (agree A) := λ n x y,
Local Instance agree_dist : Dist (agree A) := λ n x y,
( a, a agree_car x b, b agree_car y a {n} b)
( b, b agree_car y a, a agree_car x a {n} b).
Instance agree_equiv : Equiv (agree A) := λ x y, n, x {n} y.
Local Instance agree_equiv : Equiv (agree A) := λ x y, n, x {n} y.
Definition agree_ofe_mixin : OfeMixin (agree A).
Proof.
......@@ -72,62 +72,70 @@ Proof.
destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
* intros a ?. destruct (H2' a) as (b&?&?); auto.
destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
- intros n x y [??]; split; naive_solver eauto using dist_S.
- intros n m x y [??]; split; naive_solver eauto using dist_le.
Qed.
Canonical Structure agreeO := OfeT (agree A) agree_ofe_mixin.
Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
is convertible to True. This makes working with agreement much more pleasant. *)
Instance agree_validN : ValidN (agree A) := λ n x,
Local Instance agree_validN_instance : ValidN (agree A) := λ n x,
match agree_car x with
| [a] => True
| _ => a b, a agree_car x b agree_car x a {n} b
end.
Instance agree_valid : Valid (agree A) := λ x, n, {n} x.
Local Instance agree_valid_instance : Valid (agree A) := λ x, n, {n} x.
Program Instance agree_op : Op (agree A) := λ x y,
Local Program Instance agree_op_instance : Op (agree A) := λ x y,
{| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
Instance agree_pcore : PCore (agree A) := Some.
Local Instance agree_pcore_instance : PCore (agree A) := Some.
Lemma agree_validN_def n x :
{n} x a b, a agree_car x b agree_car x a {n} b.
Proof.
rewrite /validN /agree_validN. destruct (agree_car _) as [|? [|??]]; auto.
rewrite /validN /agree_validN_instance. destruct (agree_car _) as [|? [|??]]; auto.
setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Instance agree_comm : Comm () (@op (agree A) _).
Local Instance agree_comm : Comm () (@op (agree A) _).
Proof. intros x y n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
Instance agree_assoc : Assoc () (@op (agree A) _).
Local Instance agree_assoc : Assoc () (@op (agree A) _).
Proof.
intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
Qed.
Lemma agree_idemp x : x x x.
Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n).
Local Instance agree_validN_ne n :
Proper (dist n ==> impl) (@validN SI (agree A) _ n).
Proof.
intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb.
destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto.
Qed.
Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n).
Local Instance agree_validN_proper n :
Proper (equiv ==> iff) (@validN SI (agree A) _ n).
Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed.
Instance agree_op_ne' x : NonExpansive (op x).
Local Instance agree_op_ne' x : NonExpansive (op x).
Proof.
intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver.
Qed.
Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
Local Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
Instance agree_op_proper : Proper (() ==> () ==> ()) op := ne_proper_2 _.
Local Instance agree_op_proper : Proper (() ==> () ==> ()) (op (A := agree A)) :=
ne_proper_2 _.
Lemma agree_included x y : x y y x y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
Lemma agree_includedN n x y : x {n} y y {n} x y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
Lemma agree_op_invN n x1 x2 : {n} (x1 x2) x1 {n} x2.
Proof.
......@@ -139,7 +147,7 @@ Qed.
Definition agree_cmra_mixin : CmraMixin (agree A).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- intros n x; rewrite !agree_validN_def; eauto using dist_S.
- intros n m x; rewrite !agree_validN_def; eauto using dist_le.
- intros x. apply agree_idemp.
- intros n x y; rewrite !agree_validN_def /=.
setoid_rewrite elem_of_app; naive_solver.
......@@ -147,7 +155,7 @@ Proof.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin.
Canonical Structure agreeR : cmra := Cmra (agree A) agree_cmra_mixin.
Global Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
......@@ -178,6 +186,11 @@ Proof.
exists a. by rewrite elem_of_list_singleton -discrete_iff_0.
Qed.
Lemma agree_op_inv x y : (x y) x y.
Proof.
intros ?. apply equiv_dist=> n. by apply agree_op_invN, cmra_valid_validN.
Qed.
Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
Proof.
move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
......@@ -191,10 +204,9 @@ Proof.
destruct (elem_of_agree x) as [a ?].
exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Lemma to_agree_uninj x : x a, to_agree a x.
Proof.
rewrite /valid /agree_valid; setoid_rewrite agree_validN_def.
rewrite /valid /agree_valid_instance; setoid_rewrite agree_validN_def.
destruct (elem_of_agree x) as [a ?].
exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
......@@ -204,19 +216,24 @@ Proof.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
by move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
Lemma agree_valid_included x y : y x y x y.
Proof.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
by move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
Lemma to_agree_includedN n a b : to_agree a {n} to_agree b a {n} b.
Proof.
split; last by intros ->. intros [x [_ Hincl]].
by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
split; last by intros ->.
intros. by apply (inj to_agree), agree_valid_includedN.
Qed.
Lemma to_agree_included a b : to_agree a to_agree b a b.
Proof.
split; last by intros ->.
intros (x & Heq). apply equiv_dist=>n. destruct (Heq n) as [_ Hincl].
by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
intros. by apply (inj to_agree), agree_valid_included.
Qed.
Lemma to_agree_included_L `{!LeibnizEquiv A} a b : to_agree a to_agree b a = b.
Proof. unfold_leibniz. apply to_agree_included. Qed.
Global Instance agree_cancelable x : Cancelable x.
Proof.
......@@ -232,10 +249,6 @@ Proof.
by rewrite -EQy -EQz -Hx'y' -Hx'z'.
Qed.
Lemma agree_op_inv x y : (x y) x y.
Proof.
intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
Qed.
Lemma to_agree_op_invN a b n : {n} (to_agree a to_agree b) a {n} b.
Proof. by intros ?%agree_op_invN%(inj to_agree). Qed.
Lemma to_agree_op_inv a b : (to_agree a to_agree b) a b.
......@@ -258,9 +271,9 @@ Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
End agree.
Instance: Params (@to_agree) 1 := {}.
Arguments agreeO : clear implicits.
Arguments agreeR : clear implicits.
Global Instance: Params (@to_agree) 1 := {}.
Global Arguments agreeO {_} _.
Global Arguments agreeR {_} _.
Program Definition agree_map {A B} (f : A B) (x : agree A) : agree B :=
{| agree_car := f <$> agree_car x |}.
......@@ -275,15 +288,15 @@ Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
Proof. by apply agree_eq. Qed.
Section agree_map.
Context {A B : ofeT} (f : A B) {Hf: NonExpansive f}.
Context {SI : sidx} {A B : ofe} (f : A B) {Hf: NonExpansive f}.
Instance agree_map_ne : NonExpansive (agree_map f).
Local Instance agree_map_ne : NonExpansive (agree_map f).
Proof using Type*.
intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap.
- intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
- intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.
Qed.
Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
Local Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
Lemma agree_map_ext (g : A B) x :
( a, f a g a) agree_map f x agree_map g x.
......@@ -305,31 +318,34 @@ Section agree_map.
Qed.
End agree_map.
Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
Definition agreeO_map {SI : sidx} {A B : ofe}
(f : A -n> B) : agreeO A -n> agreeO B :=
OfeMor (agree_map f : agreeO A agreeO B).
Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
Global Instance agreeO_map_ne {SI : sidx} A B : NonExpansive (@agreeO_map SI A B).
Proof.
intros n f g Hfg x; split=> b /=;
setoid_rewrite elem_of_list_fmap; naive_solver.
Qed.
Program Definition agreeRF (F : oFunctor) : rFunctor := {|
Program Definition agreeRF {SI : sidx} (F : oFunctor) : rFunctor := {|
rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
|}.
Next Obligation.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_map_ne.
intros ? ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
by apply agreeO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
intros ? F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
apply (agree_map_ext _)=>y. by rewrite oFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl.
rewrite -agree_map_compose.
apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
Qed.
Instance agreeRF_contractive F :
Global Instance agreeRF_contractive {SI : sidx} F :
oFunctorContractive F rFunctorContractive (agreeRF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
......
From iris.algebra Require Export view.
From iris.algebra Require Export view frac.
From iris.algebra Require Import proofmode_classes big_op.
From iris.prelude Require Import options.
(** The authoritative camera with fractional authoritative elements *)
(** The authoritative camera has 2 types of elements: the authoritative
element [●{q} a] and the fragment [◯ b] (of which there can be several). To
enable sharing of the authoritative element [●{q} a], it is equiped with a
fraction [q]. Updates are only possible with the full authoritative element
[● a] (syntax for [●{1} a]]), while fractional authoritative elements have
agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
(** The authoritative camera has 2 types of elements: the authoritative element
[●{dq} a] and the fragment [◯ b] (of which there can be several). To enable
sharing of the authoritative element [●{dq} a], it is equipped with a
discardable fraction [dq]. Updates are only possible with the full
authoritative element [● a] (syntax for [●{#1} a]]), while fractional
authoritative elements have agreement, i.e., [✓ (●{dq1} a1 ⋅ ●{dq2} a2) → a1 ≡
a2]. *)
(** * Definition of the view relation *)
(** The authoritative camera is obtained by instantiating the view camera. *)
Definition auth_view_rel_raw {A : ucmraT} (n : nat) (a b : A) : Prop :=
Definition auth_view_rel_raw {SI : sidx} {A : ucmra} (n : SI) (a b : A) : Prop :=
b {n} a {n} a.
Lemma auth_view_rel_raw_mono (A : ucmraT) n1 n2 (a1 a2 b1 b2 : A) :
Lemma auth_view_rel_raw_mono {SI : sidx} (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
auth_view_rel_raw n1 a1 b1
a1 {n2} a2
b2 {n2} b1
n2 n1
(n2 n1)%sidx
auth_view_rel_raw n2 a2 b2.
Proof.
intros [??] Ha12 ??. split.
- trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
- rewrite -Ha12. by apply cmra_validN_le with n1.
Qed.
Lemma auth_view_rel_raw_valid (A : ucmraT) n (a b : A) :
Lemma auth_view_rel_raw_valid {SI : sidx} (A : ucmra) n (a b : A) :
auth_view_rel_raw n a b {n} b.
Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
Lemma auth_view_rel_raw_unit (A : ucmraT) n :
Lemma auth_view_rel_raw_unit {SI : sidx} (A : ucmra) n :
a : A, auth_view_rel_raw n a ε.
Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
Canonical Structure auth_view_rel {A : ucmraT} : view_rel A A :=
Canonical Structure auth_view_rel {SI : sidx} {A : ucmra} : view_rel A A :=
ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
(auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).
Lemma auth_view_rel_unit {A : ucmraT} n (a : A) : auth_view_rel n a ε {n} a.
Lemma auth_view_rel_unit {SI : sidx} {A : ucmra} n (a : A) :
auth_view_rel n a ε {n} a.
Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
Lemma auth_view_rel_exists {A : ucmraT} n (b : A) :
Lemma auth_view_rel_exists {SI : sidx} {A : ucmra} n (b : A) :
( a, auth_view_rel n a b) {n} b.
Proof.
split; [|intros; exists b; by split].
intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
Qed.
Instance auth_view_rel_discrete {A : ucmraT} :
Global Instance auth_view_rel_discrete {SI : sidx} {A : ucmra} :
CmraDiscrete A ViewRelDiscrete (auth_view_rel (A:=A)).
Proof.
intros ? n a b [??]; split.
......@@ -54,56 +56,62 @@ Qed.
(** * Definition and operations on the authoritative camera *)
(** The type [auth] is not defined as a [Definition], but as a [Notation].
This way, one can use [auth A] with [A : Type] instead of [A : ucmraT], and let
This way, one can use [auth A] with [A : Type] instead of [A : ucmra], and let
canonical structure search determine the corresponding camera instance. *)
Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
Definition authO (A : ucmraT) : ofeT := viewO (A:=A) (B:=A) auth_view_rel.
Definition authR (A : ucmraT) : cmraT := viewR (A:=A) (B:=A) auth_view_rel.
Definition authUR (A : ucmraT) : ucmraT := viewUR (A:=A) (B:=A) auth_view_rel.
Definition authO {SI : sidx} (A : ucmra) : ofe :=
viewO (A:=A) (B:=A) auth_view_rel.
Definition authR {SI : sidx} (A : ucmra) : cmra :=
viewR (A:=A) (B:=A) auth_view_rel.
Definition authUR {SI : sidx} (A : ucmra) : ucmra :=
viewUR (A:=A) (B:=A) auth_view_rel.
Definition auth_auth {A: ucmraT} : Qp A auth A := view_auth.
Definition auth_frag {A: ucmraT} : A auth A := view_frag.
Definition auth_auth {SI : sidx} {A: ucmra} : dfrac A auth A := view_auth.
Definition auth_frag {SI : sidx} {A: ucmra} : A auth A := view_frag.
Typeclasses Opaque auth_auth auth_frag.
Global Typeclasses Opaque auth_auth auth_frag.
Instance: Params (@auth_auth) 2 := {}.
Instance: Params (@auth_frag) 1 := {}.
Global Instance: Params (@auth_auth) 3 := {}.
Global Instance: Params (@auth_frag) 2 := {}.
Notation "● dq a" := (auth_auth dq a)
(at level 20, dq custom dfrac at level 1, format "● dq a").
Notation "◯ a" := (auth_frag a) (at level 20).
Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q } a").
Notation "● a" := (auth_auth 1 a) (at level 20).
(** * Laws of the authoritative camera *)
(** We omit the usual [equivI] lemma because it is hard to state a suitably
general version in terms of [●] and [◯], and because such a lemma has never
been needed in practice. *)
Section auth.
Context {A : ucmraT}.
Context {SI : sidx} {A : ucmra}.
Implicit Types a b : A.
Implicit Types x y : auth A.
Implicit Types q : frac.
Implicit Types dq : dfrac.
Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
Global Instance auth_auth_ne dq : NonExpansive (@auth_auth SI A dq).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_auth_proper q : Proper (() ==> ()) (@auth_auth A q).
Global Instance auth_auth_proper dq : Proper (() ==> ()) (@auth_auth SI A dq).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
Global Instance auth_frag_ne : NonExpansive (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_proper : Proper (() ==> ()) (@auth_frag A).
Global Instance auth_frag_proper : Proper (() ==> ()) (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_auth_dist_inj n : Inj2 (=) (dist n) (dist n) (@auth_auth A).
Global Instance auth_auth_dist_inj n :
Inj2 (=) (dist n) (dist n) (@auth_auth SI A).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_auth_inj : Inj2 (=) () () (@auth_auth A).
Global Instance auth_auth_inj : Inj2 (=) () () (@auth_auth SI A).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag A).
Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_inj : Inj () () (@auth_frag A).
Global Instance auth_frag_inj : Inj () () (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_ofe_discrete : OfeDiscrete A OfeDiscrete (authO A).
Proof. apply _. Qed.
Global Instance auth_auth_discrete q a :
Discrete a Discrete (ε : A) Discrete ({q} a).
Global Instance auth_auth_discrete dq a :
Discrete a Discrete (ε : A) Discrete ({dq} a).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_discrete a : Discrete a Discrete ( a).
Proof. rewrite /auth_frag. apply _. Qed.
......@@ -111,10 +119,10 @@ Section auth.
Proof. apply _. Qed.
(** Operation *)
Lemma auth_auth_frac_op p q a : {p + q} a {p} a {q} a.
Proof. apply view_auth_frac_op. Qed.
Global Instance auth_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 IsOp' ({q} a) ({q1} a) ({q2} a).
Lemma auth_auth_dfrac_op dq1 dq2 a : {dq1 dq2} a {dq1} a {dq2} a.
Proof. apply view_auth_dfrac_op. Qed.
Global Instance auth_auth_dfrac_is_op dq dq1 dq2 a :
IsOp dq dq1 dq2 IsOp' ({dq} a) ({dq1} a) ({dq2} a).
Proof. rewrite /auth_auth. apply _. Qed.
Lemma auth_frag_op a b : (a b) = a b.
......@@ -123,13 +131,24 @@ Section auth.
Proof. apply view_frag_mono. Qed.
Lemma auth_frag_core a : core ( a) = (core a).
Proof. apply view_frag_core. Qed.
Lemma auth_both_core_discarded a b :
core (●□ a b) ●□ a (core b).
Proof. apply view_both_core_discarded. Qed.
Lemma auth_both_core_frac q a b :
core ({#q} a b) (core b).
Proof. apply view_both_core_frac. Qed.
Global Instance auth_auth_core_id a : CoreId (●□ a).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_core_id a : CoreId a CoreId ( a).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_both_core_id a1 a2 : CoreId a2 CoreId (●□ a1 a2).
Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
Global Instance auth_frag_is_op a b1 b2 :
IsOp a b1 b2 IsOp' ( a) ( b1) ( b2).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op () (@auth_frag A).
MonoidHomomorphism op op () (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
Lemma big_opL_auth_frag {B} (g : nat B A) (l : list B) :
......@@ -146,22 +165,22 @@ Section auth.
Proof. apply (big_opMS_commute _). Qed.
(** Validity *)
Lemma auth_auth_frac_op_invN n p a q b : {n} ({p} a {q} b) a {n} b.
Proof. apply view_auth_frac_op_invN. Qed.
Lemma auth_auth_frac_op_inv p a q b : ({p} a {q} b) a b.
Proof. apply view_auth_frac_op_inv. Qed.
Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
({p} a {q} b) a = b.
Proof. by apply view_auth_frac_op_inv_L. Qed.
Lemma auth_auth_frac_validN n q a : {n} ({q} a) (q 1)%Qp {n} a.
Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
Lemma auth_auth_dfrac_op_invN n dq1 a dq2 b : {n} ({dq1} a {dq2} b) a {n} b.
Proof. apply view_auth_dfrac_op_invN. Qed.
Lemma auth_auth_dfrac_op_inv dq1 a dq2 b : ({dq1} a {dq2} b) a b.
Proof. apply view_auth_dfrac_op_inv. Qed.
Lemma auth_auth_dfrac_op_inv_L `{!LeibnizEquiv A} dq1 a dq2 b :
({dq1} a {dq2} b) a = b.
Proof. by apply view_auth_dfrac_op_inv_L. Qed.
Lemma auth_auth_dfrac_validN n dq a : {n} ({dq} a) dq {n} a.
Proof. by rewrite view_auth_dfrac_validN auth_view_rel_unit. Qed.
Lemma auth_auth_validN n a : {n} ( a) {n} a.
Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
{n} ({q1} a1 {q2} a2) (q1 + q2 1)%Qp a1 {n} a2 {n} a1.
Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
Lemma auth_auth_dfrac_op_validN n dq1 dq2 a1 a2 :
{n} ({dq1} a1 {dq2} a2) (dq1 dq2) a1 {n} a2 {n} a1.
Proof. by rewrite view_auth_dfrac_op_validN auth_view_rel_unit. Qed.
Lemma auth_auth_op_validN n a1 a2 : {n} ( a1 a2) False.
Proof. apply view_auth_op_validN. Qed.
......@@ -180,15 +199,15 @@ Section auth.
Lemma auth_frag_op_validN_2 n b1 b2 : {n} (b1 b2) {n} ( b1 b2).
Proof. apply auth_frag_op_validN. Qed.
Lemma auth_both_frac_validN n q a b :
{n} ({q} a b) (q 1)%Qp b {n} a {n} a.
Proof. apply view_both_frac_validN. Qed.
Lemma auth_both_dfrac_validN n dq a b :
{n} ({dq} a b) dq b {n} a {n} a.
Proof. apply view_both_dfrac_validN. Qed.
Lemma auth_both_validN n a b : {n} ( a b) b {n} a {n} a.
Proof. apply view_both_validN. Qed.
Lemma auth_auth_frac_valid q a : ({q} a) (q 1)%Qp a.
Lemma auth_auth_dfrac_valid dq a : ({dq} a) dq a.
Proof.
rewrite view_auth_frac_valid !cmra_valid_validN.
rewrite view_auth_dfrac_valid !cmra_valid_validN.
by setoid_rewrite auth_view_rel_unit.
Qed.
Lemma auth_auth_valid a : ( a) a.
......@@ -197,10 +216,10 @@ Section auth.
by setoid_rewrite auth_view_rel_unit.
Qed.
Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
({q1} a1 {q2} a2) (q1 + q2 1)%Qp a1 a2 a1.
Lemma auth_auth_dfrac_op_valid dq1 dq2 a1 a2 :
({dq1} a1 {dq2} a2) (dq1 dq2) a1 a2 a1.
Proof.
rewrite view_auth_frac_op_valid !cmra_valid_validN.
rewrite view_auth_dfrac_op_valid !cmra_valid_validN.
setoid_rewrite auth_view_rel_unit. done.
Qed.
Lemma auth_auth_op_valid a1 a2 : ( a1 a2) False.
......@@ -227,10 +246,10 @@ Section auth.
(** These lemma statements are a bit awkward as we cannot possibly extract a
single witness for [b ≼ a] from validity, we have to make do with one witness
per step-index, i.e., [∀ n, b ≼{n} a]. *)
Lemma auth_both_frac_valid q a b :
({q} a b) (q 1)%Qp ( n, b {n} a) a.
Lemma auth_both_dfrac_valid dq a b :
({dq} a b) dq ( n, b {n} a) a.
Proof.
rewrite view_both_frac_valid. apply and_iff_compat_l. split.
rewrite view_both_dfrac_valid. apply and_iff_compat_l. split.
- intros Hrel. split.
+ intros n. by destruct (Hrel n).
+ apply cmra_valid_validN=> n. by destruct (Hrel n).
......@@ -238,35 +257,35 @@ Section auth.
Qed.
Lemma auth_both_valid a b :
( a b) ( n, b {n} a) a.
Proof. rewrite auth_both_frac_valid. naive_solver. Qed.
Proof. rewrite auth_both_dfrac_valid. split; [naive_solver|done]. Qed.
(* The reverse direction of the two lemmas below only holds if the camera is
discrete. *)
Lemma auth_both_frac_valid_2 q a b : (q 1)%Qp a b a ({q} a b).
Lemma auth_both_dfrac_valid_2 dq a b : dq a b a ({dq} a b).
Proof.
intros. apply auth_both_frac_valid.
intros. apply auth_both_dfrac_valid.
naive_solver eauto using cmra_included_includedN.
Qed.
Lemma auth_both_valid_2 a b : a b a ( a b).
Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
Proof. intros ??. by apply auth_both_dfrac_valid_2. Qed.
Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
({q} a b) (q 1)%Qp b a a.
Lemma auth_both_dfrac_valid_discrete `{!CmraDiscrete A} dq a b :
({dq} a b) dq b a a.
Proof.
rewrite auth_both_frac_valid. setoid_rewrite <-cmra_discrete_included_iff.
naive_solver eauto using O.
rewrite auth_both_dfrac_valid. setoid_rewrite <-cmra_discrete_included_iff.
pose 0. naive_solver.
Qed.
Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
( a b) b a a.
Proof. rewrite auth_both_frac_valid_discrete. naive_solver. Qed.
Proof. rewrite auth_both_dfrac_valid_discrete. split; [naive_solver|done]. Qed.
(** Inclusion *)
Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
{p1} a1 {n} {p2} a2 b (p1 p2)%Qp a1 {n} a2.
Proof. apply view_auth_frac_includedN. Qed.
Lemma auth_auth_frac_included p1 p2 a1 a2 b :
{p1} a1 {p2} a2 b (p1 p2)%Qp a1 a2.
Proof. apply view_auth_frac_included. Qed.
Lemma auth_auth_dfrac_includedN n dq1 dq2 a1 a2 b :
{dq1} a1 {n} {dq2} a2 b (dq1 dq2 dq1 = dq2) a1 {n} a2.
Proof. apply view_auth_dfrac_includedN. Qed.
Lemma auth_auth_dfrac_included dq1 dq2 a1 a2 b :
{dq1} a1 {dq2} a2 b (dq1 dq2 dq1 = dq2) a1 a2.
Proof. apply view_auth_dfrac_included. Qed.
Lemma auth_auth_includedN n a1 a2 b :
a1 {n} a2 b a1 {n} a2.
Proof. apply view_auth_includedN. Qed.
......@@ -274,21 +293,23 @@ Section auth.
a1 a2 b a1 a2.
Proof. apply view_auth_included. Qed.
Lemma auth_frag_includedN n p a b1 b2 :
b1 {n} {p} a b2 b1 {n} b2.
Lemma auth_frag_includedN n dq a b1 b2 :
b1 {n} {dq} a b2 b1 {n} b2.
Proof. apply view_frag_includedN. Qed.
Lemma auth_frag_included p a b1 b2 :
b1 {p} a b2 b1 b2.
Lemma auth_frag_included dq a b1 b2 :
b1 {dq} a b2 b1 b2.
Proof. apply view_frag_included. Qed.
(** The weaker [auth_both_included] lemmas below are a consequence of the
[auth_auth_included] and [auth_frag_included] lemmas above. *)
Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
{p1} a1 b1 {n} {p2} a2 b2 (p1 p2)%Qp a1 {n} a2 b1 {n} b2.
Proof. apply view_both_frac_includedN. Qed.
Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
{p1} a1 b1 {p2} a2 b2 (p1 p2)%Qp a1 a2 b1 b2.
Proof. apply view_both_frac_included. Qed.
Lemma auth_both_dfrac_includedN n dq1 dq2 a1 a2 b1 b2 :
{dq1} a1 b1 {n} {dq2} a2 b2
(dq1 dq2 dq1 = dq2) a1 {n} a2 b1 {n} b2.
Proof. apply view_both_dfrac_includedN. Qed.
Lemma auth_both_dfrac_included dq1 dq2 a1 a2 b1 b2 :
{dq1} a1 b1 {dq2} a2 b2
(dq1 dq2 dq1 = dq2) a1 a2 b1 b2.
Proof. apply view_both_dfrac_included. Qed.
Lemma auth_both_includedN n a1 a2 b1 b2 :
a1 b1 {n} a2 b2 a1 {n} a2 b1 {n} b2.
Proof. apply view_both_includedN. Qed.
......@@ -314,11 +335,17 @@ Section auth.
intros. etrans; first exact: auth_update_alloc.
exact: cmra_update_op_l.
Qed.
Lemma auth_update_frac_alloc q a b `{!CoreId b} :
b a {q} a ~~> {q} a b.
Lemma auth_update_auth_persist dq a : {dq} a ~~> ●□ a.
Proof. apply view_update_auth_persist. Qed.
Lemma auth_updateP_auth_unpersist a : ●□ a ~~>: λ k, q, k = {#q} a.
Proof. apply view_updateP_auth_unpersist. Qed.
Lemma auth_updateP_both_unpersist a b : ●□ a b ~~>: λ k, q, k = {#q} a b.
Proof. apply view_updateP_both_unpersist. Qed.
Lemma auth_update_dfrac_alloc dq a b `{!CoreId b} :
b a {dq} a ~~> {dq} a b.
Proof.
intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
intros Ha%(core_id_extract _ _). apply view_update_dfrac_alloc=> n bf [??].
split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
Qed.
......@@ -333,45 +360,45 @@ Section auth.
End auth.
(** * Functor *)
Program Definition authURF (F : urFunctor) : urFunctor := {|
Program Definition authURF {SI : sidx} (F : urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Next Obligation.
intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
apply viewO_map_ne; by apply urFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
intros ? F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
rewrite -view_map_compose.
apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_compose.
Qed.
Next Obligation.
intros F A1 ? A2 ? B1 ? B2 ? fg; simpl.
intros ? F A1 ? A2 ? B1 ? B2 ? fg; simpl.
apply view_map_cmra_morphism; [apply _..|]=> n a b [??]; split.
- by apply (cmra_morphism_monotoneN _).
- by apply (cmra_morphism_validN _).
Qed.
Instance authURF_contractive F :
Global Instance authURF_contractive {SI : sidx} F :
urFunctorContractive F urFunctorContractive (authURF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
apply viewO_map_ne; by apply urFunctor_map_contractive.
Qed.
Program Definition authRF (F : urFunctor) : rFunctor := {|
Program Definition authRF {SI : sidx} (F : urFunctor) : rFunctor := {|
rFunctor_car A _ B _ := authR (urFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Solve Obligations with apply authURF.
Solve Obligations with apply @authURF.
Instance authRF_contractive F :
Global Instance authRF_contractive {SI : sidx} F :
urFunctorContractive F rFunctorContractive (authRF F).
Proof. apply authURF_contractive. Qed.
......@@ -20,14 +20,15 @@ Since these big operators are like quantifiers, they have the same precedence as
[∀] and [∃]. *)
(** * Big ops over lists *)
Fixpoint big_opL `{Monoid M o} {A} (f : nat A M) (xs : list A) : M :=
Fixpoint big_opL {SI : sidx} {M : ofe}
{o : M M M} `{!Monoid o} {A} (f : nat A M) (xs : list A) : M :=
match xs with
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Instance: Params (@big_opL) 4 := {}.
Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Global Instance: Params (@big_opL) 5 := {}.
Global Arguments big_opL {SI} {M} o {_ A} _ !_ /.
Global Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
......@@ -35,13 +36,15 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope.
Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Local Definition big_opM_def {SI : sidx} {M : ofe}
{o : M M M} `{!Monoid o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
Local Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Instance: Params (@big_opM) 7 := {}.
Global Arguments big_opM {SI} {M} o {_ K _ _ A} _ _.
Local Definition big_opM_unseal :
@big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Global Instance: Params (@big_opM) 8 := {}.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope.
......@@ -49,31 +52,35 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope.
Definition big_opS_def `{Monoid M o} `{Countable A} (f : A M)
Local Definition big_opS_def {SI : sidx} {M : ofe}
{o : M M M} `{!Monoid o} `{Countable A} (f : A M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Local Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Instance: Params (@big_opS) 6 := {}.
Global Arguments big_opS {SI} {M} o {_ A _ _} _ _.
Local Definition big_opS_unseal :
@big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Global Instance: Params (@big_opS) 7 := {}.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope.
Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A M)
Local Definition big_opMS_def {SI : sidx} {M : ofe}
{o : M M M} `{!Monoid o} `{Countable A} (f : A M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Local Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Instance: Params (@big_opMS) 6 := {}.
Global Arguments big_opMS {SI} {M} o {_ A _ _} _ _.
Local Definition big_opMS_unseal :
@big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Global Instance: Params (@big_opMS) 8 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o mset] x ∈ X , P") : stdpp_scope.
(** * Properties about big ops *)
Section big_op.
Context `{Monoid M o}.
Context {SI : sidx} {M : ofe} {o : M M M} `{!Monoid o}.
Implicit Types xs : list M.
Infix "`o`" := o (at level 50, left associativity).
......@@ -97,10 +104,23 @@ Section list.
revert f. induction l1 as [|x l1 IH]=> f /=; first by rewrite left_id.
by rewrite IH assoc.
Qed.
Lemma big_opL_snoc f l x :
([^o list] ky l ++ [x], f k y) ([^o list] ky l, f k y) `o` f (length l) x.
Proof. rewrite big_opL_app big_opL_singleton Nat.add_0_r //. Qed.
Lemma big_opL_unit l : ([^o list] ky l, monoid_unit) (monoid_unit : M).
Proof. induction l; rewrite /= ?left_id //. Qed.
Lemma big_opL_take_drop Φ l n :
([^o list] k x l, Φ k x)
([^o list] k x take n l, Φ k x) `o` ([^o list] k x drop n l, Φ (n + k) x).
Proof.
rewrite -{1}(take_drop n l) big_opL_app length_take.
destruct (decide (length l n)).
- rewrite drop_ge //=.
- rewrite Nat.min_l //=; lia.
Qed.
Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat B M)
l1 (l2 : list B) :
R monoid_unit monoid_unit
......@@ -168,7 +188,8 @@ Section list.
([^o list] k y l1, f k y) ([^o list] k y l2, g k y).
Proof.
intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
intros k. assert (l1 !! k l2 !! k) as Hlk by (by f_equiv).
(* FIXME (Coq #14441) unnecessary type annotation *)
intros k. assert (l1 !! k ≡@{option A} l2 !! k) as Hlk by (by f_equiv).
destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
......@@ -206,6 +227,18 @@ Section list.
revert f g; induction l as [|x l IH]=> f g /=; first by rewrite left_id.
by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ `o` _)]comm -!assoc.
Qed.
(** Shows that some property [P] is closed under [big_opL]. Examples of [P]
are [Persistent], [Affine], [Timeless]. *)
Lemma big_opL_closed (P : M Prop) f l :
P monoid_unit
( x y, P x P y P (x `o` y))
( k x, l !! k = Some x P (f k x))
P ([^o list] kx l, f k x).
Proof.
intros Hunit Hop. revert f. induction l as [|x l IH]=> f Hf /=; [done|].
apply Hop; first by auto. apply IH=> k. apply (Hf (S k)).
Qed.
End list.
Lemma big_opL_bind {A B} (h : A list B) (f : B M) l :
......@@ -214,23 +247,43 @@ Proof.
revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite big_opL_app IH.
Qed.
Lemma big_opL_sep_zip_with {A B C} (f : A B C) (g1 : C A) (g2 : C B)
(h1 : nat A M) (h2 : nat B M) l1 l2 :
( x y, g1 (f x y) = x)
( x y, g2 (f x y) = y)
length l1 = length l2
([^o list] kxy zip_with f l1 l2, h1 k (g1 xy) `o` h2 k (g2 xy))
([^o list] kx l1, h1 k x) `o` ([^o list] ky l2, h2 k y).
Proof.
intros Hlen Hg1 Hg2. rewrite big_opL_op.
rewrite -(big_opL_fmap g1) -(big_opL_fmap g2).
rewrite fmap_zip_with_r; [|auto with lia..].
by rewrite fmap_zip_with_l; [|auto with lia..].
Qed.
Lemma big_opL_sep_zip {A B} (h1 : nat A M) (h2 : nat B M) l1 l2 :
length l1 = length l2
([^o list] kxy zip l1 l2, h1 k xy.1 `o` h2 k xy.2)
([^o list] kx l1, h1 k x) `o` ([^o list] ky l2, h2 k y).
Proof. by apply big_opL_sep_zip_with. Qed.
(** ** Big ops over finite maps *)
Lemma big_opM_empty `{Countable K} {B} (f : K B M) :
([^o map] kx , f k x) = monoid_unit.
Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed.
Proof. by rewrite big_opM_unseal /big_opM_def map_to_list_empty. Qed.
Lemma big_opM_insert `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
m !! i = None
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky m, f k y.
Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed.
Proof. intros ?. by rewrite big_opM_unseal /big_opM_def map_to_list_insert. Qed.
Lemma big_opM_delete `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
m !! i = Some x
([^o map] ky m, f k y) f i x `o` [^o map] ky delete i m, f k y.
Proof.
intros. rewrite -big_opM_insert ?lookup_delete //.
by rewrite insert_delete insert_id.
by rewrite insert_delete.
Qed.
Section gmap.
......@@ -270,7 +323,7 @@ Section gmap.
( k x, m !! k = Some x R (f k x) (g k x))
R ([^o map] k x m, f k x) ([^o map] k x m, g k x).
Proof.
intros ?? Hf. rewrite big_opM_eq. apply (big_opL_gen_proper R); auto.
intros ?? Hf. rewrite big_opM_unseal. apply (big_opL_gen_proper R); auto.
intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
Qed.
......@@ -301,7 +354,8 @@ Section gmap.
([^o map] k y m1, f k y) ([^o map] k y m2, g k y).
Proof.
intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
intros k. assert (m1 !! k m2 !! k) as Hlk by (by f_equiv).
(* FIXME (Coq #14441) unnecessary type annotation *)
intros k. assert (m1 !! k ≡@{option A} m2 !! k) as Hlk by (by f_equiv).
destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
......@@ -314,6 +368,19 @@ Section gmap.
(big_opM o (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opM_proper; intros; apply Hf. Qed.
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opM_map_to_list f m :
([^o map] kx m, f k x) [^o list] xk map_to_list m, f (xk.1) (xk.2).
Proof. rewrite big_opM_unseal. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
Lemma big_opM_list_to_map f l :
NoDup l.*1
([^o map] kx list_to_map l, f k x) [^o list] xk l, f (xk.1) (xk.2).
Proof.
intros. rewrite big_opM_map_to_list.
by apply big_opL_permutation, map_to_list_to_map.
Qed.
Lemma big_opM_singleton f i x : ([^o map] ky {[i:=x]}, f k y) f i x.
Proof.
rewrite -insert_empty big_opM_insert/=; last eauto using lookup_empty.
......@@ -322,13 +389,13 @@ Section gmap.
Lemma big_opM_unit m : ([^o map] ky m, monoid_unit) (monoid_unit : M).
Proof.
by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_eq.
by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_unseal.
Qed.
Lemma big_opM_fmap {B} (h : A B) (f : K B M) m :
([^o map] ky h <$> m, f k y) ([^o map] ky m, f k (h y)).
Proof.
rewrite big_opM_eq /big_opM_def map_to_list_fmap big_opL_fmap.
rewrite big_opM_unseal /big_opM_def map_to_list_fmap big_opL_fmap.
by apply big_opL_proper=> ? [??].
Qed.
......@@ -340,7 +407,7 @@ Section gmap.
{ by rewrite omap_empty !big_opM_empty. }
assert (omap h m !! i = None) by (by rewrite lookup_omap Hmi).
destruct (h x) as [y|] eqn:Hhx.
- by rewrite (omap_insert _ _ _ _ y) // !big_opM_insert // IH Hhx.
- by rewrite omap_insert Hhx //= !big_opM_insert // IH Hhx.
- rewrite omap_insert_None // delete_notin // big_opM_insert //.
by rewrite Hhx /= left_id.
Qed.
......@@ -348,14 +415,14 @@ Section gmap.
Lemma big_opM_insert_delete `{Countable K} {B} (f : K B M) (m : gmap K B) i x :
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky delete i m, f k y.
Proof.
rewrite -insert_delete big_opM_insert; first done. by rewrite lookup_delete.
rewrite -insert_delete_insert big_opM_insert; first done. by rewrite lookup_delete.
Qed.
Lemma big_opM_insert_override (f : K A M) m i x x' :
m !! i = Some x f i x f i x'
([^o map] ky <[i:=x']> m, f k y) ([^o map] ky m, f k y).
Proof.
intros ? Hx. rewrite -insert_delete big_opM_insert ?lookup_delete //.
intros ? Hx. rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
by rewrite -Hx -big_opM_delete.
Qed.
......@@ -373,6 +440,20 @@ Section gmap.
([^o map] ky <[i:=x]> m, <[i:=P]> f k) (P `o` [^o map] ky m, f k).
Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
Lemma big_opM_filter' (φ : K * A Prop) `{ kx, Decision (φ kx)} f m :
([^o map] k x filter φ m, f k x)
([^o map] k x m, if decide (φ (k, x)) then f k x else monoid_unit).
Proof.
induction m as [|k v m ? IH] using map_ind.
{ by rewrite map_filter_empty !big_opM_empty. }
destruct (decide (φ (k, v))).
- rewrite map_filter_insert_True //.
assert (filter φ m !! k = None) by (apply map_lookup_filter_None; eauto).
by rewrite !big_opM_insert // decide_True // IH.
- rewrite map_filter_insert_not' //; last by congruence.
rewrite !big_opM_insert // decide_False // IH. by rewrite left_id.
Qed.
Lemma big_opM_union f m1 m2 :
m1 ## m2
([^o map] ky m1 m2, f k y)
......@@ -390,10 +471,48 @@ Section gmap.
([^o map] kx m, f k x `o` g k x)
([^o map] kx m, f k x) `o` ([^o map] kx m, g k x).
Proof.
rewrite big_opM_eq /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
rewrite big_opM_unseal /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
Qed.
(** Shows that some property [P] is closed under [big_opM]. Examples of [P]
are [Persistent], [Affine], [Timeless]. *)
Lemma big_opM_closed (P : M Prop) f m :
Proper (() ==> iff) P
P monoid_unit
( x y, P x P y P (x `o` y))
( k x, m !! k = Some x P (f k x))
P ([^o map] kx m, f k x).
Proof.
intros ?? Hop Hf. induction m as [|k x ?? IH] using map_ind.
{ by rewrite big_opM_empty. }
rewrite big_opM_insert //. apply Hop.
{ apply Hf. by rewrite lookup_insert. }
apply IH=> k' x' ?. apply Hf. rewrite lookup_insert_ne; naive_solver.
Qed.
End gmap.
Lemma big_opM_sep_zip_with `{Countable K} {A B C}
(f : A B C) (g1 : C A) (g2 : C B)
(h1 : K A M) (h2 : K B M) m1 m2 :
( x y, g1 (f x y) = x)
( x y, g2 (f x y) = y)
( k, is_Some (m1 !! k) is_Some (m2 !! k))
([^o map] kxy map_zip_with f m1 m2, h1 k (g1 xy) `o` h2 k (g2 xy))
([^o map] kx m1, h1 k x) `o` ([^o map] ky m2, h2 k y).
Proof.
intros Hdom Hg1 Hg2. rewrite big_opM_op.
rewrite -(big_opM_fmap g1) -(big_opM_fmap g2).
rewrite map_fmap_zip_with_r; [|naive_solver..].
by rewrite map_fmap_zip_with_l; [|naive_solver..].
Qed.
Lemma big_opM_sep_zip `{Countable K} {A B}
(h1 : K A M) (h2 : K B M) m1 m2 :
( k, is_Some (m1 !! k) is_Some (m2 !! k))
([^o map] kxy map_zip m1 m2, h1 k xy.1 `o` h2 k xy.2)
([^o map] kx m1, h1 k x) `o` ([^o map] ky m2, h2 k y).
Proof. intros. by apply big_opM_sep_zip_with. Qed.
(** ** Big ops over finite sets *)
Section gset.
......@@ -406,7 +525,7 @@ Section gset.
( x, x X R (f x) (g x))
R ([^o set] x X, f x) ([^o set] x X, g x).
Proof.
rewrite big_opS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
rewrite big_opS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
Qed.
......@@ -433,12 +552,18 @@ Section gset.
Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opS_proper; intros; apply Hf. Qed.
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opS_elements f X :
([^o set] x X, f x) [^o list] x elements X, f x.
Proof. by rewrite big_opS_unseal. Qed.
Lemma big_opS_empty f : ([^o set] x , f x) = monoid_unit.
Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
Proof. by rewrite big_opS_unseal /big_opS_def elements_empty. Qed.
Lemma big_opS_insert f X x :
x X ([^o set] y {[ x ]} X, f y) (f x `o` [^o set] y X, f y).
Proof. intros. by rewrite big_opS_eq /big_opS_def elements_union_singleton. Qed.
Proof. intros. by rewrite !big_opS_elements elements_union_singleton. Qed.
Lemma big_opS_fn_insert {B} (f : A B M) h X x b :
x X
([^o set] y {[ x ]} X, f y (<[x:=b]> h y))
......@@ -470,25 +595,83 @@ Section gset.
Qed.
Lemma big_opS_singleton f x : ([^o set] y {[ x ]}, f y) f x.
Proof. intros. by rewrite big_opS_eq /big_opS_def elements_singleton /= right_id. Qed.
Proof. intros. by rewrite big_opS_elements elements_singleton /= right_id. Qed.
Lemma big_opS_unit X : ([^o set] y X, monoid_unit) (monoid_unit : M).
Proof.
by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_unseal.
Qed.
Lemma big_opS_filter' (φ : A Prop) `{ x, Decision (φ x)} f X :
([^o set] y filter φ X, f y)
([^o set] y X, if decide (φ y) then f y else monoid_unit).
Proof.
induction X as [|x X ? IH] using set_ind_L.
{ by rewrite filter_empty_L !big_opS_empty. }
destruct (decide (φ x)).
- rewrite filter_union_L filter_singleton_L //.
rewrite !big_opS_insert //; last set_solver.
by rewrite decide_True // IH.
- rewrite filter_union_L filter_singleton_not_L // left_id_L.
by rewrite !big_opS_insert // decide_False // IH left_id.
Qed.
Lemma big_opS_op f g X :
([^o set] y X, f y `o` g y) ([^o set] y X, f y) `o` ([^o set] y X, g y).
Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
Proof. by rewrite !big_opS_elements -big_opL_op. Qed.
Lemma big_opS_list_to_set f (l : list A) :
NoDup l
([^o set] x list_to_set l, f x) [^o list] x l, f x.
Proof.
induction 1 as [|x l ?? IHl].
- rewrite big_opS_empty //.
- rewrite /= big_opS_union; last set_solver.
by rewrite big_opS_singleton IHl.
Qed.
(** Shows that some property [P] is closed under [big_opS]. Examples of [P]
are [Persistent], [Affine], [Timeless]. *)
Lemma big_opS_closed (P : M Prop) f X :
Proper (() ==> iff) P
P monoid_unit
( x y, P x P y P (x `o` y))
( x, x X P (f x))
P ([^o set] x X, f x).
Proof.
intros ?? Hop Hf. induction X as [|x X ? IH] using set_ind_L.
{ by rewrite big_opS_empty. }
rewrite big_opS_insert //. apply Hop.
{ apply Hf. set_solver. }
apply IH=> x' ?. apply Hf. set_solver.
Qed.
End gset.
Lemma big_opS_set_map `{Countable A, Countable B} (h : A B) (X : gset A) (f : B M) :
Inj (=) (=) h
([^o set] x set_map h X, f x) ([^o set] x X, f (h x)).
Proof.
intros Hinj.
induction X as [|x X ? IH] using set_ind_L.
{ by rewrite set_map_empty !big_opS_empty. }
rewrite set_map_union_L set_map_singleton_L.
rewrite !big_opS_union; [|set_solver..].
rewrite !big_opS_singleton IH //.
Qed.
Lemma big_opM_dom `{Countable K} {A} (f : K M) (m : gmap K A) :
([^o map] k↦_ m, f k) ([^o set] k dom _ m, f k).
([^o map] k↦_ m, f k) ([^o set] k dom m, f k).
Proof.
induction m as [|i x ?? IH] using map_ind.
{ by rewrite big_opM_eq big_opS_eq dom_empty_L. }
{ by rewrite big_opM_unseal big_opS_unseal dom_empty_L. }
by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
Qed.
Lemma big_opM_gset_to_gmap `{Countable K} {A} (f : K A M) (X : gset K) c :
([^o map] ka gset_to_gmap c X, f k a) ([^o set] k X, f k c).
Proof.
rewrite -{2}(dom_gset_to_gmap X c) -big_opM_dom.
apply big_opM_proper. by intros k ? [_ ->]%lookup_gset_to_gmap_Some.
Qed.
(** ** Big ops over finite msets *)
Section gmultiset.
......@@ -501,7 +684,7 @@ Section gmultiset.
( x, x X R (f x) (g x))
R ([^o mset] x X, f x) ([^o mset] x X, g x).
Proof.
rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
rewrite big_opMS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
Qed.
......@@ -528,20 +711,30 @@ Section gmultiset.
Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opMS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opMS_proper; intros; apply Hf. Qed.
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opMS_elements f X :
([^o mset] x X, f x) [^o list] x elements X, f x.
Proof. by rewrite big_opMS_unseal. Qed.
Lemma big_opMS_empty f : ([^o mset] x , f x) = monoid_unit.
Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_empty. Qed.
Lemma big_opMS_disj_union f X Y :
([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y.
Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x.
Lemma big_opMS_singleton f x : ([^o mset] y {[+ x +]}, f y) f x.
Proof.
intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
intros. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_singleton /= right_id.
Qed.
Lemma big_opMS_insert f X x :
([^o mset] y {[+ x +]} X, f y) (f x `o` [^o mset] y X, f y).
Proof. intros. rewrite big_opMS_disj_union big_opMS_singleton //. Qed.
Lemma big_opMS_delete f X x :
x X ([^o mset] y X, f y) f x `o` [^o mset] y X {[ x ]}, f y.
x X ([^o mset] y X, f y) f x `o` [^o mset] y X {[+ x +]}, f y.
Proof.
intros. rewrite -big_opMS_singleton -big_opMS_disj_union.
by rewrite -gmultiset_disj_union_difference'.
......@@ -550,17 +743,128 @@ Section gmultiset.
Lemma big_opMS_unit X : ([^o mset] y X, monoid_unit) (monoid_unit : M).
Proof.
by induction X using gmultiset_ind;
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_eq.
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_unseal.
Qed.
Lemma big_opMS_op f g X :
([^o mset] y X, f y `o` g y) ([^o mset] y X, f y) `o` ([^o mset] y X, g y).
Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
Proof. by rewrite big_opMS_unseal /big_opMS_def -big_opL_op. Qed.
(** Shows that some property [P] is closed under [big_opMS]. Examples of [P]
are [Persistent], [Affine], [Timeless]. *)
Lemma big_opMS_closed (P : M Prop) f X :
Proper (() ==> iff) P
P monoid_unit
( x y, P x P y P (x `o` y))
( x, x X P (f x))
P ([^o mset] x X, f x).
Proof.
intros ?? Hop Hf. induction X as [|x X IH] using gmultiset_ind.
{ by rewrite big_opMS_empty. }
rewrite big_opMS_insert //. apply Hop.
{ apply Hf. set_solver. }
apply IH=> x' ?. apply Hf. set_solver.
Qed.
End gmultiset.
(** Commuting lemmas *)
Lemma big_opL_opL {A B} (f : nat A nat B M) (l1 : list A) (l2 : list B) :
([^o list] k1x1 l1, [^o list] k2x2 l2, f k1 x1 k2 x2)
([^o list] k2x2 l2, [^o list] k1x1 l1, f k1 x1 k2 x2).
Proof.
revert f l2. induction l1 as [|x1 l1 IH]; simpl; intros Φ l2.
{ by rewrite big_opL_unit. }
by rewrite IH big_opL_op.
Qed.
Lemma big_opL_opM {A} `{Countable K} {B}
(f : nat A K B M) (l1 : list A) (m2 : gmap K B) :
([^o list] k1x1 l1, [^o map] k2x2 m2, f k1 x1 k2 x2)
([^o map] k2x2 m2, [^o list] k1x1 l1, f k1 x1 k2 x2).
Proof. repeat setoid_rewrite big_opM_map_to_list. by rewrite big_opL_opL. Qed.
Lemma big_opL_opS {A} `{Countable B}
(f : nat A B M) (l1 : list A) (X2 : gset B) :
([^o list] k1x1 l1, [^o set] x2 X2, f k1 x1 x2)
([^o set] x2 X2, [^o list] k1x1 l1, f k1 x1 x2).
Proof. repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL. Qed.
Lemma big_opL_opMS {A} `{Countable B}
(f : nat A B M) (l1 : list A) (X2 : gmultiset B) :
([^o list] k1x1 l1, [^o mset] x2 X2, f k1 x1 x2)
([^o mset] x2 X2, [^o list] k1x1 l1, f k1 x1 x2).
Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
Lemma big_opM_opL {A} `{Countable K} {B}
(f : K A nat B M) (m1 : gmap K A) (l2 : list B) :
([^o map] k1x1 m1, [^o list] k2x2 l2, f k1 x1 k2 x2)
([^o list] k2x2 l2, [^o map] k1x1 m1, f k1 x1 k2 x2).
Proof. symmetry. apply big_opL_opM. Qed.
Lemma big_opM_opM `{Countable K1} {A} `{Countable K2} {B}
(f : K1 A K2 B M) (m1 : gmap K1 A) (m2 : gmap K2 B) :
([^o map] k1x1 m1, [^o map] k2x2 m2, f k1 x1 k2 x2)
([^o map] k2x2 m2, [^o map] k1x1 m1, f k1 x1 k2 x2).
Proof. repeat setoid_rewrite big_opM_map_to_list. by rewrite big_opL_opL. Qed.
Lemma big_opM_opS `{Countable K} {A} `{Countable B}
(f : K A B M) (m1 : gmap K A) (X2 : gset B) :
([^o map] k1x1 m1, [^o set] x2 X2, f k1 x1 x2)
([^o set] x2 X2, [^o map] k1x1 m1, f k1 x1 x2).
Proof.
repeat setoid_rewrite big_opM_map_to_list.
repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL.
Qed.
Lemma big_opM_opMS `{Countable K} {A} `{Countable B} (f : K A B M)
(m1 : gmap K A) (X2 : gmultiset B) :
([^o map] k1x1 m1, [^o mset] x2 X2, f k1 x1 x2)
([^o mset] x2 X2, [^o map] k1x1 m1, f k1 x1 x2).
Proof.
repeat setoid_rewrite big_opM_map_to_list.
repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL.
Qed.
Lemma big_opS_opL `{Countable A} {B}
(f : A nat B M) (X1 : gset A) (l2 : list B) :
([^o set] x1 X1, [^o list] k2x2 l2, f x1 k2 x2)
([^o list] k2x2 l2, [^o set] x1 X1, f x1 k2 x2).
Proof. symmetry. apply big_opL_opS. Qed.
Lemma big_opS_opM `{Countable A} `{Countable K} {B}
(f : A K B M) (X1 : gset A) (m2 : gmap K B) :
([^o set] x1 X1, [^o map] k2x2 m2, f x1 k2 x2)
([^o map] k2x2 m2, [^o set] x1 X1, f x1 k2 x2).
Proof. symmetry. apply big_opM_opS. Qed.
Lemma big_opS_opS `{Countable A, Countable B}
(X : gset A) (Y : gset B) (f : A B M) :
([^o set] x X, [^o set] y Y, f x y) ([^o set] y Y, [^o set] x X, f x y).
Proof. repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL. Qed.
Lemma big_opS_opMS `{Countable A, Countable B}
(X : gset A) (Y : gmultiset B) (f : A B M) :
([^o set] x X, [^o mset] y Y, f x y) ([^o mset] y Y, [^o set] x X, f x y).
Proof.
repeat setoid_rewrite big_opS_elements.
repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL.
Qed.
Lemma big_opMS_opL `{Countable A} {B}
(f : A nat B M) (X1 : gmultiset A) (l2 : list B) :
([^o mset] x1 X1, [^o list] k2x2 l2, f x1 k2 x2)
([^o list] k2x2 l2, [^o mset] x1 X1, f x1 k2 x2).
Proof. symmetry. apply big_opL_opMS. Qed.
Lemma big_opMS_opM `{Countable A} `{Countable K} {B} (f : A K B M)
(X1 : gmultiset A) (m2 : gmap K B) :
([^o mset] x1 X1, [^o map] k2x2 m2, f x1 k2 x2)
([^o map] k2x2 m2, [^o mset] x1 X1, f x1 k2 x2).
Proof. symmetry. apply big_opM_opMS. Qed.
Lemma big_opMS_opS `{Countable A, Countable B}
(X : gmultiset A) (Y : gset B) (f : A B M) :
([^o mset] x X, [^o set] y Y, f x y) ([^o set] y Y, [^o mset] x X, f x y).
Proof. symmetry. apply big_opS_opMS. Qed.
Lemma big_opMS_opMS `{Countable A, Countable B}
(X : gmultiset A) (Y : gmultiset B) (f : A B M) :
([^o mset] x X, [^o mset] y Y, f x y) ([^o mset] y Y, [^o mset] x X, f x y).
Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
End big_op.
Section homomorphisms.
Context `{Monoid M1 o1, Monoid M2 o2}.
Context {SI : sidx} {M1 M2 : ofe}.
Context {o1 : M1 M1 M1} {o2 : M2 M2 M2} `{!Monoid o1, !Monoid o2}.
Infix "`o1`" := o1 (at level 50, left associativity).
Infix "`o2`" := o2 (at level 50, left associativity).
(** The ssreflect rewrite tactic only works for relations that have a
......
From stdpp Require Import finite.
From iris.algebra Require Export ofe monoid.
From iris.prelude Require Import options.
Local Set Primitive Projections.
Local Open Scope sidx_scope.
Class PCore (A : Type) := pcore : A option A.
Global Hint Mode PCore ! : typeclass_instances.
Instance: Params (@pcore) 2 := {}.
Global Instance: Params (@pcore) 2 := {}.
Class Op (A : Type) := op : A A A.
Global Hint Mode Op ! : typeclass_instances.
Instance: Params (@op) 2 := {}.
Global Instance: Params (@op) 2 := {}.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
......@@ -16,41 +19,51 @@ Notation "(⋅)" := op (only parsing) : stdpp_scope.
reflexivity. However, if we used [option A], the following would no longer
hold:
x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
If you need the reflexive closure of the inclusion relation, you can use
[Some a ≼ Some b]. There are various [Some_included] lemmas that help
deal with propositions of this shape.
*)
Definition included `{Equiv A, Op A} (x y : A) := z, y x z.
Definition included {A} `{!Equiv A, !Op A} (x y : A) := z, y x z.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Global Hint Extern 0 (_ _) => reflexivity : core.
Instance: Params (@included) 3 := {}.
Global Instance: Params (@included) 3 := {}.
(** [opM] is used in some lemma statements where [A] has not yet been shown to
be a CMRA, so we define it directly in terms of [Op]. *)
Definition opM `{!Op A} (x : A) (my : option A) :=
match my with Some y => x y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
Class ValidN (A : Type) := validN : nat A Prop.
Global Hint Mode ValidN ! : typeclass_instances.
Instance: Params (@validN) 3 := {}.
Class ValidN {SI : sidx} (A : Type) := validN : SI A Prop.
Global Hint Mode ValidN - ! : typeclass_instances.
Global Instance: Params (@validN) 4 := {}.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A Prop.
Global Hint Mode Valid ! : typeclass_instances.
Instance: Params (@valid) 2 := {}.
Global Instance: Params (@valid) 2 := {}.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := z, y {n} x z.
Definition includedN {SI : sidx} `{!Dist A, Op A} (n : SI) (x y : A) :=
z, y {n} x z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4 := {}.
Global Instance: Params (@includedN) 5 := {}.
Global Hint Extern 0 (_ {_} _) => reflexivity : core.
Section mixin.
Local Set Primitive Projections.
Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
Record CmraMixin {SI : sidx} A
`{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {
(* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n (x y : A) cx :
x {n} y pcore x = Some cx cy, pcore y = Some cy cx {n} cy;
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
(* valid *)
mixin_cmra_valid_validN (x : A) : x n, {n} x;
mixin_cmra_validN_S n (x : A) : {S n} x {n} x;
mixin_cmra_validN_le n n' (x : A) : {n} x n' n {n'} x;
(* monoid *)
mixin_cmra_assoc : Assoc (≡@{A}) ();
mixin_cmra_comm : Comm (≡@{A}) ();
......@@ -66,7 +79,9 @@ Section mixin.
End mixin.
(** Bundled version *)
Structure cmraT := CmraT' {
#[projections(primitive=no)] (* FIXME: making this primitive leads to strange
TC resolution failures in view.v *)
Structure cmra {SI : sidx} := Cmra' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
......@@ -77,48 +92,63 @@ Structure cmraT := CmraT' {
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
Arguments CmraT' _ {_ _ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
Global Arguments Cmra' {_} _ {_ _ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [Cmra A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m) (only parsing).
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_pcore : simpl never.
Arguments cmra_op : simpl never.
Arguments cmra_valid : simpl never.
Arguments cmra_validN : simpl never.
Arguments cmra_ofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_ofeO (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
Global Arguments cmra_car : simpl never.
Global Arguments cmra_equiv : simpl never.
Global Arguments cmra_dist : simpl never.
Global Arguments cmra_pcore : simpl never.
Global Arguments cmra_op : simpl never.
Global Arguments cmra_valid : simpl never.
Global Arguments cmra_validN : simpl never.
Global Arguments cmra_ofe_mixin : simpl never.
Global Arguments cmra_mixin : simpl never.
Add Printing Constructor cmra.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
Coercion cmra_ofeO {SI : sidx} (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac A) : CmraMixin Ac := cmra_mixin Ac.
(** As explained more thoroughly in iris#539, Coq can run into trouble when
[cmra] combinators (such as [optionUR]) are stacked and combined with
coercions like [cmra_ofeO]. To partially address this, we give Coq's
type-checker some directions for unfolding, with the Strategy command.
For these structures, we instruct Coq to eagerly _expand_ all projections,
except for the coercion to type (in this case, [cmra_car]), since that causes
problem with canonical structure inference. Additionally, we make Coq
eagerly expand the coercions that go from one structure to another, like
[cmra_ofeO] in this case. *)
Global Strategy expand [cmra_ofeO cmra_equiv cmra_dist cmra_pcore cmra_op
cmra_valid cmra_validN cmra_ofe_mixin cmra_mixin].
Definition cmra_mixin_of' {SI : sidx} A {Ac : cmra}
(f : Ac A) : CmraMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
(** Lifting properties from the mixin *)
Section cmra_mixin.
Context {A : cmraT}.
Context {SI : sidx} {A : cmra}.
Implicit Types x y : A.
Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
Lemma cmra_pcore_ne n x y cx :
x {n} y pcore x = Some cx cy, pcore y = Some cy cx {n} cy.
Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.
Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN _ A _ n).
Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
Lemma cmra_valid_validN x : x n, {n} x.
Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
Lemma cmra_validN_S n x : {S n} x {n} x.
Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
Lemma cmra_validN_le n n' x : {n} x n' n {n'} x.
Proof. apply (mixin_cmra_validN_le _ (cmra_mixin A)). Qed.
Global Instance cmra_assoc : Assoc () (@op A _).
Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
Global Instance cmra_comm : Comm () (@op A _).
......@@ -138,57 +168,59 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin.
Definition opM {A : cmraT} (x : A) (my : option A) :=
match my with Some y => x y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x Some x.
Arguments core_id {_} _ {_}.
Global Hint Mode CoreId + ! : typeclass_instances.
Instance: Params (@CoreId) 1 := {}.
Class CoreId {SI : sidx} {A : cmra} (x : A) := core_id : pcore x Some x.
Global Arguments core_id {_ _} _ {_}.
Global Hint Mode CoreId - + ! : typeclass_instances.
Global Instance: Params (@CoreId) 2 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False.
Arguments exclusive0_l {_} _ {_} _ _.
Global Hint Mode Exclusive + ! : typeclass_instances.
Instance: Params (@Exclusive) 1 := {}.
Class Exclusive {SI : sidx} {A : cmra} (x : A) :=
exclusive0_l y : {0} (x y) False.
Global Arguments exclusive0_l {_ _} _ {_} _ _.
Global Hint Mode Exclusive - + ! : typeclass_instances.
Global Instance: Params (@Exclusive) 2 := {}.
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
cancelableN n y z : {n}(x y) x y {n} x z y {n} z.
Arguments cancelableN {_} _ {_} _ _ _ _.
Global Hint Mode Cancelable + ! : typeclass_instances.
Instance: Params (@Cancelable) 1 := {}.
Class Cancelable {SI : sidx} {A : cmra} (x : A) :=
cancelableN n y z : {n} (x y) x y {n} x z y {n} z.
Global Arguments cancelableN {_ _} _ {_} _ _ _ _.
Global Hint Mode Cancelable - + ! : typeclass_instances.
Global Instance: Params (@Cancelable) 2 := {}.
(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
id_free0_r y : {0}x x y {0} x False.
Arguments id_free0_r {_} _ {_} _ _.
Global Hint Mode IdFree + ! : typeclass_instances.
Instance: Params (@IdFree) 1 := {}.
Class IdFree {SI : sidx} {A : cmra} (x : A) :=
id_free0_r y : {0} x x y {0} x False.
Global Arguments id_free0_r {_ _} _ {_} _ _.
Global Hint Mode IdFree - + ! : typeclass_instances.
Global Instance: Params (@IdFree) 2 := {}.
(** * CMRAs whose core is total *)
Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Global Hint Mode CmraTotal ! : typeclass_instances.
Class CmraTotal {SI : sidx} (A : cmra) :=
cmra_total (x : A) : is_Some (pcore x).
Global Hint Mode CmraTotal - ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
to not require that proof to be able to call this function. *)
Definition core `{PCore A} (x : A) : A := default x (pcore x).
Instance: Params (@core) 2 := {}.
Definition core {A} `{!PCore A} (x : A) : A := default x (pcore x).
Global Instance: Params (@core) 2 := {}.
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
Global Hint Mode Unit ! : typeclass_instances.
Global Arguments ε {_ _}.
Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
Record UcmraMixin {SI : sidx} A
`{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
mixin_ucmra_unit_valid : (ε : A);
mixin_ucmra_unit_left_id : LeftId () ε ();
mixin_ucmra_pcore_unit : pcore ε Some ε
mixin_ucmra_unit_left_id : LeftId (@{A}) ε ();
mixin_ucmra_pcore_unit : pcore ε @{option A} Some ε
}.
Structure ucmraT := UcmraT' {
#[projections(primitive=no)] (* FIXME: making this primitive leads to strange
TC resolution failures in view.v *)
Structure ucmra {SI : sidx} := Ucmra' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
......@@ -201,30 +233,40 @@ Structure ucmraT := UcmraT' {
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
Notation UcmraT A m :=
(UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Arguments ucmra_pcore : simpl never.
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
Arguments ucmra_ofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Global Arguments Ucmra' {_} _ {_ _ _ _ _ _ _} _ _ _.
Notation Ucmra A m :=
(Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Global Arguments ucmra_car : simpl never.
Global Arguments ucmra_equiv : simpl never.
Global Arguments ucmra_dist : simpl never.
Global Arguments ucmra_pcore : simpl never.
Global Arguments ucmra_op : simpl never.
Global Arguments ucmra_valid : simpl never.
Global Arguments ucmra_validN : simpl never.
Global Arguments ucmra_ofe_mixin : simpl never.
Global Arguments ucmra_cmra_mixin : simpl never.
Global Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmra.
(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
Coercion ucmra_ofeO {SI : sidx} (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Coercion ucmra_cmraR {SI : sidx} (A : ucmra) : cmra :=
Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.
(** As for CMRAs above, we instruct Coq to eagerly _expand_ all projections,
except for the coercion to type (in this case, [ucmra_car]), since that causes
problem with canonical structure inference. Additionally, we make Coq
eagerly expand the coercions that go from one structure to another, like
[ucmra_cmraR] and [ucmra_ofeO] in this case. *)
Global Strategy expand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist ucmra_pcore
ucmra_op ucmra_valid ucmra_validN ucmra_unit
ucmra_ofe_mixin ucmra_cmra_mixin].
(** Lifting properties from the mixin *)
Section ucmra_mixin.
Context {A : ucmraT}.
Context {SI : sidx} {A : ucmra}.
Implicit Types x y : A.
Lemma ucmra_unit_valid : (ε : A).
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
......@@ -235,26 +277,29 @@ Section ucmra_mixin.
End ucmra_mixin.
(** * Discrete CMRAs *)
Class CmraDiscrete (A : cmraT) := {
cmra_discrete_ofe_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : {0} x x
#[projections(primitive=no)] (* FIXME: making this primitive means we cannot use
the projections with eauto any more (see https://github.com/coq/coq/issues/17561) *)
Class CmraDiscrete {SI : sidx} (A : cmra) := {
#[global] cmra_discrete_ofe_discrete :: OfeDiscrete A;
cmra_discrete_valid (x : A) : {0} x x
}.
Global Hint Mode CmraDiscrete ! : typeclass_instances.
Global Hint Mode CmraDiscrete - ! : typeclass_instances.
(** * Morphisms *)
Class CmraMorphism {A B : cmraT} (f : A B) := {
cmra_morphism_ne :> NonExpansive f;
Class CmraMorphism {SI : sidx} {A B : cmra} (f : A B) := {
#[global] cmra_morphism_ne :: NonExpansive f;
cmra_morphism_validN n x : {n} x {n} f x;
cmra_morphism_pcore x : f <$> pcore x pcore (f x);
cmra_morphism_op x y : f (x y) f x f y
}.
Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
Global Hint Mode CmraMorphism - - - ! : typeclass_instances.
Global Arguments cmra_morphism_validN {_ _ _} _ {_} _ _ _.
Global Arguments cmra_morphism_pcore {_ _ _} _ {_} _.
Global Arguments cmra_morphism_op {_ _ _} _ {_} _ _.
(** * Properties **)
Section cmra.
Context {A : cmraT}.
Context {SI : sidx} {A : cmra}.
Implicit Types x y z : A.
Implicit Types xs ys zs : list A.
......@@ -269,7 +314,7 @@ Qed.
Lemma cmra_pcore_proper x y cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy.
Proof.
intros. destruct (cmra_pcore_ne 0 x y cx) as (cy&?&?); auto.
intros. destruct (cmra_pcore_ne 0 x y cx) as (cy&?&?); auto.
exists cy; split; [done|apply equiv_dist=> n].
destruct (cmra_pcore_ne n x y cx) as (cy'&?&?); naive_solver.
Qed.
......@@ -279,9 +324,9 @@ Global Instance cmra_op_ne' : NonExpansive2 (@op A _).
Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
Global Instance cmra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_validN_ne' n : Proper (dist n ==> iff) (@validN A _ n) | 1.
Global Instance cmra_validN_ne' n : Proper (dist n ==> iff) (@validN SI A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
Global Instance cmra_validN_proper n : Proper (() ==> iff) (@validN A _ n) | 1.
Global Instance cmra_validN_proper n : Proper (() ==> iff) (@validN SI A _ n) | 1.
Proof. by intros x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
Global Instance cmra_valid_proper : Proper (() ==> iff) (@valid A _).
......@@ -290,13 +335,13 @@ Proof.
by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
Global Instance cmra_includedN_ne n :
Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
Proper (dist n ==> dist n ==> iff) (@includedN SI A _ _ n) | 1.
Proof.
intros x x' Hx y y' Hy.
by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_includedN_proper n :
Proper (() ==> () ==> iff) (@includedN A _ _ n) | 1.
Proper (() ==> () ==> iff) (@includedN SI A _ _ n) | 1.
Proof.
intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
by rewrite (Hx n) (Hy n).
......@@ -307,18 +352,18 @@ Proof.
intros x x' Hx y y' Hy.
by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_opM_ne : NonExpansive2 (@opM A).
Global Instance cmra_opM_ne : NonExpansive2 (@opM A _).
Proof. destruct 2; by ofe_subst. Qed.
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A).
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A _).
Proof. destruct 2; by setoid_subst. Qed.
Global Instance CoreId_proper : Proper (() ==> iff) (@CoreId A).
Global Instance CoreId_proper : Proper (() ==> iff) (@CoreId SI A).
Proof. solve_proper. Qed.
Global Instance Exclusive_proper : Proper (() ==> iff) (@Exclusive A).
Global Instance Exclusive_proper : Proper (() ==> iff) (@Exclusive SI A).
Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
Global Instance Cancelable_proper : Proper (() ==> iff) (@Cancelable A).
Global Instance Cancelable_proper : Proper (() ==> iff) (@Cancelable SI A).
Proof. intros x y Hxy. rewrite /Cancelable. by setoid_rewrite Hxy. Qed.
Global Instance IdFree_proper : Proper (() ==> iff) (@IdFree A).
Global Instance IdFree_proper : Proper (() ==> iff) (@IdFree SI A).
Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
(** ** Op *)
......@@ -326,8 +371,8 @@ Lemma cmra_op_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.
(** ** Validity *)
Lemma cmra_validN_le n n' x : {n} x n' n {n'} x.
Proof. induction 2; eauto using cmra_validN_S. Qed.
Lemma cmra_validN_lt n n' x : {n} x n' < n {n'} x.
Proof. eauto using cmra_validN_le, SIdx.lt_le_incl. Qed.
Lemma cmra_valid_op_l x y : (x y) x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_op_r n x y : {n} (x y) {n} y.
......@@ -337,13 +382,13 @@ Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
(** ** Core *)
Lemma cmra_pcore_l' x cx : pcore x Some cx cx x x.
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_l. Qed.
Lemma cmra_pcore_r x cx : pcore x = Some cx x cx x.
Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
Lemma cmra_pcore_r' x cx : pcore x Some cx x cx x.
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_r. Qed.
Lemma cmra_pcore_idemp' x cx : pcore x Some cx pcore cx Some cx.
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
Proof. intros (cx'&?&<-)%Some_equiv_eq. eauto using cmra_pcore_idemp. Qed.
Lemma cmra_pcore_dup x cx : pcore x = Some cx cx cx cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
Lemma cmra_pcore_dup' x cx : pcore x Some cx cx cx cx.
......@@ -359,11 +404,11 @@ Qed.
(** ** Exclusive elements *)
Lemma exclusiveN_l n x `{!Exclusive x} y : {n} (x y) False.
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
Proof. intros. by eapply (exclusive0_l x y), cmra_validN_le, SIdx.le_0_l. Qed.
Lemma exclusiveN_r n x `{!Exclusive x} y : {n} (y x) False.
Proof. rewrite comm. by apply exclusiveN_l. Qed.
Lemma exclusive_l x `{!Exclusive x} y : (x y) False.
Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
Lemma exclusive_r x `{!Exclusive x} y : (y x) False.
Proof. rewrite comm. by apply exclusive_l. Qed.
Lemma exclusiveN_opM n x `{!Exclusive x} my : {n} (x ? my) my = None.
......@@ -376,7 +421,7 @@ Proof. intros [? ->]. by apply exclusive_l. Qed.
(** ** Order *)
Lemma cmra_included_includedN n x y : x y x {n} y.
Proof. intros [z ->]. by exists z. Qed.
Global Instance cmra_includedN_trans n : Transitive (@includedN A _ _ n).
Global Instance cmra_includedN_trans n : Transitive (@includedN SI A _ _ n).
Proof.
intros x y z [z1 Hy] [z2 Hz]; exists (z1 z2). by rewrite assoc -Hy -Hz.
Qed.
......@@ -391,10 +436,10 @@ Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included n x y : {n} y x y {n} x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
Lemma cmra_includedN_S n x y : x {S n} y x {n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Lemma cmra_includedN_le n n' x y : x {n} y n' n x {n'} y.
Proof. induction 2; auto using cmra_includedN_S. Qed.
Lemma cmra_includedN_le n m x y : x {n} y m n x {m} y.
Proof. by intros [z Hz] H; exists z; eapply dist_le. Qed.
Lemma cmra_includedN_S n x y : x {Sᵢ n} y x {n} y.
Proof. intros ?. by eapply cmra_includedN_le, SIdx.le_succ_diag_r. Qed.
Lemma cmra_includedN_l n x y : x {n} x y.
Proof. by exists y. Qed.
......@@ -408,9 +453,9 @@ Proof. rewrite (comm op); apply cmra_included_l. Qed.
Lemma cmra_pcore_mono' x y cx :
x y pcore x Some cx cy, pcore y = Some cy cx cy.
Proof.
intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
intros ? (cx'&?&Hcx)%Some_equiv_eq.
destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
exists cy; by rewrite Hcx.
exists cy; by rewrite -Hcx.
Qed.
Lemma cmra_pcore_monoN' n x y cx :
x {n} y pcore x {n} Some cx cy, pcore y = Some cy cx {n} cy.
......@@ -469,7 +514,7 @@ Qed.
(** ** Total core *)
Section total_core.
Local Set Default Proof Using "Type*".
Context `{CmraTotal A}.
Context `{!CmraTotal A}.
Lemma cmra_pcore_core x : pcore x = Some (core x).
Proof.
......@@ -516,15 +561,16 @@ Section total_core.
Lemma core_id_core x `{!CoreId x} : core x x.
Proof. by apply core_id_total. Qed.
(** Not an instance since TC search cannot solve the premise. *)
Lemma cmra_pcore_core_id x y : pcore x = Some y CoreId y.
Proof. rewrite /CoreId. eauto using cmra_pcore_idemp. Qed.
Global Instance cmra_core_core_id x : CoreId (core x).
Proof.
destruct (cmra_total x) as [cx Hcx].
rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp.
Qed.
Proof. eapply cmra_pcore_core_id. rewrite cmra_pcore_core. done. Qed.
Lemma cmra_included_core x : core x x.
Proof. by exists x; rewrite cmra_core_l. Qed.
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Global Instance cmra_includedN_preorder n : PreOrder (@includedN SI A _ _ n).
Proof.
split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
Qed.
......@@ -540,45 +586,45 @@ Section total_core.
End total_core.
(** ** Discrete *)
Lemma cmra_discrete_included_l x y : Discrete x {0} y x {0} y x y.
Lemma cmra_discrete_included_l x y : Discrete x {0} y x {0} y x y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (discrete x z).
Qed.
Lemma cmra_discrete_included_r x y : Discrete y x {0} y x y.
Proof. intros ? [x' ?]. exists x'. by apply (discrete y). Qed.
destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (discrete_0 x z).
Qed.
Lemma cmra_discrete_included_r x y : Discrete y x {0} y x y.
Proof. intros ? [x' ?]. exists x'. by apply (discrete_0 y). Qed.
Lemma cmra_op_discrete x1 x2 :
(x1 x2) Discrete x1 Discrete x2 Discrete (x1 x2).
{0} (x1 x2) Discrete x1 Discrete x2 Discrete (x1 x2).
Proof.
intros ??? z Hz.
destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
{ rewrite -?Hz. by apply cmra_valid_validN. }
by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
{ rewrite -?Hz. done. }
by rewrite Hz' (discrete_0 x1 y1) // (discrete_0 x2 y2).
Qed.
(** ** Discrete *)
Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x : x {n} x.
Lemma cmra_discrete_valid_iff `{!CmraDiscrete A} n x : x {n} x.
Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
eauto using cmra_discrete_valid, cmra_validN_le, SIdx.le_0_l.
Qed.
Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : {0} x {n} x.
Lemma cmra_discrete_valid_iff_0 `{!CmraDiscrete A} n x : {0} x {n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x y x {n} y.
Lemma cmra_discrete_included_iff `{!OfeDiscrete A} n x y : x y x {n} y.
Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x {0} y x {n} y.
Lemma cmra_discrete_included_iff_0 `{!OfeDiscrete A} n x y : x {0} y x {n} y.
Proof. by rewrite -!cmra_discrete_included_iff. Qed.
(** Cancelable elements *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable SI A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
Lemma cancelable x `{!Cancelable x} y z : (x y) x y x z y z.
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
Lemma discrete_cancelable x `{CmraDiscrete A}:
Lemma discrete_cancelable x `{!CmraDiscrete A}:
( y z, (x y) x y x z y z) Cancelable x.
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
......@@ -593,25 +639,25 @@ Global Instance exclusive_cancelable (x : A) : Exclusive x → Cancelable x.
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
(** Id-free elements *)
Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree SI A).
Proof.
intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
intros x x' EQ%(dist_le _ 0); [|apply SIdx.le_0_l]. rewrite /IdFree.
split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
Qed.
Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree SI A).
Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
Lemma id_freeN_r n n' x `{!IdFree x} y : {n}x x y {n'} x False.
Proof. eauto using cmra_validN_le, dist_le with lia. Qed.
Proof. eauto using cmra_validN_le, dist_le, SIdx.le_0_l. Qed.
Lemma id_freeN_l n n' x `{!IdFree x} y : {n}x y x {n'} x False.
Proof. rewrite comm. eauto using id_freeN_r. Qed.
Lemma id_free_r x `{!IdFree x} y : x x y x False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
Lemma id_free_l x `{!IdFree x} y : x y x x False.
Proof. rewrite comm. eauto using id_free_r. Qed.
Lemma discrete_id_free x `{CmraDiscrete A}:
Lemma discrete_id_free x `{!CmraDiscrete A}:
( y, x x y x False) IdFree x.
Proof.
intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
intros Hx y ??. apply (Hx y), (discrete_0 _); eauto using cmra_discrete_valid.
Qed.
Global Instance id_free_op_r x y : IdFree y Cancelable x IdFree (x y).
Proof.
......@@ -621,12 +667,18 @@ Qed.
Global Instance id_free_op_l x y : IdFree x Cancelable y IdFree (x y).
Proof. intros. rewrite comm. apply _. Qed.
Global Instance exclusive_id_free x : Exclusive x IdFree x.
Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
End cmra.
(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
the new unification algorithm. The old unification algorithm sometimes gets
confused by going from [ucmra]'s to [cmra]'s and back. *)
Global Hint Extern 0 (?a ?a _) => apply: cmra_included_l : core.
Global Hint Extern 0 (?a _ ?a) => apply: cmra_included_r : core.
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Context {A : ucmraT}.
Context {SI : sidx} {A : ucmra}.
Implicit Types x y z : A.
Lemma ucmra_unit_validN n : {n} (ε:A).
......@@ -654,11 +706,12 @@ Section ucmra.
End ucmra.
Global Hint Immediate cmra_unit_cmra_total : core.
Global Hint Extern 0 (ε _) => apply: ucmra_unit_least : core.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
Local Set Default Proof Using "Type*".
Context {A : cmraT} `{!LeibnizEquiv A}.
Context {SI : sidx} {A : cmra} `{!LeibnizEquiv A}.
Implicit Types x y : A.
Global Instance cmra_assoc_L : Assoc (=) (@op A _).
......@@ -686,7 +739,7 @@ Section cmra_leibniz.
(** ** Total core *)
Section total_core.
Context `{CmraTotal A}.
Context `{!CmraTotal A}.
Lemma cmra_core_r_L x : x core x = x.
Proof. unfold_leibniz. apply cmra_core_r. Qed.
......@@ -705,7 +758,7 @@ End cmra_leibniz.
Section ucmra_leibniz.
Local Set Default Proof Using "Type*".
Context {A : ucmraT} `{!LeibnizEquiv A}.
Context {SI : sidx} {A : ucmra} `{!LeibnizEquiv A}.
Implicit Types x y z : A.
Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
......@@ -716,13 +769,13 @@ End ucmra_leibniz.
(** * Constructing a CMRA with total core *)
Section cmra_total.
Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
Context {SI : sidx} A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A}.
Context (total : x : A, is_Some (pcore x)).
Context (op_ne : x : A, NonExpansive (op x)).
Context (core_ne : NonExpansive (@core A _)).
Context (validN_ne : n, Proper (dist n ==> impl) (@validN A _ n)).
Context (validN_ne : n, Proper (dist n ==> impl) (@validN SI A _ n)).
Context (valid_validN : (x : A), x n, {n} x).
Context (validN_S : n (x : A), {S n} x {n} x).
Context (validN_le : n n' (x : A), {n} x n' n {n'} x).
Context (op_assoc : Assoc () (@op A _)).
Context (op_comm : Comm () (@op A _)).
Context (core_l : x : A, core x x x).
......@@ -746,7 +799,7 @@ Section cmra_total.
End cmra_total.
(** * Properties about morphisms *)
Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
Global Instance cmra_morphism_id {SI : sidx} {A : cmra} : CmraMorphism (@id A).
Proof.
split => /=.
- apply _.
......@@ -754,9 +807,11 @@ Proof.
- intros. by rewrite option_fmap_id.
- done.
Qed.
Instance cmra_morphism_proper {A B : cmraT} (f : A B) `{!CmraMorphism f} :
Global Instance cmra_morphism_proper {SI : sidx}
{A B : cmra} (f : A B) `{!CmraMorphism f} :
Proper (() ==> ()) f := ne_proper _.
Instance cmra_morphism_compose {A B C : cmraT} (f : A B) (g : B C) :
Global Instance cmra_morphism_compose {SI : sidx}
{A B C : cmra} (f : A B) (g : B C) :
CmraMorphism f CmraMorphism g CmraMorphism (g f).
Proof.
split.
......@@ -768,7 +823,7 @@ Qed.
Section cmra_morphism.
Local Set Default Proof Using "Type*".
Context {A B : cmraT} (f : A B) `{!CmraMorphism f}.
Context {SI : sidx} {A B : cmra} (f : A B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : f (core x) core (f x).
Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x y f x f y.
......@@ -780,8 +835,8 @@ Section cmra_morphism.
End cmra_morphism.
(** COFE → CMRA Functors *)
Record rFunctor := RFunctor {
rFunctor_car : A `{!Cofe A} B `{!Cofe B}, cmraT;
Record rFunctor {SI : sidx} := RFunctor {
rFunctor_car : A `{!Cofe A} B `{!Cofe B}, cmra;
rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
((A2 -n> A1) * (B1 -n> B2)) rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
......@@ -795,84 +850,88 @@ Record rFunctor := RFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_map_ne rFunctor_mor.
Instance: Params (@rFunctor_map) 9 := {}.
Global Existing Instances rFunctor_map_ne rFunctor_mor.
Global Instance: Params (@rFunctor_map) 10 := {}.
Declare Scope rFunctor_scope.
Delimit Scope rFunctor_scope with RF.
Bind Scope rFunctor_scope with rFunctor.
Class rFunctorContractive (F : rFunctor) :=
rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
Class rFunctorContractive {SI : sidx} (F : rFunctor) :=
#[global] rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
Contractive (@rFunctor_map SI F A1 _ A2 _ B1 _ B2 _).
Global Hint Mode rFunctorContractive - ! : typeclass_instances.
Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
Definition rFunctor_apply {SI : sidx} (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
rFunctor_car F A A.
Program Definition rFunctor_to_oFunctor (F: rFunctor) : oFunctor := {|
Program Definition rFunctor_to_oFunctor {SI : sidx} (F: rFunctor) : oFunctor := {|
oFunctor_car A _ B _ := rFunctor_car F A B;
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := rFunctor_map F fg
|}.
Next Obligation.
intros F A ? B ? x. simpl in *. apply rFunctor_map_id.
intros ? F A ? B ? x. simpl in *. apply rFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
apply rFunctor_map_compose.
Qed.
Global Instance rFunctor_to_oFunctor_contractive F :
Global Instance rFunctor_to_oFunctor_contractive {SI : sidx} F :
rFunctorContractive F oFunctorContractive (rFunctor_to_oFunctor F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply rFunctor_map_contractive. done.
Qed.
Program Definition rFunctor_oFunctor_compose (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
Program Definition rFunctor_oFunctor_compose
{SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
rFunctor_car A _ B _ := rFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
rFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
intros ? F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
apply rFunctor_map_ne; split; apply oFunctor_map_ne; by split.
Qed.
Next Obligation.
intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(rFunctor_map_id F1 x).
intros ? F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(rFunctor_map_id F1 x).
apply equiv_dist=> n. apply rFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_id.
Qed.
Next Obligation.
intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
intros ? F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
rewrite -rFunctor_map_compose. apply equiv_dist=> n. apply rFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
Instance rFunctor_oFunctor_compose_contractive_1 (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
Global Instance rFunctor_oFunctor_compose_contractive_1
{SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
rFunctorContractive F1 rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
Instance rFunctor_oFunctor_compose_contractive_2 (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
Global Instance rFunctor_oFunctor_compose_contractive_2
{SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
`{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
oFunctorContractive F2 rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
Qed.
Program Definition constRF (B : cmraT) : rFunctor :=
Program Definition constRF {SI : sidx} (B : cmra) : rFunctor :=
{| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
Coercion constRF : cmraT >-> rFunctor.
Coercion constRF : cmra >-> rFunctor.
Instance constRF_contractive B : rFunctorContractive (constRF B).
Global Instance constRF_contractive {SI : sidx} B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
(** COFE → UCMRA Functors *)
Record urFunctor := URFunctor {
urFunctor_car : A `{!Cofe A} B `{!Cofe B}, ucmraT;
Record urFunctor {SI : sidx} := URFunctor {
urFunctor_car : A `{!Cofe A} B `{!Cofe B}, ucmra;
urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
((A2 -n> A1) * (B1 -n> B2)) urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
urFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
......@@ -886,91 +945,96 @@ Record urFunctor := URFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_map_ne urFunctor_mor.
Instance: Params (@urFunctor_map) 9 := {}.
Global Existing Instances urFunctor_map_ne urFunctor_mor.
Global Instance: Params (@urFunctor_map) 10 := {}.
Declare Scope urFunctor_scope.
Delimit Scope urFunctor_scope with URF.
Bind Scope urFunctor_scope with urFunctor.
Class urFunctorContractive (F : urFunctor) :=
urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
Class urFunctorContractive {SI : sidx} (F : urFunctor) :=
#[global] urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
Contractive (@urFunctor_map SI F A1 _ A2 _ B1 _ B2 _).
Global Hint Mode urFunctorContractive - ! : typeclass_instances.
Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
Definition urFunctor_apply {SI : sidx} (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
urFunctor_car F A A.
Program Definition urFunctor_to_rFunctor (F: urFunctor) : rFunctor := {|
Program Definition urFunctor_to_rFunctor {SI : sidx} (F: urFunctor) : rFunctor := {|
rFunctor_car A _ B _ := urFunctor_car F A B;
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := urFunctor_map F fg
|}.
Next Obligation.
intros F A ? B ? x. simpl in *. apply urFunctor_map_id.
intros ? F A ? B ? x. simpl in *. apply urFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
apply urFunctor_map_compose.
Qed.
Global Instance urFunctor_to_rFunctor_contractive F :
Global Instance urFunctor_to_rFunctor_contractive {SI : sidx} F :
urFunctorContractive F rFunctorContractive (urFunctor_to_rFunctor F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply urFunctor_map_contractive. done.
Qed.
Program Definition urFunctor_oFunctor_compose (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
Program Definition urFunctor_oFunctor_compose
{SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
urFunctor_car A _ B _ := urFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
urFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
intros ? F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
apply urFunctor_map_ne; split; apply oFunctor_map_ne; by split.
Qed.
Next Obligation.
intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(urFunctor_map_id F1 x).
intros ? F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(urFunctor_map_id F1 x).
apply equiv_dist=> n. apply urFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_id.
Qed.
Next Obligation.
intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
intros ? F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
rewrite -urFunctor_map_compose. apply equiv_dist=> n. apply urFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
Instance urFunctor_oFunctor_compose_contractive_1 (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
Global Instance urFunctor_oFunctor_compose_contractive_1
{SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
urFunctorContractive F1 urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
Instance urFunctor_oFunctor_compose_contractive_2 (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
Global Instance urFunctor_oFunctor_compose_contractive_2
{SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
`{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
oFunctorContractive F2 urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
Qed.
Program Definition constURF (B : ucmraT) : urFunctor :=
Program Definition constURF {SI : sidx} (B : ucmra) : urFunctor :=
{| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.
Coercion constURF : ucmraT >-> urFunctor.
Coercion constURF : ucmra >-> urFunctor.
Instance constURF_contractive B : urFunctorContractive (constURF B).
Global Instance constURF_contractive {SI : sidx} B :
urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
Definition cmra_transport {SI : sidx} {A B : cmra} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
Lemma cmra_transport_trans {A B C : cmraT} (H1 : A = B) (H2 : B = C) x :
Lemma cmra_transport_trans {SI : sidx} {A B C : cmra} (H1 : A = B) (H2 : B = C) x :
cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
Proof. by destruct H2. Qed.
Section cmra_transport.
Context {A B : cmraT} (H : A = B).
Context {SI : sidx} {A B : cmra} (H : A = B).
Notation T := (cmra_transport H).
Global Instance cmra_transport_ne : NonExpansive T.
Proof. by intros ???; destruct H. Qed.
......@@ -1010,20 +1074,21 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
Section discrete.
Local Set Default Proof Using "Type*".
Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A ()).
Context {SI : sidx} `{!Equiv A, !PCore A, !Op A, !Valid A}.
Context (Heq : @Equivalence A ()).
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist.
Instance discrete_validN : ValidN A := λ n x, x.
Local Instance discrete_validN_instance : ValidN A := λ n x, x.
Definition discrete_cmra_mixin : CmraMixin A.
Proof.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ 0).
- intros x; split; first done. by move=> /(_ 0).
- intros n x y1 y2 ??; by exists y1, y2.
Qed.
Instance discrete_cmra_discrete :
CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
Local Instance discrete_cmra_discrete :
CmraDiscrete (Cmra' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
Proof. split; first apply _. done. Qed.
End discrete.
......@@ -1031,7 +1096,7 @@ End discrete.
[ofe_discrete_equivalence_of A] to make sure the same [Equivalence] proof is
used as when constructing the OFE. *)
Notation discreteR A ra_mix :=
(CmraT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(Cmra A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(only parsing).
Section ra_total.
......@@ -1062,18 +1127,19 @@ End ra_total.
(** ** CMRA for the unit type *)
Section unit.
Instance unit_valid : Valid () := λ x, True.
Instance unit_validN : ValidN () := λ n x, True.
Instance unit_pcore : PCore () := λ x, Some x.
Instance unit_op : Op () := λ x y, ().
Context {SI : sidx}.
Local Instance unit_valid_instance : Valid () := λ x, True.
Local Instance unit_validN_instance : ValidN () := λ n x, True.
Local Instance unit_pcore_instance : PCore () := λ x, Some x.
Local Instance unit_op_instance : Op () := λ x y, ().
Lemma unit_cmra_mixin : CmraMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
Canonical Structure unitR : cmraT := CmraT unit unit_cmra_mixin.
Canonical Structure unitR : cmra := Cmra unit unit_cmra_mixin.
Instance unit_unit : Unit () := ().
Local Instance unit_unit_instance : Unit () := ().
Lemma unit_ucmra_mixin : UcmraMixin ().
Proof. done. Qed.
Canonical Structure unitUR : ucmraT := UcmraT unit unit_ucmra_mixin.
Canonical Structure unitUR : ucmra := Ucmra unit unit_ucmra_mixin.
Global Instance unit_cmra_discrete : CmraDiscrete unitR.
Proof. done. Qed.
......@@ -1085,13 +1151,14 @@ End unit.
(** ** CMRA for the empty type *)
Section empty.
Instance Empty_set_valid : Valid Empty_set := λ x, False.
Instance Empty_set_validN : ValidN Empty_set := λ n x, False.
Instance Empty_set_pcore : PCore Empty_set := λ x, Some x.
Instance Empty_set_op : Op Empty_set := λ x y, x.
Context {SI : sidx}.
Local Instance Empty_set_valid_instance : Valid Empty_set := λ x, False.
Local Instance Empty_set_validN_instance : ValidN Empty_set := λ n x, False.
Local Instance Empty_set_pcore_instance : PCore Empty_set := λ x, Some x.
Local Instance Empty_set_op_instance : Op Empty_set := λ x y, x.
Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
Canonical Structure Empty_setR : cmraT := CmraT Empty_set Empty_set_cmra_mixin.
Canonical Structure Empty_setR : cmra := Cmra Empty_set Empty_set_cmra_mixin.
Global Instance Empty_set_cmra_discrete : CmraDiscrete Empty_setR.
Proof. done. Qed.
......@@ -1103,16 +1170,16 @@ End empty.
(** ** Product *)
Section prod.
Context {A B : cmraT}.
Context {SI : sidx} {A B : cmra}.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_/.
Instance prod_op : Op (A * B) := λ x y, (x.1 y.1, x.2 y.2).
Instance prod_pcore : PCore (A * B) := λ x,
Local Instance prod_op_instance : Op (A * B) := λ x y, (x.1 y.1, x.2 y.2).
Local Instance prod_pcore_instance : PCore (A * B) := λ x,
c1 pcore (x.1); c2 pcore (x.2); Some (c1, c2).
Arguments prod_pcore !_ /.
Instance prod_valid : Valid (A * B) := λ x, x.1 x.2.
Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1 {n} x.2.
Local Arguments prod_pcore_instance !_ /.
Local Instance prod_valid_instance : Valid (A * B) := λ x, x.1 x.2.
Local Instance prod_validN_instance : ValidN (A * B) := λ n x, {n} x.1 {n} x.2.
Lemma prod_pcore_Some (x cx : A * B) :
pcore x = Some cx pcore (x.1) = Some (cx.1) pcore (x.2) = Some (cx.2).
......@@ -1120,8 +1187,8 @@ Section prod.
Lemma prod_pcore_Some' (x cx : A * B) :
pcore x Some cx pcore (x.1) Some (cx.1) pcore (x.2) Some (cx.2).
Proof.
split; [by intros (cx'&[-> ->]%prod_pcore_Some&->)%equiv_Some_inv_r'|].
rewrite {3}/pcore /prod_pcore. (* TODO: use setoid rewrite *)
split; [by intros (cx'&[-> ->]%prod_pcore_Some&<-)%Some_equiv_eq|].
rewrite {3}/pcore /prod_pcore_instance. (* TODO: use setoid rewrite *)
intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
by constructor.
Qed.
......@@ -1149,7 +1216,7 @@ Section prod.
- intros x; split.
+ intros [??] n; split; by apply cmra_valid_validN.
+ intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
- by intros n x [??]; split; apply cmra_validN_S.
- intros n m x [??]; split; by eapply cmra_validN_le.
- by split; rewrite /= assoc.
- by split; rewrite /= comm.
- intros x y [??]%prod_pcore_Some;
......@@ -1166,7 +1233,7 @@ Section prod.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
by exists (z11,z21), (z12,z22).
Qed.
Canonical Structure prodR := CmraT (prod A B) prod_cmra_mixin.
Canonical Structure prodR := Cmra (prod A B) prod_cmra_mixin.
Lemma pair_op (a a' : A) (b b' : B) : (a a', b b') = (a, b) (a', b').
Proof. done. Qed.
......@@ -1216,21 +1283,21 @@ Section prod.
Proof. intros ???[][][][]. constructor; simpl in *; by eapply cancelableN. Qed.
Global Instance pair_id_free_l x y : IdFree x IdFree (x,y).
Proof. move=>? [??] [? _] [/=? _]. eauto. Qed.
Proof. move=> Hx [a b] [? _] [/=? _]. apply (Hx a); eauto. Qed.
Global Instance pair_id_free_r x y : IdFree y IdFree (x,y).
Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
Proof. move=> Hy [a b] [_ ?] [_ /=?]. apply (Hy b); eauto. Qed.
End prod.
(* Registering as [Hint Extern] with new unification. *)
Global Hint Extern 4 (CoreId _) =>
notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
Arguments prodR : clear implicits.
Global Arguments prodR {_} _ _.
Section prod_unit.
Context {A B : ucmraT}.
Context {SI : sidx} {A B : ucmra}.
Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
Local Instance prod_unit_instance `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
Lemma prod_ucmra_mixin : UcmraMixin (A * B).
Proof.
split.
......@@ -1238,7 +1305,7 @@ Section prod_unit.
- by split; rewrite /=left_id.
- rewrite prod_pcore_Some'; split; apply (core_id _).
Qed.
Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
Canonical Structure prodUR := Ucmra (prod A B) prod_ucmra_mixin.
Lemma pair_split (a : A) (b : B) : (a, b) (a, ε) (ε, b).
Proof. by rewrite -pair_op left_id right_id. Qed.
......@@ -1262,39 +1329,40 @@ Section prod_unit.
Proof. unfold_leibniz. apply pair_op_2. Qed.
End prod_unit.
Arguments prodUR : clear implicits.
Global Arguments prodUR {_} _ _.
Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A A') (g : B B') :
Global Instance prod_map_cmra_morphism
{SI : sidx} {A A' B B' : cmra} (f : A A') (g : B B') :
CmraMorphism f CmraMorphism g CmraMorphism (prod_map f g).
Proof.
split; first apply _.
- by intros n x [??]; split; simpl; apply cmra_morphism_validN.
- intros x. etrans; last apply (reflexivity (mbind _ _)).
etrans; first apply (reflexivity (_ <$> mbind _ _)). simpl.
assert (Hf := cmra_morphism_pcore f (x.1)).
destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=.
assert (Hg := cmra_morphism_pcore g (x.2)).
destruct (pcore (g (x.2))), (pcore (x.2)); inversion_clear Hg=>//=.
- intros [x1 x2]. rewrite /= !pair_pcore /=.
pose proof (Hf := cmra_morphism_pcore f (x1)).
destruct (pcore (f (x1))), (pcore (x1)); inv Hf=>//=.
pose proof (Hg := cmra_morphism_pcore g (x2)).
destruct (pcore (g (x2))), (pcore (x2)); inv Hg=>//=.
by setoid_subst.
- intros. by rewrite /prod_map /= !cmra_morphism_op.
Qed.
Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
Program Definition prodRF {SI : sidx} (F1 F2 : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_map_ne.
intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
by apply prodO_map_ne; apply rFunctor_map_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !rFunctor_map_compose.
Qed.
Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
Instance prodRF_contractive F1 F2 :
Global Instance prodRF_contractive {SI : sidx} F1 F2 :
rFunctorContractive F1 rFunctorContractive F2
rFunctorContractive (prodRF F1 F2).
Proof.
......@@ -1302,22 +1370,23 @@ Proof.
by apply prodO_map_ne; apply rFunctor_map_contractive.
Qed.
Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
Program Definition prodURF {SI : sidx} (F1 F2 : urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_map_ne.
intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
by apply prodO_map_ne; apply urFunctor_map_ne.
Qed.
Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
by rewrite !urFunctor_map_compose.
Qed.
Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
Instance prodURF_contractive F1 F2 :
Global Instance prodURF_contractive {SI : sidx} F1 F2 :
urFunctorContractive F1 urFunctorContractive F2
urFunctorContractive (prodURF F1 F2).
Proof.
......@@ -1327,25 +1396,29 @@ Qed.
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
Context {SI : sidx} {A : cmra}.
Implicit Types a b : A.
Implicit Types ma mb : option A.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
Instance option_valid : Valid (option A) := λ ma,
Local Instance option_valid_instance : Valid (option A) := λ ma,
match ma with Some a => a | None => True end.
Instance option_validN : ValidN (option A) := λ n ma,
Local Instance option_validN_instance : ValidN (option A) := λ n ma,
match ma with Some a => {n} a | None => True end.
Instance option_pcore : PCore (option A) := λ ma, Some (ma ≫= pcore).
Arguments option_pcore !_ /.
Instance option_op : Op (option A) := union_with (λ a b, Some (a b)).
Local Instance option_pcore_instance : PCore (option A) := λ ma,
Some (ma ≫= pcore).
Local Arguments option_pcore_instance !_ /.
Local Instance option_op_instance : Op (option A) :=
union_with (λ a b, Some (a b)).
Definition Some_valid a : Some a a := reflexivity _.
Definition Some_validN a n : {n} Some a {n} a := reflexivity _.
Definition Some_op a b : Some (a b) = Some a Some b := eq_refl.
Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
Lemma Some_core `{!CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Lemma pcore_Some a : pcore (Some a) = Some (pcore a).
Proof. done. Qed.
Lemma Some_op_opM a ma : Some a ma = Some (a ? ma).
Proof. by destruct ma. Qed.
......@@ -1357,7 +1430,7 @@ Section option.
destruct ma as [a|]; [right|by left].
destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
setoid_subst; eauto using cmra_included_l.
setoid_subst; eauto.
- intros [->|(a&b&->&->&[Hc|[c Hc]])].
+ exists mb. by destruct mb.
+ exists None; by constructor.
......@@ -1372,7 +1445,8 @@ Section option.
Qed.
Lemma option_includedN n ma mb :
ma {n} mb ma = None x y, ma = Some x mb = Some y (x {n} y x {n} y).
ma {n} mb ma = None
x y, ma = Some x mb = Some y (x {n} y x {n} y).
Proof.
split.
- intros [mc Hmc].
......@@ -1393,15 +1467,18 @@ Section option.
right. exists a, b. by rewrite {3}Hab.
Qed.
(* See below for more [included] lemmas. *)
Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
apply cmra_total_mixin.
- eauto.
- by intros [a|] n; destruct 1; constructor; ofe_subst.
- destruct 1; by ofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; ofe_subst.
- by destruct 1; rewrite /validN /option_validN_instance //=; ofe_subst.
- intros [a|]; [apply cmra_valid_validN|done].
- intros n [a|]; unfold validN, option_validN; eauto using cmra_validN_S.
- intros n m [a|];
unfold validN, option_validN_instance; eauto using cmra_validN_le.
- intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
- intros [a|] [b|]; constructor; rewrite 1?comm; auto.
- intros [a|]; simpl; auto.
......@@ -1414,7 +1491,7 @@ Section option.
destruct (cmra_pcore_proper a b ca) as (?&?&?); eauto 10.
+ destruct (pcore a) as [ca|] eqn:?; eauto.
destruct (cmra_pcore_mono a b ca) as (?&?&?); eauto 10.
- intros n [a|] [b|]; rewrite /validN /option_validN /=;
- intros n [a|] [b|]; rewrite /validN /option_validN_instance /=;
eauto using cmra_validN_op_l.
- intros n ma mb1 mb2.
destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
......@@ -1425,15 +1502,15 @@ Section option.
+ by exists None, (Some a); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
Canonical Structure optionR := CmraT (option A) option_cmra_mixin.
Canonical Structure optionR := Cmra (option A) option_cmra_mixin.
Global Instance option_cmra_discrete : CmraDiscrete A CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
Instance option_unit : Unit (option A) := None.
Local Instance option_unit_instance : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
Proof. split; [done| |done]. by intros []. Qed.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.
(** Misc *)
Lemma op_None ma mb : ma mb = None ma = None mb = None.
......@@ -1449,12 +1526,16 @@ Section option.
Lemma cmra_opM_opM_assoc a mb mc : a ? mb ? mc a ? (mb mc).
Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc : a ? mb ? mc = a ? (mb mc).
Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc :
a ? mb ? mc = a ? (mb mc).
Proof. unfold_leibniz. apply cmra_opM_opM_assoc. Qed.
Lemma cmra_opM_opM_swap a mb mc : a ? mb ? mc a ? mc ? mb.
Proof. by rewrite !cmra_opM_opM_assoc (comm _ mb). Qed.
Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc : a ? mb ? mc = a ? mc ? mb.
Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc :
a ? mb ? mc = a ? mc ? mb.
Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.
Lemma cmra_opM_fmap_Some ma1 ma2 : ma1 ? (Some <$> ma2) = ma1 ma2.
Proof. by destruct ma1, ma2. Qed.
Global Instance Some_core_id a : CoreId a CoreId (Some a).
Proof. by constructor. Qed.
......@@ -1475,14 +1556,47 @@ Section option.
Lemma Some_includedN n a b : Some a {n} Some b a {n} b a {n} b.
Proof. rewrite option_includedN; naive_solver. Qed.
Lemma Some_includedN_1 n a b : Some a {n} Some b a {n} b a {n} b.
Proof. rewrite Some_includedN. auto. Qed.
Lemma Some_includedN_2 n a b : a {n} b a {n} b Some a {n} Some b.
Proof. rewrite Some_includedN. auto. Qed.
Lemma Some_includedN_mono n a b : a {n} b Some a {n} Some b.
Proof. rewrite Some_includedN. auto. Qed.
Lemma Some_includedN_refl n a b : a {n} b Some a {n} Some b.
Proof. rewrite Some_includedN. auto. Qed.
Lemma Some_includedN_is_Some n x mb : Some x {n} mb is_Some mb.
Proof. rewrite option_includedN. naive_solver. Qed.
Lemma Some_included a b : Some a Some b a b a b.
Proof. rewrite option_included; naive_solver. Qed.
Lemma Some_included_2 a b : a b Some a Some b.
Proof. rewrite Some_included; eauto. Qed.
Lemma Some_included_1 a b : Some a Some b a b a b.
Proof. rewrite Some_included. auto. Qed.
Lemma Some_included_2 a b : a b a b Some a Some b.
Proof. rewrite Some_included. auto. Qed.
Lemma Some_included_mono a b : a b Some a Some b.
Proof. rewrite Some_included. auto. Qed.
Lemma Some_included_refl a b : a b Some a Some b.
Proof. rewrite Some_included. auto. Qed.
Lemma Some_included_is_Some x mb : Some x mb is_Some mb.
Proof. rewrite option_included. naive_solver. Qed.
Lemma Some_includedN_opM n a b : Some a {n} Some b mc, b {n} a ? mc.
Proof.
rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
Qed.
Lemma Some_included_opM a b : Some a Some b mc, b a ? mc.
Proof.
rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
Qed.
Lemma cmra_validN_Some_includedN n a b : {n} a Some b {n} Some a {n} b.
Proof. apply: (cmra_validN_includedN _ (Some _) (Some _)). Qed.
Lemma cmra_valid_Some_included a b : a Some b Some a b.
Proof. apply: (cmra_valid_included (Some _) (Some _)). Qed.
Lemma Some_includedN_total `{CmraTotal A} n a b : Some a {n} Some b a {n} b.
Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a {n} Some b a {n} b.
Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
Lemma Some_included_total `{CmraTotal A} a b : Some a Some b a b.
Lemma Some_included_total `{!CmraTotal A} a b : Some a Some b a b.
Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
......@@ -1502,10 +1616,10 @@ Section option.
Proof.
intros Hirr ? n [b|] [c|] ? EQ; inversion_clear EQ.
- constructor. by apply (cancelableN a).
- destruct (Hirr b); [|eauto using dist_le with lia].
by eapply (cmra_validN_op_l 0 a b), (cmra_validN_le n); last lia.
- destruct (Hirr c); [|symmetry; eauto using dist_le with lia].
by eapply (cmra_validN_le n); last lia.
- destruct (Hirr b); [|eauto using dist_le, SIdx.le_0_l].
by eapply (cmra_validN_op_l 0 a b), (cmra_validN_le n), SIdx.le_0_l.
- destruct (Hirr c); [|symmetry; eauto using dist_le, SIdx.le_0_l].
by eapply (cmra_validN_le n), SIdx.le_0_l.
- done.
Qed.
......@@ -1514,36 +1628,48 @@ Section option.
Proof. destruct ma; apply _. Qed.
End option.
Arguments optionR : clear implicits.
Arguments optionUR : clear implicits.
Global Arguments optionR {_} _.
Global Arguments optionUR {_} _.
Section option_prod.
Context {A B : cmraT}.
Context {SI : sidx} {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
Lemma Some_pair_includedN n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) Some a1 {n} Some a2 Some b1 {n} Some b2.
Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.
Lemma Some_pair_includedN_total_1 `{CmraTotal A} n a1 a2 b1 b2 :
Lemma Some_pair_includedN_l n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) Some a1 {n} Some a2.
Proof. intros. eapply Some_pair_includedN. done. Qed.
Lemma Some_pair_includedN_r n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) Some b1 {n} Some b2.
Proof. intros. eapply Some_pair_includedN. done. Qed.
Lemma Some_pair_includedN_total_1 `{!CmraTotal A} n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) a1 {n} a2 Some b1 {n} Some b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ a1). Qed.
Lemma Some_pair_includedN_total_2 `{CmraTotal B} n a1 a2 b1 b2 :
Lemma Some_pair_includedN_total_2 `{!CmraTotal B} n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) Some a1 {n} Some a2 b1 {n} b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ b1). Qed.
Lemma Some_pair_included a1 a2 b1 b2 :
Some (a1,b1) Some (a2,b2) Some a1 Some a2 Some b1 Some b2.
Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
Lemma Some_pair_included_total_1 `{CmraTotal A} a1 a2 b1 b2 :
Lemma Some_pair_included_l a1 a2 b1 b2 :
Some (a1,b1) Some (a2,b2) Some a1 Some a2.
Proof. intros. eapply Some_pair_included. done. Qed.
Lemma Some_pair_included_r a1 a2 b1 b2 :
Some (a1,b1) Some (a2,b2) Some b1 Some b2.
Proof. intros. eapply Some_pair_included. done. Qed.
Lemma Some_pair_included_total_1 `{!CmraTotal A} a1 a2 b1 b2 :
Some (a1,b1) Some (a2,b2) a1 a2 Some b1 Some b2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total a1). Qed.
Lemma Some_pair_included_total_2 `{CmraTotal B} a1 a2 b1 b2 :
Lemma Some_pair_included_total_2 `{!CmraTotal B} a1 a2 b1 b2 :
Some (a1,b1) Some (a2,b2) Some a1 Some a2 b1 b2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
End option_prod.
Lemma option_fmap_mono {A B : cmraT} (f : A B) ma mb :
Lemma option_fmap_mono {SI : sidx} {A B : cmra} (f : A B) (ma mb : option A) :
Proper (() ==> ()) f
( a b, a b f a f b)
ma mb f <$> ma f <$> mb.
......@@ -1551,7 +1677,8 @@ Proof.
intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.
Instance option_fmap_cmra_morphism {A B : cmraT} (f: A B) `{!CmraMorphism f} :
Global Instance option_fmap_cmra_morphism {SI : sidx}
{A B : cmra} (f: A B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A option B).
Proof.
split; first apply _.
......@@ -1560,55 +1687,65 @@ Proof.
- move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
Qed.
Program Definition optionURF (F : rFunctor) : urFunctor := {|
Program Definition optionURF {SI : sidx} (F : rFunctor) : urFunctor := {|
urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
by apply optionO_map_ne, rFunctor_map_ne.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
intros ? F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
rewrite /= -option_fmap_compose.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
Qed.
Instance optionURF_contractive F :
Global Instance optionURF_contractive {SI : sidx} F :
rFunctorContractive F urFunctorContractive (optionURF F).
Proof.
by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
by apply optionO_map_ne, rFunctor_map_contractive.
Qed.
Program Definition optionRF (F : rFunctor) : rFunctor := {|
Program Definition optionRF {SI : sidx} (F : rFunctor) : rFunctor := {|
rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Solve Obligations with apply optionURF.
Solve Obligations with apply @optionURF.
Instance optionRF_contractive F :
Global Instance optionRF_contractive {SI : sidx} F :
rFunctorContractive F rFunctorContractive (optionRF F).
Proof. apply optionURF_contractive. Qed.
(* Dependently-typed functions over a discrete domain *)
Section discrete_fun_cmra.
Context `{B : A ucmraT}.
Context {SI : sidx} {A: Type} {B : A ucmra}.
Implicit Types f g : discrete_fun B.
Instance discrete_fun_op : Op (discrete_fun B) := λ f g x, f x g x.
Instance discrete_fun_pcore : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
Instance discrete_fun_valid : Valid (discrete_fun B) := λ f, x, f x.
Instance discrete_fun_validN : ValidN (discrete_fun B) := λ n f, x, {n} f x.
Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x,
f x g x.
Local Instance discrete_fun_pcore_instance : PCore (discrete_fun B) := λ f,
Some (λ x, core (f x)).
Local Instance discrete_fun_valid_instance : Valid (discrete_fun B) := λ f,
x, f x.
Local Instance discrete_fun_validN_instance : ValidN (discrete_fun B) := λ n f,
x, {n} f x.
Definition discrete_fun_lookup_op f g x : (f g) x = f x g x := eq_refl.
Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
Lemma discrete_fun_included_spec_1 (f g : discrete_fun B) x : f g f x g x.
Proof. by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op (Hh x). Qed.
Proof.
by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
Qed.
Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) : f g x, f x g x.
Lemma discrete_fun_included_spec `{Finite A} (f g : discrete_fun B) :
f g x, f x g x.
Proof.
split; [by intros; apply discrete_fun_included_spec_1|].
intros [h ?]%finite_choice; by exists h.
......@@ -1618,160 +1755,254 @@ Section discrete_fun_cmra.
Proof.
apply cmra_total_mixin.
- eauto.
- by intros n f1 f2 f3 Hf x; rewrite discrete_fun_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite discrete_fun_lookup_core (Hf x).
- by intros n f1 f2 Hf ? x; rewrite -(Hf x).
- intros n f1 f2 f3 Hf x. by rewrite discrete_fun_lookup_op (Hf x).
- intros n f1 f2 Hf x. by rewrite discrete_fun_lookup_core (Hf x).
- intros n f1 f2 Hf ? x. by rewrite -(Hf x).
- intros g; split.
+ intros Hg n i; apply cmra_valid_validN, Hg.
+ intros Hg i; apply cmra_valid_validN=> n; apply Hg.
- intros n f Hf x; apply cmra_validN_S, Hf.
- by intros f1 f2 f3 x; rewrite discrete_fun_lookup_op assoc.
- by intros f1 f2 x; rewrite discrete_fun_lookup_op comm.
- by intros f x; rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
- by intros f x; rewrite discrete_fun_lookup_core cmra_core_idemp.
- intros n n' f Hf ? x. eauto using cmra_validN_le.
- intros f1 f2 f3 x. by rewrite discrete_fun_lookup_op assoc.
- intros f1 f2 x. by rewrite discrete_fun_lookup_op comm.
- intros f x.
by rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
- intros f x. by rewrite discrete_fun_lookup_core cmra_core_idemp.
- intros f1 f2 Hf12. exists (core f2)=>x. rewrite discrete_fun_lookup_op.
apply (discrete_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
rewrite !discrete_fun_lookup_core. destruct Hf12 as [? ->].
rewrite assoc -cmra_core_dup //.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f1 f2 Hf x. apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))).
split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
by destruct (FUN x) as (?&?&?&?&?).
by destruct (FUN x) as (?&?&?&?&?).
Qed.
Canonical Structure discrete_funR := CmraT (discrete_fun B) discrete_fun_cmra_mixin.
Canonical Structure discrete_funR :=
Cmra (discrete_fun B) discrete_fun_cmra_mixin.
Instance discrete_fun_unit : Unit (discrete_fun B) := λ x, ε.
Local Instance discrete_fun_unit_instance : Unit (discrete_fun B) := λ x, ε.
Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
Proof.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite discrete_fun_lookup_op left_id.
- intros x. apply ucmra_unit_valid.
- intros f x. by rewrite discrete_fun_lookup_op left_id.
- constructor=> x. apply core_id_core, _.
Qed.
Canonical Structure discrete_funUR := UcmraT (discrete_fun B) discrete_fun_ucmra_mixin.
Canonical Structure discrete_funUR :=
Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
Global Instance discrete_fun_unit_discrete :
( i, Discrete (ε : B i)) Discrete (ε : discrete_fun B).
Proof. intros ? f Hf x. by apply: discrete. Qed.
End discrete_fun_cmra.
Arguments discrete_funR {_} _.
Arguments discrete_funUR {_} _.
Global Arguments discrete_funR {_ _} _.
Global Arguments discrete_funUR {_ _} _.
Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A ucmraT} (f : x, B1 x B2 x) :
Global Instance discrete_fun_map_cmra_morphism
{SI : sidx} {A} {B1 B2 : A ucmra} (f : x, B1 x B2 x) :
( x, CmraMorphism (f x)) CmraMorphism (discrete_fun_map f).
Proof.
split; first apply _.
- intros n g Hg x; rewrite /discrete_fun_map; apply (cmra_morphism_validN (f _)), Hg.
- intros n g Hg x. rewrite /discrete_fun_map.
apply (cmra_morphism_validN (f _)), Hg.
- intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
- intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
- intros g1 g2 i.
by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed.
Program Definition discrete_funURF {C} (F : C urFunctor) : urFunctor := {|
Program Definition discrete_funURF
{SI : sidx} {C} (F : C urFunctor) : urFunctor := {|
urFunctor_car A _ B _ := discrete_funUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
discrete_funO_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
intros ? C F A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
Qed.
Next Obligation.
intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
intros ? C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
apply discrete_fun_map_ext=> y; apply urFunctor_map_id.
Qed.
Next Obligation.
intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
intros ? C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g.
rewrite /=-discrete_fun_map_compose.
apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
Qed.
Instance discrete_funURF_contractive {C} (F : C urFunctor) :
Global Instance discrete_funURF_contractive {SI : sidx} {C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (discrete_funURF F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
by apply discrete_funO_map_ne=> c; apply urFunctor_map_contractive.
Qed.
(** * Constructing a camera [B] through a bijection with [A] that
is mostly an isomorphism but restricts validity. *)
Lemma iso_cmra_mixin_restrict {A : cmraT} {B : Type}
`{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(f : A B) (g : B A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
(g_equiv : y1 y2, y1 y2 g y1 g y2)
(** * Constructing a camera [B] through a mapping into [A]
The mapping may restrict the domain (i.e., we have an injection from [B] to [A],
not a bijection) and validity. These two restrictions work on opposite "ends" of
[A] according to [≼]: domain restriction must prove that when an element is in
the domain, so is its composition with other elements; validity restriction must
prove that if the composition of two elements is valid, then so are both of the
elements. The "domain" is the image of [g] in [A], or equivalently the part of
[A] where [f] returns [Some]. *)
Lemma inj_cmra_mixin_restrict_validity {SI : sidx} {A : cmra} {B : ofe}
`{!PCore B, !Op B, !Valid B, !ValidN B}
(f : A option B) (g : B A)
(* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
(g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2)
(* [g] is surjective (and [f] its inverse) *)
(gf : x, g (f x) x)
(* [g] commutes with [pcore] and [op] *)
(g_pcore : y, pcore (g y) g <$> pcore y)
(g_op : y1 y2, g (y1 y2) g y1 g y2)
(* [g] is surjective into the part of [A] where [is_Some ∘ f] holds
(and [f] its inverse) *)
(gf_dist : (x : A) (y : B) n, f x {n} Some y g y {n} x)
(* [g] commutes with [pcore] (on the part where it is defined) and [op] *)
(g_pcore_dist : (y cy : B) n,
pcore y {n} Some cy pcore (g y) {n} Some (g cy))
(g_op : (y1 y2 : B), g (y1 y2) g y1 g y2)
(* [g] also commutes with [opM] when the right-hand side is produced by [f],
and cancels the [f]. In particular this axiom implies that when taking an
element in the domain ([g y]), its composition with *any* [x : A] is still in
the domain, and [f] computes the preimage properly.
Note that just requiring "the composition of two elements from the domain
is in the domain" is insufficient for this lemma to hold. [g_op] already shows
that this is the case, but the issue is that in [pcore_mono] we obtain a
[g y1 ≼ g y2], and the existentially quantified "remainder" in the [≼] has no
reason to be in the domain, so [g_op] is too weak to turn this into some
relation between [y1] and [y2] in [B]. At the same time, [g_opM_f] does not
impl [g_op] since we need [g_op] to prove that [⋅] in [B] respects [≡].
Therefore both [g_op] and [g_opM_f] are required for this lemma to work. *)
(g_opM_f : (x : A) (y : B), g (y ? f x) g y x)
(* The validity predicate on [B] restricts the one on [A] *)
(g_validN : n y, {n} y {n} (g y))
(g_validN : n (y : B), {n} y {n} (g y))
(* The validity predicate on [B] satisfies the laws of validity *)
(valid_validN_ne : n, Proper (dist n ==> impl) (validN (A:=B) n))
(valid_rvalidN : y : B, y n, {n} y)
(validN_S : n (y : B), {S n} y {n} y)
(validN_le : n n' (y : B), {n} y n' n {n'} y)
(validN_op_l : n (y1 y2 : B), {n} (y1 y2) {n} y1) :
CmraMixin B.
Proof.
(* Some general derived facts that will be useful later. *)
assert (g_equiv : y1 y2, y1 y2 g y1 g y2).
{ intros ??. rewrite !equiv_dist. naive_solver. }
assert (g_pcore : (y cy : B),
pcore y Some cy pcore (g y) Some (g cy)).
{ intros. rewrite !equiv_dist. naive_solver. }
assert (gf : x y, f x Some y g y x).
{ intros. rewrite !equiv_dist. naive_solver. }
assert (fg : y, f (g y) Some y).
{ intros. apply gf. done. }
assert (g_ne : NonExpansive g).
{ intros n ???. apply g_dist. done. }
(* Some of the CMRA properties are useful in proving the others. *)
assert (b_pcore_l' : y cy : B, pcore y Some cy cy y y).
{ intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
apply g_pcore. done. }
assert (b_pcore_idemp : y cy : B, pcore y Some cy pcore cy Some cy).
{ intros y cy Hy. eapply g_pcore, cmra_pcore_idemp', g_pcore. done. }
(* Now prove all the mixin laws. *)
split.
- intros y n z1 z2 Hz%g_dist. apply g_dist. by rewrite !g_op Hz.
- intros n y1 y2 cy Hy%g_dist Hy1.
assert (g <$> pcore y2 {n} Some (g cy))
as (cx&(cy'&->&->)%fmap_Some_1&?%g_dist)%dist_Some_inv_r'; [|by eauto].
by rewrite -g_pcore -Hy g_pcore Hy1.
as (cx & (cy'&->&->)%fmap_Some_1 & ?%g_dist)%dist_Some_inv_r'; [|by eauto].
assert (Hgcy : pcore (g y1) Some (g cy)).
{ apply g_pcore. rewrite Hy1. done. }
rewrite equiv_dist in Hgcy. specialize (Hgcy n).
rewrite Hy in Hgcy. apply g_pcore_dist in Hgcy. rewrite Hgcy. done.
- done.
- done.
- done.
- intros y1 y2 y3. apply g_equiv. by rewrite !g_op assoc.
- intros y1 y2. apply g_equiv. by rewrite !g_op comm.
- intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
by rewrite g_pcore Hy.
- intros y cy Hy.
assert (g <$> pcore cy Some (g cy)) as (cy'&->&?)%fmap_Some_equiv.
{ rewrite -g_pcore.
apply cmra_pcore_idemp' with (g y). by rewrite g_pcore Hy. }
constructor. by apply g_equiv.
- intros y cy Hcy. apply b_pcore_l'. by rewrite Hcy.
- intros y cy Hcy. eapply b_pcore_idemp. by rewrite -Hcy.
- intros y1 y2 cy [z Hy2] Hy1.
destruct (cmra_pcore_mono' (g y1) (g y2) (g cy)) as (cx&Hcgy2&[x Hcx]).
{ exists (g z). rewrite -g_op. by apply g_equiv. }
{ by rewrite g_pcore Hy1. }
assert (g <$> pcore y2 Some cx) as (cy'&->&?)%fmap_Some_equiv.
{ by rewrite -g_pcore Hcgy2. }
exists cy'; split; [done|].
exists (f x). apply g_equiv. by rewrite g_op gf -Hcx.
{ apply g_pcore. rewrite Hy1 //. }
apply (reflexive_eq (R:=equiv)) in Hcgy2.
rewrite -g_opM_f in Hcx. rewrite Hcx in Hcgy2.
apply g_pcore in Hcgy2.
apply Some_equiv_eq in Hcgy2 as [cy' [-> Hcy']].
eexists. split; first done.
destruct (f x) as [y|].
+ exists y. done.
+ exists cy. apply (reflexive_eq (R:=equiv)), b_pcore_idemp, b_pcore_l' in Hy1.
rewrite Hy1 //.
- done.
- intros n y z1 z2 ?%g_validN ?.
destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&?&?).
destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&Hx1&Hx2).
{ done. }
{ rewrite -g_op. by apply g_dist. }
exists (f x1), (f x2). split_and!.
+ apply g_equiv. by rewrite Hgy g_op !gf.
+ apply g_dist. by rewrite gf.
+ apply g_dist. by rewrite gf.
symmetry in Hx1, Hx2.
apply gf_dist in Hx1, Hx2.
destruct (f x1) as [y1|] eqn:Hy1; last first.
{ exfalso. inversion Hx1. }
destruct (f x2) as [y2|] eqn:Hy2; last first.
{ exfalso. inversion Hx2. }
exists y1, y2. split_and!.
+ apply g_equiv. rewrite Hgy g_op.
f_equiv; symmetry; apply gf; rewrite ?Hy1 ?Hy2 //.
+ apply g_dist. apply (inj Some) in Hx1. rewrite Hx1 //.
+ apply g_dist. apply (inj Some) in Hx2. rewrite Hx2 //.
Qed.
(** * Constructing a camera through an isomorphism *)
Lemma iso_cmra_mixin {A : cmraT} {B : Type}
`{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(** Constructing a CMRA through an isomorphism that may restrict validity. *)
Lemma iso_cmra_mixin_restrict_validity {SI : sidx} {A : cmra} {B : ofe}
`{!PCore B, !Op B, !Valid B, !ValidN B}
(f : A B) (g : B A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
(g_equiv : y1 y2, y1 y2 g y1 g y2)
(g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2)
(* [g] is surjective (and [f] its inverse) *)
(gf : x, g (f x) x)
(gf : x : A, g (f x) x)
(* [g] commutes with [pcore] and [op] *)
(g_pcore : y : B, pcore (g y) g <$> pcore y)
(g_op : y1 y2, g (y1 y2) g y1 g y2)
(* The validity predicate on [B] restricts the one on [A] *)
(g_validN : n y, {n} y {n} (g y))
(* The validity predicate on [B] satisfies the laws of validity *)
(valid_validN_ne : n, Proper (dist n ==> impl) (validN (A:=B) n))
(valid_rvalidN : y : B, y n, {n} y)
(validN_le: n m (y : B), {n} y m n {m} y)
(validN_op_l : n (y1 y2 : B), {n} (y1 y2) {n} y1) :
CmraMixin B.
Proof.
assert (g_ne : NonExpansive g).
{ intros n ???. apply g_dist. done. }
assert (g_equiv : y1 y2, y1 y2 g y1 g y2).
{ intros ??.
split; intros ?; apply equiv_dist; intros; apply g_dist, equiv_dist; done. }
apply (inj_cmra_mixin_restrict_validity (λ x, Some (f x)) g); try done.
- intros. split.
+ intros Hy%(inj Some). rewrite -Hy gf //.
+ intros ?. f_equiv. apply g_dist. rewrite gf. done.
- intros. rewrite g_pcore. split.
+ intros ->. done.
+ intros (? & -> & ->%g_dist)%fmap_Some_dist. done.
- intros ??. simpl. rewrite g_op gf //.
Qed.
(** * Constructing a camera through an isomorphism *)
Lemma iso_cmra_mixin {SI : sidx} {A : cmra} {B : ofe}
`{!PCore B, !Op B, !Valid B, !ValidN B}
(f : A B) (g : B A)
(* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
(g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2)
(* [g] is surjective (and [f] its inverse) *)
(gf : x : A, g (f x) x)
(* [g] commutes with [pcore], [op], [valid], and [validN] *)
(g_pcore : y, pcore (g y) g <$> pcore y)
(g_pcore : y : B, pcore (g y) g <$> pcore y)
(g_op : y1 y2, g (y1 y2) g y1 g y2)
(g_valid : y, (g y) y)
(g_validN : n y, {n} (g y) {n} y) :
CmraMixin B.
Proof.
apply (iso_cmra_mixin_restrict f g); auto.
apply (iso_cmra_mixin_restrict_validity f g); auto.
- by intros n y ?%g_validN.
- intros n y1 y2 Hy%g_dist Hy1. by rewrite -g_validN -Hy g_validN.
- intros y. rewrite -g_valid cmra_valid_validN. naive_solver.
- intros n y. rewrite -!g_validN. apply cmra_validN_S.
- intros n m y. rewrite -!g_validN. apply cmra_validN_le.
- intros n y1 y2. rewrite -!g_validN g_op. apply cmra_validN_op_l.
Qed.