diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 95e7913279fc7fa5410f355c2a1d30f96e4c11b1..b37f02c6995efed239caf8b7cf94e2323d52afc1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -3,6 +3,7 @@ image: ralfjung/opam-ci:latest
stages:
- build
- deploy
+ - build_more
variables:
CPU_CORES: "9"
@@ -19,7 +20,6 @@ variables:
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
cache:
key: "$CI_JOB_NAME"
paths:
@@ -52,6 +52,7 @@ reverse-deps:
build-coq.8.7.dev:
<<: *template
+ stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev coq-mathcomp-ssreflect version dev"
except:
@@ -68,7 +69,6 @@ build-coq.8.6.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.4"
- VALIDATE: "1"
artifacts:
paths:
- build-time.txt
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 548ce8d50ec9ac2aa45205bac7d7bf99bf4ce83b..b06ef6950cbe9f28675d04f2a3fa9d7525b0c282 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
-* [#] Add new modality: â– ("plainly").
+* Add new modality: â– ("plainly").
* Camera morphisms have to be homomorphisms, not just monotone functions.
* Add a proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates
diff --git a/_CoqProject b/_CoqProject
index 61631c3ee3821c3c999004ff91d41579c2682a2b..13c296354ff16a778c455e79595df5e381685a62 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,7 +14,7 @@ theories/algebra/dra.v
theories/algebra/cofe_solver.v
theories/algebra/agree.v
theories/algebra/excl.v
-theories/algebra/iprod.v
+theories/algebra/functions.v
theories/algebra/frac.v
theories/algebra/csum.v
theories/algebra/list.v
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 9cfed25eaca982e31b347286ce1b1b4eabe61bd7..3ba0967042888774ba91ee1af53f50d672ba8acc 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -37,7 +37,8 @@ Elements that cannot be distinguished by programs within $n$ steps remain indist
The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.
\end{defn}
-Note that $\OFEs$ is cartesian closed. In particular:
+Note that $\OFEs$ is bicartesian closed, \ie it has all sums, products and exponentials as well as an initial and a terminal object.
+In particular:
\begin{defn}
Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with
\begin{align*}
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 93c0f58facf2107c768409563a5f75f017d237ce..2a45cae7cbd88a1fc94619caf86a6a06aadb95df 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -32,18 +32,25 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\begin{align*}
\type \bnfdef{}&
\sigtype \mid
+ 0 \mid
1 \mid
+ \type + \type \mid
\type \times \type \mid
\type \to \type
\\[0.4em]
\term, \prop, \pred \bnfdef{}&
\var \mid
\sigfn(\term_1, \dots, \term_n) \mid
+ \textlog{abort}\; \term \mid
() \mid
(\term, \term) \mid
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
\term(\term) \mid
+\\&
+ \textlog{inj}_i\; \term \mid
+ \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term \mid \Ret\textlog{inj}_2\; \var. \term \;\textlog{end} \mid
+%
\melt \mid
\mcore\term \mid
\term \mtimes \term \mid
@@ -63,12 +70,16 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
%\\&
\ownM{\term} \mid \mval(\term) \mid
\always\prop \mid
+ \plainly\prop \mid
{\later\prop} \mid
\upd \prop
\end{align*}
-Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
+Well-typedness forces recursive definitions to be \emph{guarded}:
+In $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
+Furthermore, the type of the definition must be \emph{complete}.
+The type $\Prop$ is complete, and if $\type$ is complete, then so is $\type' \to \type$.
-Note that the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
+Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
\paragraph{Variable conventions.}
@@ -105,7 +116,10 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
}{
\vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}}
}
-%%% products
+%%% empty, unit, products, sums
+\and
+ \infer{\vctx \proves \wtt\term{0}}
+ {\vctx \proves \wtt{\textlog{abort}\; \term}\type}
\and
\axiom{\vctx \proves \wtt{()}{1}}
\and
@@ -114,6 +128,14 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
+\and
+ \infer{\vctx \proves \wtt\term{\type_i} \and i \in \{1, 2\}}
+ {\vctx \proves \wtt{\textlog{inj}_i\;\term}{\type_1 + \type_2}}
+\and
+ \infer{\vctx \proves \wtt\term{\type_1 + \type_2} \and
+ \vctx, \var:\type_1 \proves \wtt{\term_1}\type \and
+ \vctx, \varB:\type_2 \proves \wtt{\term_2}\type}
+ {\vctx \proves \wtt{\textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term_1 \mid \Ret\textlog{inj}_2\; \varB. \term_2 \;\textlog{end}}{\type}}
%%% functions
\and
\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
@@ -124,7 +146,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
- \infer{}{\vctx \proves \wtt\munit{\textlog{M}}}
+ \infer{}{\vctx \proves \wtt\melt{\textlog{M}}}
\and
\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
\and
@@ -156,7 +178,8 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{
\vctx, \var:\type \proves \wtt{\term}{\type} \and
- \text{$\var$ is guarded in $\term$}
+ \text{$\var$ is guarded in $\term$} \and
+ \text{$\type$ is complete}
}{
\vctx \proves \wtt{\MU \var:\type. \term}{\type}
}
@@ -175,6 +198,9 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\always\prop}{\Prop}}
+\and
+ \infer{\vctx \proves \wtt{\prop}{\Prop}}
+ {\vctx \proves \wtt{\plainly\prop}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\later\prop}{\Prop}}
@@ -282,7 +308,7 @@ This is entirely standard.
% {}
% {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
-Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$.
+Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$.
\paragraph{Laws of (affine) bunched implications.}
@@ -303,7 +329,30 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\prop \proves \propB \wand \propC}
\end{mathpar}
-\paragraph{Laws for the always modality.}
+\paragraph{Laws for the plainness modality.}
+\begin{mathpar}
+\infer[$\plainly$-mono]
+ {\prop \proves \propB}
+ {\plainly{\prop} \proves \plainly{\propB}}
+\and
+\infer[$\plainly$-E]{}
+{\plainly\prop \proves \always\prop}
+\and
+\begin{array}[c]{rMcMl}
+ (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q) \\
+\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) &\proves& P =_{\Prop} Q
+\end{array}
+\and
+\begin{array}[c]{rMcMl}
+ \plainly{\prop} &\proves& \plainly\plainly\prop \\
+ \All x. \plainly{\prop} &\proves& \plainly{\All x. \prop} \\
+ \plainly{\Exists x. \prop} &\proves& \Exists x. \plainly{\prop}
+\end{array}
+%\and
+%\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
+\end{mathpar}
+
+\paragraph{Laws for the persistence modality.}
\begin{mathpar}
\infer[$\always$-mono]
{\prop \proves \propB}
@@ -313,8 +362,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\always\prop \proves \prop}
\and
\begin{array}[c]{rMcMl}
- \TRUE &\proves& \always{\TRUE} \\
- \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
+ (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB
\end{array}
\and
@@ -332,7 +380,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\prop \proves \propB}
{\later\prop \proves \later{\propB}}
\and
-\infer[L{\"o}b]
+\inferhref{L{\"o}b}{Loeb}
{}
{(\later\prop\Ra\prop) \proves \prop}
\and
@@ -344,7 +392,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\and
\begin{array}[c]{rMcMl}
\later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
- \always{\later\prop} &\provesIff& \later\always{\prop}
+ \always{\later\prop} &\provesIff& \later\always{\prop} \\
+ \plainly{\later\prop} &\provesIff& \later\plainly{\prop}
\end{array}
\end{mathpar}
@@ -393,6 +442,10 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\inferH{upd-update}
{\melt \mupd \meltsB}
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
+
+\inferH{upd-plainly}
+{}
+{\upd\plainly\prop \proves \prop}
\end{mathpar}
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
@@ -401,13 +454,14 @@ The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that h
The consistency statement of the logic reads as follows: For any $n$, we have
\begin{align*}
- \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)
+ \lnot(\TRUE \proves (\later)^n\spac\FALSE)
\end{align*}
-where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.
+where $(\later)^n$ is short for $\later$ being nested $n$ times.
The reason we want a stronger consistency than the usual $\lnot(\TRUE \proves \FALSE)$ is our modalities: it should be impossible to derive a contradiction below the modalities.
-For $\always$, this follows from the elimination rule, but the other two modalities do not have an elimination rule.
-Hence we declare that it is impossible to derive a contradiction below any combination of these two modalities.
+For $\always$ and $\plainly$, this follows from the elimination rules.
+For updates, we use the fact that $\upd\FALSE \proves \upd\plainly\FALSE \proves \FALSE$.
+However, there is no elimination rule for $\later$, so we declare that it is impossible to derive a contradiction below any number of laters.
%%% Local Variables:
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index d8cd9b8fa4d95d17197ec5a4dd8672854f2deede..bd10d54efa60000c9290d79789776440300a521a 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -35,8 +35,13 @@ We collect here some important and frequently used derived proof rules.
\infer{}
{\prop \proves \later\prop}
+
+ \infer{}
+ {\TRUE \proves \plainly\TRUE}
\end{mathparpagebreakable}
+Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from Löb induction, and $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
+
\subsection{Persistent assertions}
We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
These are assertions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic assertions.
diff --git a/docs/iris.sty b/docs/iris.sty
index aefb06027655b6d93f6be21c6fd354bcb02ab0b4..9ba0f619ee6025bb86dd090ac8e161017be62f73 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -260,6 +260,7 @@
\newcommand{\later}{\mathop{{\triangleright}}}
\newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
\newcommand{\always}{\mathop{\Box}}
+\newcommand{\plainly}{\mathop{\blacksquare}}
%% Invariants and Ghost ownership
% PDS: Was 0pt inner, 2pt outer.
diff --git a/docs/iris.tex b/docs/iris.tex
index 83d56c6d7aa6b9e1a67b75449110abedc0082149..dfe6a1dbc75fb3121ae453c90d5fc7b91579f9e3 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -16,7 +16,7 @@
\input{setup}
-\title{\bfseries The Iris 3.0 Documentation}
+\title{\bfseries The Iris 3.1 Documentation}
\author{\url{http://plv.mpi-sws.org/iris/}}
diff --git a/docs/model.tex b/docs/model.tex
index 4ea588ae82bffaf573ab6ea9777a34843d9a98fd..6100fb39be49d0689d410ad482466b1962b4a34e 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -9,11 +9,13 @@ The semantic domains are interpreted as follows:
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{\Prop} &\eqdef& \UPred(\monoid) \\
-\Sem{\textlog{M}} &\eqdef& \monoid
+\Sem{\textlog{M}} &\eqdef& \monoid \\
+\Sem{0} &\eqdef& \Delta \emptyset \\
+\Sem{1} &\eqdef& \Delta \{ () \}
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
-\Sem{1} &\eqdef& \Delta \{ () \} \\
+\Sem{\type + \type'} &\eqdef& \Sem{\type} + \Sem{\type} \\
\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
@@ -54,10 +56,11 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
- \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
- \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
\Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB} \\
\Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \in \mval_n} \\
+ \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
+ \Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\
+ \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
\Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
\All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
\end{aligned}
@@ -79,9 +82,15 @@ For every definition, we have to show all the side-conditions: The maps have to
\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
\mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
~\\
+ \Sem{\vctx \proves \textlog{abort}\;\term : \type}_\gamma &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\gamma) \\
\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
- \Sem{\vctx \proves \pi_i(\term) : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
+ \Sem{\vctx \proves \pi_i\; \term : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
+ \Sem{\vctx \proves \textlog{inj}_i\;\term : \type_1 + \type_2}_\gamma &\eqdef \mathit{inj}_i(\Sem{\vctx \proves \term : \type_i}_\gamma) \\
+ \Sem{\vctx \proves \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var_1. \term_1 \mid \Ret\textlog{inj}_2\; \var_2. \term_2 \;\textlog{end} : \type }_\gamma &\eqdef
+ \Sem{\vctx, \var_i:\type_i \proves \term_i : \type}_{\mapinsert{\var_i}\termB \gamma} \\
+ &\qquad \text{where $\Sem{\vctx \proves \term : \type_1 + \type_2}_\gamma = \mathit{inj}_i(\termB)$}
+ \\
~\\
\Sem{ \melt : \textlog{M} }_\gamma &\eqdef \melt \\
\Sem{\vctx \proves \mcore\term : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \term : \textlog{M}}_\gamma} \\
@@ -93,6 +102,7 @@ For every definition, we have to show all the side-conditions: The maps have to
An environment $\vctx$ is interpreted as the set of
finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and
$\rho(x)\in\Sem{\vctx(x)}$.
+Above, $\mathit{fix}$ is the fixed-point on COFEs, and $\mathit{abort}_T$ is the unique function $\emptyset \to T$.
\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.
diff --git a/opam b/opam
index 6e0055ed38a08223a584482192853ae4172988c4..96a1b6ce42198be82ba61ded5fd5f1c51aada1aa 100644
--- a/opam
+++ b/opam
@@ -10,7 +10,7 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
- "coq" { >= "8.6.1" & < "8.8~" }
+ "coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
- "coq-stdpp" { (= "dev.2017-11-22.1") | (= "dev") }
+ "coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") }
]
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 2a6b94f843a2ed2088fbe2878ae405a9aa8e29fa..1f6404d4b47ad72a90578a6ccc64639316f63c60 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -26,15 +26,17 @@ Proof.
Thus Ag(T) is not necessarily complete.
*)
-Record agree (A : Type) : Type := Agree {
+Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
-Arguments Agree {_} _ _.
Arguments agree_car {_} _.
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
+Definition to_agree {A} (a : A) : agree A :=
+ {| agree_car := [a]; agree_not_nil := eq_refl |}.
+
Lemma elem_of_agree {A} (x : agree A) : ∃ a, a ∈ agree_car x.
Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y → x = y.
@@ -82,7 +84,7 @@ Instance agree_validN : ValidN (agree A) := λ n x,
Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Program Instance agree_op : Op (agree A) := λ x y,
- Agree (agree_car x ++ agree_car y) _.
+ {| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
Instance agree_pcore : PCore (agree A) := Some.
@@ -157,9 +159,6 @@ Proof.
apply discrete_iff_0; auto.
Qed.
-Program Definition to_agree (a : A) : agree A :=
- {| agree_car := [a]; agree_not_nil := eq_refl |}.
-
Global Instance to_agree_ne : NonExpansive to_agree.
Proof.
intros n a1 a2 Hx; split=> b /=;
@@ -167,6 +166,15 @@ Proof.
Qed.
Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
+Global Instance to_agree_discrete a : Discrete a → Discrete (to_agree a).
+Proof.
+ intros ? y [H H'] n; split.
+ - intros a' ->%elem_of_list_singleton. destruct (H a) as [b ?]; first by left.
+ exists b. by rewrite -discrete_iff_0.
+ - intros b Hb. destruct (H' b) as (b'&->%elem_of_list_singleton&?); auto.
+ exists a. by rewrite elem_of_list_singleton -discrete_iff_0.
+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.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 992400cac2f4e44a79c8b626d6ed7bf786df4e37..87b5a7cc741f95400ad5e89ee56c68ef185bf530 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Global Instance auth_frag_sep_homomorphism :
- MonoidHomomorphism op op (≡) (Auth None).
+ MonoidHomomorphism op op (≡) (@Auth A None).
Proof. by split; [split; try apply _|]. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b ≡ ◠a ⋅ ◯ b.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3c3b1171ca0a40c770e295e5aaff79a7dcecd443..0c1a040fe84a3579d0eb511bb74d34e1ac80caf9 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,4 +1,5 @@
From iris.algebra Require Export ofe monoid.
+From stdpp Require Import finite.
Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A → option A.
@@ -554,11 +555,15 @@ Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
+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.
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.
+Proof. by rewrite -!cmra_discrete_included_iff. Qed.
(** Cancelable elements *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
@@ -1230,92 +1235,93 @@ Qed.
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
- Implicit Types a : A.
+ Implicit Types a b : A.
+ Implicit Types ma mb : option A.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
- Instance option_valid : Valid (option A) := λ mx,
- match mx with Some x => ✓ x | None => True end.
- Instance option_validN : ValidN (option A) := λ n mx,
- match mx with Some x => ✓{n} x | None => True end.
- Instance option_pcore : PCore (option A) := λ mx, Some (mx ≫= pcore).
+ Instance option_valid : Valid (option A) := λ ma,
+ match ma with Some a => ✓ a | None => True end.
+ Instance option_validN : 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 (λ x y, Some (x ⋅ y)).
+ Instance option_op : 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).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
- Lemma Some_op_opM x my : Some x â‹… my = Some (x â‹…? my).
- Proof. by destruct my. Qed.
+ Lemma Some_op_opM a ma : Some a â‹… ma = Some (a â‹…? ma).
+ Proof. by destruct ma. Qed.
- Lemma option_included (mx my : option A) :
- mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≡ y ∨ x ≼ y).
+ Lemma option_included ma mb :
+ ma ≼ mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ (a ≡ b ∨ a ≼ b).
Proof.
split.
- - intros [mz Hmz].
- destruct mx as [x|]; [right|by left].
- destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
- destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
+ - intros [mc Hmc].
+ 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.
- - intros [->|(x&y&->&->&[Hz|[z Hz]])].
- + exists my. by destruct my.
+ - intros [->|(a&b&->&->&[Hc|[c Hc]])].
+ + exists mb. by destruct mb.
+ exists None; by constructor.
- + exists (Some z); by constructor.
+ + exists (Some c); by constructor.
Qed.
- Lemma option_includedN n (mx my : option A) :
- mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y).
+ 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).
Proof.
split.
- - intros [mz Hmz].
- destruct mx as [x|]; [right|by left].
- destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
- destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
+ - intros [mc Hmc].
+ 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;
ofe_subst; eauto using cmra_includedN_l.
- - intros [->|(x&y&->&->&[Hz|[z Hz]])].
- + exists my. by destruct my.
+ - intros [->|(a&y&->&->&[Hc|[c Hc]])].
+ + exists mb. by destruct mb.
+ exists None; by constructor.
- + exists (Some z); by constructor.
+ + exists (Some c); by constructor.
Qed.
Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
apply cmra_total_mixin.
- eauto.
- - by intros [x|] n; destruct 1; constructor; ofe_subst.
+ - by intros [a|] n; destruct 1; constructor; ofe_subst.
- destruct 1; by ofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; ofe_subst.
- - intros [x|]; [apply cmra_valid_validN|done].
- - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
- - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
- - intros [x|]; simpl; auto.
- destruct (pcore x) as [cx|] eqn:?; constructor; eauto using cmra_pcore_l.
- - intros [x|]; simpl; auto.
- destruct (pcore x) as [cx|] eqn:?; simpl; eauto using cmra_pcore_idemp.
- - intros mx my; setoid_rewrite option_included.
- intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
- + destruct (pcore x) as [cx|] eqn:?; eauto.
- destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
- + destruct (pcore x) as [cx|] eqn:?; eauto.
- destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
- - intros n [x|] [y|]; rewrite /validN /option_validN /=;
+ - intros [a|]; [apply cmra_valid_validN|done].
+ - intros n [a|]; unfold validN, option_validN; eauto using cmra_validN_S.
+ - intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
+ - intros [a|] [b|]; constructor; rewrite 1?comm; auto.
+ - intros [a|]; simpl; auto.
+ destruct (pcore a) as [ca|] eqn:?; constructor; eauto using cmra_pcore_l.
+ - intros [a|]; simpl; auto.
+ destruct (pcore a) as [ca|] eqn:?; simpl; eauto using cmra_pcore_idemp.
+ - intros ma mb; setoid_rewrite option_included.
+ intros [->|(a&b&->&->&[?|?])]; simpl; eauto.
+ + destruct (pcore a) as [ca|] eqn:?; eauto.
+ 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 /=;
eauto using cmra_validN_op_l.
- - intros n mx my1 my2.
- destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
+ - intros n ma mb1 mb2.
+ destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
inversion_clear Hx'; auto.
- + destruct (cmra_extend n x y1 y2) as (z1&z2&?&?&?); auto.
- by exists (Some z1), (Some z2); repeat constructor.
- + by exists (Some x), None; repeat constructor.
- + by exists None, (Some x); repeat constructor.
+ + destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto.
+ by exists (Some c1), (Some c2); repeat constructor.
+ + by exists (Some a), None; repeat constructor.
+ + by exists None, (Some a); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
Canonical Structure optionR := CmraT (option A) option_cmra_mixin.
Global Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
- Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
+ Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
Instance option_unit : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
@@ -1323,61 +1329,63 @@ Section option.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
(** Misc *)
- Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None.
- Proof. destruct mx, my; naive_solver. Qed.
- Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
- Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
+ Lemma op_None ma mb : ma ⋅ mb = None ↔ ma = None ∧ mb = None.
+ Proof. destruct ma, mb; naive_solver. Qed.
+ Lemma op_is_Some ma mb : is_Some (ma ⋅ mb) ↔ is_Some ma ∨ is_Some mb.
+ Proof. rewrite -!not_eq_None_Some op_None. destruct ma, mb; naive_solver. Qed.
+
+ Lemma cmra_opM_assoc' a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
+ Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
- Global Instance Some_core_id (x : A) : CoreId x → CoreId (Some x).
+ Global Instance Some_core_id a : CoreId a → CoreId (Some a).
Proof. by constructor. Qed.
- Global Instance option_core_id (mx : option A) :
- (∀ x : A, CoreId x) → CoreId mx.
- Proof. intros. destruct mx; apply _. Qed.
-
- Lemma exclusiveN_Some_l n x `{!Exclusive x} my :
- ✓{n} (Some x ⋅ my) → my = None.
- Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed.
- Lemma exclusiveN_Some_r n x `{!Exclusive x} my :
- ✓{n} (my ⋅ Some x) → my = None.
+ Global Instance option_core_id ma : (∀ x : A, CoreId x) → CoreId ma.
+ Proof. intros. destruct ma; apply _. Qed.
+
+ Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
+ ✓{n} (Some a ⋅ mb) → mb = None.
+ Proof. destruct mb. move=> /(exclusiveN_l _ a) []. done. Qed.
+ Lemma exclusiveN_Some_r n a `{!Exclusive a} mb :
+ ✓{n} (mb ⋅ Some a) → mb = None.
Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
- Lemma exclusive_Some_l x `{!Exclusive x} my : ✓ (Some x ⋅ my) → my = None.
- Proof. destruct my. move=> /(exclusive_l x) []. done. Qed.
- Lemma exclusive_Some_r x `{!Exclusive x} my : ✓ (my ⋅ Some x) → my = None.
+ Lemma exclusive_Some_l a `{!Exclusive a} mb : ✓ (Some a ⋅ mb) → mb = None.
+ Proof. destruct mb. move=> /(exclusive_l a) []. done. Qed.
+ Lemma exclusive_Some_r a `{!Exclusive a} mb : ✓ (mb ⋅ Some a) → mb = None.
Proof. rewrite comm. by apply exclusive_Some_l. Qed.
- Lemma Some_includedN n x y : Some x ≼{n} Some y ↔ x ≡{n}≡ y ∨ x ≼{n} y.
+ 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_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
+ Lemma Some_included a b : Some a ≼ Some b ↔ a ≡ b ∨ a ≼ b.
Proof. rewrite option_included; naive_solver. Qed.
- Lemma Some_included_2 x y : x ≼ y → Some x ≼ Some y.
+ Lemma Some_included_2 a b : a ≼ b → Some a ≼ Some b.
Proof. rewrite Some_included; eauto. Qed.
- Lemma Some_includedN_total `{CmraTotal A} n x y : Some x ≼{n} Some y ↔ x ≼{n} y.
+ Lemma Some_includedN_total `{CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
Proof. rewrite Some_includedN. split. by intros [->|?]. eauto. Qed.
- Lemma Some_included_total `{CmraTotal A} x y : Some x ≼ Some y ↔ x ≼ y.
+ Lemma Some_included_total `{CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
- Lemma Some_includedN_exclusive n x `{!Exclusive x} y :
- Some x ≼{n} Some y → ✓{n} y → x ≡{n}≡ y.
+ Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
+ Some a ≼{n} Some b → ✓{n} b → a ≡{n}≡ b.
Proof. move=> /Some_includedN [//|/exclusive_includedN]; tauto. Qed.
- Lemma Some_included_exclusive x `{!Exclusive x} y :
- Some x ≼ Some y → ✓ y → x ≡ y.
+ Lemma Some_included_exclusive a `{!Exclusive a} b :
+ Some a ≼ Some b → ✓ b → a ≡ b.
Proof. move=> /Some_included [//|/exclusive_included]; tauto. Qed.
- Lemma is_Some_includedN n mx my : mx ≼{n} my → is_Some mx → is_Some my.
+ Lemma is_Some_includedN n ma mb : ma ≼{n} mb → is_Some ma → is_Some mb.
Proof. rewrite -!not_eq_None_Some option_includedN. naive_solver. Qed.
- Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
+ Lemma is_Some_included ma mb : ma ≼ mb → is_Some ma → is_Some mb.
Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
- Global Instance cancelable_Some x :
- IdFree x → Cancelable x → Cancelable (Some x).
+ Global Instance cancelable_Some a :
+ IdFree a → Cancelable a → Cancelable (Some a).
Proof.
- intros Hirr ?? [y|] [z|] ? EQ; inversion_clear EQ.
- - constructor. by apply (cancelableN x).
- - destruct (Hirr y); [|eauto using dist_le with lia].
- by eapply (cmra_validN_op_l 0 x y), (cmra_validN_le n); last lia.
- - destruct (Hirr z); [|symmetry; eauto using dist_le with lia].
+ intros Hirr ?? [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.
- done.
Qed.
@@ -1388,35 +1396,37 @@ Arguments optionUR : clear implicits.
Section option_prod.
Context {A B : cmraT}.
+ Implicit Types a : A.
+ Implicit Types b : B.
- Lemma Some_pair_includedN n (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼{n} Some (x2,y2) → Some x1 ≼{n} Some x2 ∧ Some y1 ≼{n} Some y2.
+ 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 (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼{n} Some (x2,y2) → x1 ≼{n} x2 ∧ Some y1 ≼{n} Some y2.
- Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ x1). Qed.
- Lemma Some_pair_includedN_total_2 `{CmraTotal B} n (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼{n} Some (x2,y2) → Some x1 ≼{n} Some x2 ∧ y1 ≼{n} y2.
- Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ y1). Qed.
-
- Lemma Some_pair_included (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ Some y1 ≼ Some y2.
+ 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 :
+ 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} (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼ Some (x2,y2) → x1 ≼ x2 ∧ Some y1 ≼ Some y2.
- Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total x1). Qed.
- Lemma Some_pair_included_total_2 `{CmraTotal B} (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ y1 ≼ y2.
- Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total y1). 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 :
+ 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.
Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A → option B).
Proof.
split; first apply _.
- - intros n [x|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
- - move=> [x|] //. by apply Some_proper, cmra_morphism_pcore.
- - move=> [x|] [y|] //=. by rewrite -(cmra_morphism_op f).
+ - intros n [a|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
+ - move=> [a|] //. by apply Some_proper, cmra_morphism_pcore.
+ - move=> [a|] [b|] //=. by rewrite -(cmra_morphism_op f).
Qed.
Program Definition optionRF (F : rFunctor) : rFunctor := {|
@@ -1462,3 +1472,103 @@ Instance optionURF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
+
+(* Dependently-typed functions over a finite discrete domain *)
+Section ofe_fun_cmra.
+ Context `{Hfin : Finite A} {B : A → ucmraT}.
+ Implicit Types f g : ofe_fun B.
+
+ Instance ofe_fun_op : Op (ofe_fun B) := λ f g x, f x ⋅ g x.
+ Instance ofe_fun_pcore : PCore (ofe_fun B) := λ f, Some (λ x, core (f x)).
+ Instance ofe_fun_valid : Valid (ofe_fun B) := λ f, ∀ x, ✓ f x.
+ Instance ofe_fun_validN : ValidN (ofe_fun B) := λ n f, ∀ x, ✓{n} f x.
+
+ Definition ofe_fun_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
+ Definition ofe_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
+
+ Lemma ofe_fun_included_spec (f g : ofe_fun B) : f ≼ g ↔ ∀ x, f x ≼ g x.
+ Proof using Hfin.
+ split; [by intros [h Hh] x; exists (h x); rewrite /op /ofe_fun_op (Hh x)|].
+ intros [h ?]%finite_choice. by exists h.
+ Qed.
+
+ Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B).
+ Proof using Hfin.
+ apply cmra_total_mixin.
+ - eauto.
+ - by intros n f1 f2 f3 Hf x; rewrite ofe_fun_lookup_op (Hf x).
+ - by intros n f1 f2 Hf x; rewrite ofe_fun_lookup_core (Hf x).
+ - by intros n f1 f2 Hf ? x; 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 ofe_fun_lookup_op assoc.
+ - by intros f1 f2 x; rewrite ofe_fun_lookup_op comm.
+ - by intros f x; rewrite ofe_fun_lookup_op ofe_fun_lookup_core cmra_core_l.
+ - by intros f x; rewrite ofe_fun_lookup_core cmra_core_idemp.
+ - intros f1 f2; rewrite !ofe_fun_included_spec=> Hf x.
+ by rewrite ofe_fun_lookup_core; apply cmra_core_mono, Hf.
+ - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
+ - intros n f f1 f2 Hf Hf12.
+ destruct (finite_choice (λ x (yy : B x * B x),
+ f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg].
+ { intros x. specialize (Hf12 x).
+ destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
+ exists (y1,y2); eauto. }
+ exists (λ x, (gg x).1), (λ x, (gg x).2). split_and!=> -?; naive_solver.
+ Qed.
+ Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
+
+ Instance ofe_fun_unit : Unit (ofe_fun B) := λ x, ε.
+ Definition ofe_fun_lookup_empty x : ε x = ε := eq_refl.
+
+ Lemma ofe_fun_ucmra_mixin : UcmraMixin (ofe_fun B).
+ Proof.
+ split.
+ - intros x; apply ucmra_unit_valid.
+ - by intros f x; rewrite ofe_fun_lookup_op left_id.
+ - constructor=> x. apply core_id_core, _.
+ Qed.
+ Canonical Structure ofe_funUR := UcmraT (ofe_fun B) ofe_fun_ucmra_mixin.
+
+ Global Instance ofe_fun_unit_discrete :
+ (∀ i, Discrete (ε : B i)) → Discrete (ε : ofe_fun B).
+ Proof. intros ? f Hf x. by apply: discrete. Qed.
+End ofe_fun_cmra.
+
+Arguments ofe_funR {_ _ _} _.
+Arguments ofe_funUR {_ _ _} _.
+
+Instance ofe_fun_map_cmra_morphism
+ `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
+ (∀ x, CmraMorphism (f x)) → CmraMorphism (ofe_fun_map f).
+Proof.
+ split; first apply _.
+ - intros n g Hg x; rewrite /ofe_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 /ofe_fun_map ofe_fun_lookup_op cmra_morphism_op.
+Qed.
+
+Program Definition ofe_funURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
+ urFunctor_car A B := ofe_funUR (λ c, urFunctor_car (F c) A B);
+ urFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
+|}.
+Next Obligation.
+ intros C ?? F A1 A2 B1 B2 n ?? g.
+ by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
+Qed.
+Next Obligation.
+ intros C ?? F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
+ apply ofe_fun_map_ext=> y; apply urFunctor_id.
+Qed.
+Next Obligation.
+ intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose.
+ apply ofe_fun_map_ext=>y; apply urFunctor_compose.
+Qed.
+Instance ofe_funURF_contractive `{Finite C} (F : C → urFunctor) :
+ (∀ c, urFunctorContractive (F c)) → urFunctorContractive (ofe_funURF F).
+Proof.
+ intros ? A1 A2 B1 B2 n ?? g.
+ by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
+Qed.
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 3f65239d370aa0d8241d9e0dc3ac7f9d6de51de1..814bf3224fc636e4f5480dd552be77e92e3736ee 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -93,7 +93,7 @@ Section frac_auth.
IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
- Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
+ Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) :
CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
new file mode 100644
index 0000000000000000000000000000000000000000..a0fd519b00d28b13f1a2587cd4b7c4acd91a7cdd
--- /dev/null
+++ b/theories/algebra/functions.v
@@ -0,0 +1,153 @@
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates.
+From stdpp Require Import finite.
+Set Default Proof Using "Type".
+
+Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
+ (x : A) (y : B x) (f : ofe_fun B) : ofe_fun B := λ x',
+ match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
+Instance: Params (@ofe_fun_insert) 5.
+
+Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT}
+ (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
+Instance: Params (@ofe_fun_singleton) 5.
+
+Section ofe.
+ Context `{Heqdec : EqDecision A} {B : A → ofeT}.
+ Implicit Types x : A.
+ Implicit Types f g : ofe_fun B.
+
+ (** Properties of ofe_fun_insert. *)
+ Global Instance ofe_fun_insert_ne x :
+ NonExpansive2 (ofe_fun_insert (B:=B) x).
+ Proof.
+ intros n y1 y2 ? f1 f2 ? x'; rewrite /ofe_fun_insert.
+ by destruct (decide _) as [[]|].
+ Qed.
+ Global Instance ofe_fun_insert_proper x :
+ Proper ((≡) ==> (≡) ==> (≡)) (ofe_fun_insert (B:=B) x) := ne_proper_2 _.
+
+ Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
+ Proof.
+ rewrite /ofe_fun_insert; destruct (decide _) as [Hx|]; last done.
+ by rewrite (proof_irrel Hx eq_refl).
+ Qed.
+ Lemma ofe_fun_lookup_insert_ne f x x' y :
+ x ≠x' → (ofe_fun_insert x y f) x' = f x'.
+ Proof. by rewrite /ofe_fun_insert; destruct (decide _). Qed.
+
+ Global Instance ofe_fun_insert_discrete f x y :
+ Discrete f → Discrete y → Discrete (ofe_fun_insert x y f).
+ Proof.
+ intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
+ - rewrite ofe_fun_lookup_insert.
+ apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert.
+ - rewrite ofe_fun_lookup_insert_ne //.
+ apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert_ne.
+ Qed.
+End ofe.
+
+Section cmra.
+ Context `{Finite A} {B : A → ucmraT}.
+ Implicit Types x : A.
+ Implicit Types f g : ofe_fun B.
+
+ Global Instance ofe_fun_singleton_ne x :
+ NonExpansive (ofe_fun_singleton x : B x → _).
+ Proof. intros n y1 y2 ?; apply ofe_fun_insert_ne. done. by apply equiv_dist. Qed.
+ Global Instance ofe_fun_singleton_proper x :
+ Proper ((≡) ==> (≡)) (ofe_fun_singleton x) := ne_proper _.
+
+ Lemma ofe_fun_lookup_singleton x (y : B x) : (ofe_fun_singleton x y) x = y.
+ Proof. by rewrite /ofe_fun_singleton ofe_fun_lookup_insert. Qed.
+ Lemma ofe_fun_lookup_singleton_ne x x' (y : B x) :
+ x ≠x' → (ofe_fun_singleton x y) x' = ε.
+ Proof. intros; by rewrite /ofe_fun_singleton ofe_fun_lookup_insert_ne. Qed.
+
+ Global Instance ofe_fun_singleton_discrete x (y : B x) :
+ (∀ i, Discrete (ε : B i)) → Discrete y → Discrete (ofe_fun_singleton x y).
+ Proof. apply _. Qed.
+
+ Lemma ofe_fun_singleton_validN n x (y : B x) : ✓{n} ofe_fun_singleton x y ↔ ✓{n} y.
+ Proof.
+ split; [by move=>/(_ x); rewrite ofe_fun_lookup_singleton|].
+ move=>Hx x'; destruct (decide (x = x')) as [->|];
+ rewrite ?ofe_fun_lookup_singleton ?ofe_fun_lookup_singleton_ne //.
+ by apply ucmra_unit_validN.
+ Qed.
+
+ Lemma ofe_fun_core_singleton x (y : B x) :
+ core (ofe_fun_singleton x y) ≡ ofe_fun_singleton x (core y).
+ Proof.
+ move=>x'; destruct (decide (x = x')) as [->|];
+ by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
+ ?ofe_fun_lookup_singleton_ne // (core_id_core ∅).
+ Qed.
+
+ Global Instance ofe_fun_singleton_core_id x (y : B x) :
+ CoreId y → CoreId (ofe_fun_singleton x y).
+ Proof. by rewrite !core_id_total ofe_fun_core_singleton=> ->. Qed.
+
+ Lemma ofe_fun_op_singleton (x : A) (y1 y2 : B x) :
+ ofe_fun_singleton x y1 ⋅ ofe_fun_singleton x y2 ≡ ofe_fun_singleton x (y1 ⋅ y2).
+ Proof.
+ intros x'; destruct (decide (x' = x)) as [->|].
+ - by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton.
+ - by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton_ne // left_id.
+ Qed.
+
+ Lemma ofe_fun_insert_updateP x (P : B x → Prop) (Q : ofe_fun B → Prop) g y1 :
+ y1 ~~>: P → (∀ y2, P y2 → Q (ofe_fun_insert x y2 g)) →
+ ofe_fun_insert x y1 g ~~>: Q.
+ Proof.
+ intros Hy1 HP; apply cmra_total_updateP.
+ intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
+ { move: (Hg x). by rewrite ofe_fun_lookup_op ofe_fun_lookup_insert. }
+ exists (ofe_fun_insert x y2 g); split; [auto|].
+ intros x'; destruct (decide (x' = x)) as [->|];
+ rewrite ofe_fun_lookup_op ?ofe_fun_lookup_insert //; [].
+ move: (Hg x'). by rewrite ofe_fun_lookup_op !ofe_fun_lookup_insert_ne.
+ Qed.
+
+ Lemma ofe_fun_insert_updateP' x (P : B x → Prop) g y1 :
+ y1 ~~>: P →
+ ofe_fun_insert x y1 g ~~>: λ g', ∃ y2, g' = ofe_fun_insert x y2 g ∧ P y2.
+ Proof. eauto using ofe_fun_insert_updateP. Qed.
+ Lemma ofe_fun_insert_update g x y1 y2 :
+ y1 ~~> y2 → ofe_fun_insert x y1 g ~~> ofe_fun_insert x y2 g.
+ Proof.
+ rewrite !cmra_update_updateP; eauto using ofe_fun_insert_updateP with subst.
+ Qed.
+
+ Lemma ofe_fun_singleton_updateP x (P : B x → Prop) (Q : ofe_fun B → Prop) y1 :
+ y1 ~~>: P → (∀ y2, P y2 → Q (ofe_fun_singleton x y2)) →
+ ofe_fun_singleton x y1 ~~>: Q.
+ Proof. rewrite /ofe_fun_singleton; eauto using ofe_fun_insert_updateP. Qed.
+ Lemma ofe_fun_singleton_updateP' x (P : B x → Prop) y1 :
+ y1 ~~>: P →
+ ofe_fun_singleton x y1 ~~>: λ g, ∃ y2, g = ofe_fun_singleton x y2 ∧ P y2.
+ Proof. eauto using ofe_fun_singleton_updateP. Qed.
+ Lemma ofe_fun_singleton_update x (y1 y2 : B x) :
+ y1 ~~> y2 → ofe_fun_singleton x y1 ~~> ofe_fun_singleton x y2.
+ Proof. eauto using ofe_fun_insert_update. Qed.
+
+ Lemma ofe_fun_singleton_updateP_empty x (P : B x → Prop) (Q : ofe_fun B → Prop) :
+ ε ~~>: P → (∀ y2, P y2 → Q (ofe_fun_singleton x y2)) → ε ~~>: Q.
+ Proof.
+ intros Hx HQ; apply cmra_total_updateP.
+ intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
+ exists (ofe_fun_singleton x y2); split; [by apply HQ|].
+ intros x'; destruct (decide (x' = x)) as [->|].
+ - by rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton.
+ - rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton_ne //. apply Hg.
+ Qed.
+ Lemma ofe_fun_singleton_updateP_empty' x (P : B x → Prop) :
+ ε ~~>: P → ε ~~>: λ g, ∃ y2, g = ofe_fun_singleton x y2 ∧ P y2.
+ Proof. eauto using ofe_fun_singleton_updateP_empty. Qed.
+ Lemma ofe_fun_singleton_update_empty x (y : B x) :
+ ε ~~> y → ε ~~> ofe_fun_singleton x y.
+ Proof.
+ rewrite !cmra_update_updateP;
+ eauto using ofe_fun_singleton_updateP_empty with subst.
+ Qed.
+End cmra.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index a09b287e85b6afdfd71b15e2226985ae528e6e50..b9a995537ea553ed15d6c179b48769353d47beb4 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -7,6 +7,7 @@ Set Default Proof Using "Type".
Section cofe.
Context `{Countable K} {A : ofeT}.
Implicit Types m : gmap K A.
+Implicit Types i : K.
Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
∀ i, m1 !! i ≡{n}≡ m2 !! i.
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
deleted file mode 100644
index e3051d27f9b7e4d4fc730c14eb8ac68afde98794..0000000000000000000000000000000000000000
--- a/theories/algebra/iprod.v
+++ /dev/null
@@ -1,345 +0,0 @@
-From iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
-From stdpp Require Import finite.
-Set Default Proof Using "Type".
-
-(** * Indexed product *)
-(** Need to put this in a definition to make canonical structures to work. *)
-Definition iprod `{Finite A} (B : A → ofeT) := ∀ x, B x.
-Definition iprod_insert `{Finite A} {B : A → ofeT}
- (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
- match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Instance: Params (@iprod_insert) 5.
-
-Section iprod_cofe.
- Context `{Finite A} {B : A → ofeT}.
- Implicit Types x : A.
- Implicit Types f g : iprod B.
-
- Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
- Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
- Definition iprod_ofe_mixin : OfeMixin (iprod B).
- Proof.
- split.
- - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
- intros Hfg k; apply equiv_dist; intros n; apply Hfg.
- - intros n; split.
- + by intros f x.
- + by intros f g ? x.
- + by intros f g h ?? x; trans (g x).
- - intros n f g Hfg x; apply dist_S, Hfg.
- Qed.
- Canonical Structure iprodC : ofeT := OfeT (iprod B) iprod_ofe_mixin.
-
- Program Definition iprod_chain (c : chain iprodC) (x : A) : chain (B x) :=
- {| chain_car n := c n x |}.
- Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
- Global Program Instance iprod_cofe `{∀ a, Cofe (B a)} : Cofe iprodC :=
- {| compl c x := compl (iprod_chain c x) |}.
- Next Obligation.
- intros ? n c x.
- rewrite (conv_compl n (iprod_chain c x)).
- apply (chain_cauchy c); lia.
- Qed.
-
- (** Properties of iprod_insert. *)
- Global Instance iprod_insert_ne x :
- NonExpansive2 (iprod_insert x).
- Proof.
- intros n y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
- by destruct (decide _) as [[]|].
- Qed.
- Global Instance iprod_insert_proper x :
- Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _.
-
- Lemma iprod_lookup_insert f x y : (iprod_insert x y f) x = y.
- Proof.
- rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done.
- by rewrite (proof_irrel Hx eq_refl).
- Qed.
- Lemma iprod_lookup_insert_ne f x x' y :
- x ≠x' → (iprod_insert x y f) x' = f x'.
- Proof. by rewrite /iprod_insert; destruct (decide _). Qed.
-
- Global Instance iprod_lookup_discrete f x : Discrete f → Discrete (f x).
- Proof.
- intros ? y ?.
- cut (f ≡ iprod_insert x y f).
- { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
- apply (discrete _)=> x'; destruct (decide (x = x')) as [->|];
- by rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
- Qed.
- Global Instance iprod_insert_discrete f x y :
- Discrete f → Discrete y → Discrete (iprod_insert x y f).
- Proof.
- intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
- - rewrite iprod_lookup_insert.
- apply: discrete. by rewrite -(Heq x') iprod_lookup_insert.
- - rewrite iprod_lookup_insert_ne //.
- apply: discrete. by rewrite -(Heq x') iprod_lookup_insert_ne.
- Qed.
-End iprod_cofe.
-
-Arguments iprodC {_ _ _} _.
-
-Section iprod_cmra.
- Context `{Finite A} {B : A → ucmraT}.
- Implicit Types f g : iprod B.
-
- Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
- Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)).
- Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
- Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
-
- Definition iprod_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
- Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
-
- Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
- Proof.
- split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
- intros [h ?]%finite_choice. by exists h.
- Qed.
-
- Lemma iprod_cmra_mixin : CmraMixin (iprod B).
- Proof.
- apply cmra_total_mixin.
- - eauto.
- - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
- - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
- - by intros n f1 f2 Hf ? x; 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 iprod_lookup_op assoc.
- - by intros f1 f2 x; rewrite iprod_lookup_op comm.
- - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
- - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
- - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
- by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
- - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- - intros n f f1 f2 Hf Hf12.
- destruct (finite_choice (λ x (yy : B x * B x),
- f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg].
- { intros x. specialize (Hf12 x).
- destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
- exists (y1,y2); eauto. }
- exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
- Qed.
- Canonical Structure iprodR := CmraT (iprod B) iprod_cmra_mixin.
-
- Instance iprod_unit : Unit (iprod B) := λ x, ε.
- Definition iprod_lookup_empty x : ε x = ε := eq_refl.
-
- Lemma iprod_ucmra_mixin : UcmraMixin (iprod B).
- Proof.
- split.
- - intros x; apply ucmra_unit_valid.
- - by intros f x; rewrite iprod_lookup_op left_id.
- - constructor=> x. apply core_id_core, _.
- Qed.
- Canonical Structure iprodUR := UcmraT (iprod B) iprod_ucmra_mixin.
-
- Global Instance iprod_unit_discrete :
- (∀ i, Discrete (ε : B i)) → Discrete (ε : iprod B).
- Proof. intros ? f Hf x. by apply: discrete. Qed.
-
- (** Internalized properties *)
- Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
- Proof. by uPred.unseal. Qed.
- Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M).
- Proof. by uPred.unseal. Qed.
-
- (** Properties of iprod_insert. *)
- Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 :
- y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
- iprod_insert x y1 g ~~>: Q.
- Proof.
- intros Hy1 HP; apply cmra_total_updateP.
- intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
- { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
- exists (iprod_insert x y2 g); split; [auto|].
- intros x'; destruct (decide (x' = x)) as [->|];
- rewrite iprod_lookup_op ?iprod_lookup_insert //; [].
- move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne.
- Qed.
-
- Lemma iprod_insert_updateP' x (P : B x → Prop) g y1 :
- y1 ~~>: P →
- iprod_insert x y1 g ~~>: λ g', ∃ y2, g' = iprod_insert x y2 g ∧ P y2.
- Proof. eauto using iprod_insert_updateP. Qed.
- Lemma iprod_insert_update g x y1 y2 :
- y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
- Proof.
- rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
- Qed.
-End iprod_cmra.
-
-Arguments iprodR {_ _ _} _.
-Arguments iprodUR {_ _ _} _.
-
-Definition iprod_singleton `{Finite A} {B : A → ucmraT}
- (x : A) (y : B x) : iprod B := iprod_insert x y ε.
-Instance: Params (@iprod_singleton) 5.
-
-Section iprod_singleton.
- Context `{Finite A} {B : A → ucmraT}.
- Implicit Types x : A.
-
- Global Instance iprod_singleton_ne x :
- NonExpansive (iprod_singleton x : B x → _).
- Proof. intros n y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
- Global Instance iprod_singleton_proper x :
- Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
-
- Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y.
- Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
- Lemma iprod_lookup_singleton_ne x x' (y : B x) :
- x ≠x' → (iprod_singleton x y) x' = ε.
- Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
-
- Global Instance iprod_singleton_discrete x (y : B x) :
- (∀ i, Discrete (ε : B i)) → Discrete y → Discrete (iprod_singleton x y).
- Proof. apply _. Qed.
-
- Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
- Proof.
- split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
- move=>Hx x'; destruct (decide (x = x')) as [->|];
- rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
- by apply ucmra_unit_validN.
- Qed.
-
- Lemma iprod_core_singleton x (y : B x) :
- core (iprod_singleton x y) ≡ iprod_singleton x (core y).
- Proof.
- move=>x'; destruct (decide (x = x')) as [->|];
- by rewrite iprod_lookup_core ?iprod_lookup_singleton
- ?iprod_lookup_singleton_ne // (core_id_core ∅).
- Qed.
-
- Global Instance iprod_singleton_core_id x (y : B x) :
- CoreId y → CoreId (iprod_singleton x y).
- Proof. by rewrite !core_id_total iprod_core_singleton=> ->. Qed.
-
- Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
- iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
- Proof.
- intros x'; destruct (decide (x' = x)) as [->|].
- - by rewrite iprod_lookup_op !iprod_lookup_singleton.
- - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
- Qed.
-
- Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 :
- y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
- iprod_singleton x y1 ~~>: Q.
- Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
- Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
- y1 ~~>: P →
- iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
- Proof. eauto using iprod_singleton_updateP. Qed.
- Lemma iprod_singleton_update x (y1 y2 : B x) :
- y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
- Proof. eauto using iprod_insert_update. Qed.
-
- Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
- ε ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ε ~~>: Q.
- Proof.
- intros Hx HQ; apply cmra_total_updateP.
- intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
- exists (iprod_singleton x y2); split; [by apply HQ|].
- intros x'; destruct (decide (x' = x)) as [->|].
- - by rewrite iprod_lookup_op iprod_lookup_singleton.
- - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
- Qed.
- Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
- ε ~~>: P → ε ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
- Proof. eauto using iprod_singleton_updateP_empty. Qed.
- Lemma iprod_singleton_update_empty x (y : B x) :
- ε ~~> y → ε ~~> iprod_singleton x y.
- Proof.
- rewrite !cmra_update_updateP;
- eauto using iprod_singleton_updateP_empty with subst.
- Qed.
-End iprod_singleton.
-
-(** * Functor *)
-Definition iprod_map `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
- (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-
-Lemma iprod_map_ext `{Finite A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x) (g : iprod B1) :
- (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
-Proof. done. Qed.
-Lemma iprod_map_id `{Finite A} {B : A → ofeT} (g : iprod B) :
- iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose `{Finite A} {B1 B2 B3 : A → ofeT}
- (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
- iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
-Proof. done. Qed.
-
-Instance iprod_map_ne `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
- (∀ x, Proper (dist n ==> dist n) (f x)) →
- Proper (dist n ==> dist n) (iprod_map f).
-Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Instance iprod_map_cmra_morphism
- `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
- (∀ x, CmraMorphism (f x)) → CmraMorphism (iprod_map f).
-Proof.
- split; first apply _.
- - intros n g Hg x; rewrite /iprod_map; apply (cmra_morphism_validN (f _)), Hg.
- - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
- - intros g1 g2 i. by rewrite /iprod_map iprod_lookup_op cmra_morphism_op.
-Qed.
-
-Definition iprodC_map `{Finite A} {B1 B2 : A → ofeT}
- (f : iprod (λ x, B1 x -n> B2 x)) :
- iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} :
- NonExpansive (@iprodC_map A _ _ B1 B2).
-Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
-
-Program Definition iprodCF `{Finite C} (F : C → cFunctor) : cFunctor := {|
- cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
- cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
-|}.
-Next Obligation.
- intros C ?? F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
-Qed.
-Next Obligation.
- intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
- apply iprod_map_ext=> y; apply cFunctor_id.
-Qed.
-Next Obligation.
- intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
- apply iprod_map_ext=>y; apply cFunctor_compose.
-Qed.
-Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
- (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
-Proof.
- intros ? A1 A2 B1 B2 n ?? g.
- by apply iprodC_map_ne=>c; apply cFunctor_contractive.
-Qed.
-
-Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
- urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
- urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
-|}.
-Next Obligation.
- intros C ?? F A1 A2 B1 B2 n ?? g.
- by apply iprodC_map_ne=>?; apply urFunctor_ne.
-Qed.
-Next Obligation.
- intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
- apply iprod_map_ext=> y; apply urFunctor_id.
-Qed.
-Next Obligation.
- intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
- apply iprod_map_ext=>y; apply urFunctor_compose.
-Qed.
-Instance iprodURF_contractive `{Finite C} (F : C → urFunctor) :
- (∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F).
-Proof.
- intros ? A1 A2 B1 B2 n ?? g.
- by apply iprodC_map_ne=>c; apply urFunctor_contractive.
-Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index ed4736a1875450294db3b1b7474a06c9357e0fe8..67f56c2f782c5a6844f9c9998799824eeb3821f3 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -6,6 +6,7 @@ Set Default Proof Using "Type".
Section cofe.
Context {A : ofeT}.
+Implicit Types l : list A.
Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 56d17e71096d71848325e74fce4f1ea7b0b9e2b3..d573744c283d7a6106d6166ddf434deaf02f62ae 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -190,9 +190,7 @@ Section ofe.
split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
Qed.
Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x ≡{0}≡ y ↔ x ≡{n}≡ y.
- Proof.
- split=> ?. by apply equiv_dist, (discrete _). eauto using dist_le with lia.
- Qed.
+ Proof. by rewrite -!discrete_iff. Qed.
End ofe.
(** Contractive functions *)
@@ -511,42 +509,6 @@ Section fixpointAB_ne.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
End fixpointAB_ne.
-(** Function space *)
-(* We make [ofe_fun] a definition so that we can register it as a canonical
-structure. *)
-Definition ofe_fun (A : Type) (B : ofeT) := A → B.
-
-Section ofe_fun.
- Context {A : Type} {B : ofeT}.
- Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, ∀ x, f x ≡ g x.
- Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
- Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
- Proof.
- split.
- - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
- intros Hfg k; apply equiv_dist=> n; apply Hfg.
- - intros n; split.
- + by intros f x.
- + by intros f g ? x.
- + by intros f g h ?? x; trans (g x).
- - by intros n f g ? x; apply dist_S.
- Qed.
- Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
-
- Program Definition ofe_fun_chain `(c : chain ofe_funC)
- (x : A) : chain B := {| chain_car n := c n x |}.
- Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
- Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
- { compl c x := compl (ofe_fun_chain c x) }.
- Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
-End ofe_fun.
-
-Arguments ofe_funC : clear implicits.
-Notation "A -c> B" :=
- (ofe_funC A B) (at level 99, B at level 200, right associativity).
-Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
- Inhabited (A -c> B) := populate (λ _, inhabitant).
-
(** Non-expansive function space *)
Record ofe_mor (A B : ofeT) : Type := CofeMor {
ofe_mor_car :> A → B;
@@ -762,37 +724,6 @@ Proof.
by apply prodC_map_ne; apply cFunctor_contractive.
Qed.
-Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') :
- NonExpansive (compose f : (A -c> B) → A -c> B').
-Proof. intros n g g' Hf x; simpl. by rewrite (Hf x). Qed.
-
-Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
- @CofeMor (_ -c> _) (_ -c> _) (compose f) _.
-Instance ofe_funC_map_ne {A B B'} :
- NonExpansive (@ofe_funC_map A B B').
-Proof. intros n f f' Hf g x. apply Hf. Qed.
-
-Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
- cFunctor_car A B := ofe_funC T (cFunctor_car F A B);
- cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
- intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne.
-Qed.
-Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed.
-Next Obligation.
- intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
- by rewrite !cFunctor_compose.
-Qed.
-Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
-
-Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
- cFunctorContractive F → cFunctorContractive (ofe_funCF T F).
-Proof.
- intros ?? A1 A2 B1 B2 n ???;
- by apply ofe_funC_map_ne; apply cFunctor_contractive.
-Qed.
-
Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
cFunctor_map A1 A2 B1 B2 fg :=
@@ -1154,6 +1085,106 @@ Proof.
destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
Qed.
+(* Dependently-typed functions over a discrete domain *)
+(* We make [ofe_fun] a definition so that we can register it as a canonical
+structure. *)
+Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x.
+
+Section ofe_fun.
+ Context {A : Type} {B : A → ofeT}.
+ Implicit Types f g : ofe_fun B.
+
+ Instance ofe_fun_equiv : Equiv (ofe_fun B) := λ f g, ∀ x, f x ≡ g x.
+ Instance ofe_fun_dist : Dist (ofe_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+ Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun B).
+ Proof.
+ split.
+ - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
+ intros Hfg k; apply equiv_dist=> n; apply Hfg.
+ - intros n; split.
+ + by intros f x.
+ + by intros f g ? x.
+ + by intros f g h ?? x; trans (g x).
+ - by intros n f g ? x; apply dist_S.
+ Qed.
+ Canonical Structure ofe_funC := OfeT (ofe_fun B) ofe_fun_ofe_mixin.
+
+ Program Definition ofe_fun_chain `(c : chain ofe_funC)
+ (x : A) : chain (B x) := {| chain_car n := c n x |}.
+ Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
+ Global Program Instance ofe_fun_cofe `{∀ x, Cofe (B x)} : Cofe ofe_funC :=
+ { compl c x := compl (ofe_fun_chain c x) }.
+ Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
+
+ Global Instance ofe_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited ofe_funC :=
+ populate (λ _, inhabitant).
+ Global Instance ofe_fun_lookup_discrete `{EqDecision A} f x :
+ Discrete f → Discrete (f x).
+ Proof.
+ intros Hf y ?.
+ set (g x' := if decide (x = x') is left H then eq_rect _ B y _ H else f x').
+ trans (g x).
+ { apply Hf=> x'. unfold g. by destruct (decide _) as [[]|]. }
+ unfold g. destruct (decide _) as [Hx|]; last done.
+ by rewrite (proof_irrel Hx eq_refl).
+ Qed.
+End ofe_fun.
+
+Arguments ofe_funC {_} _.
+Notation "A -c> B" :=
+ (@ofe_funC A (λ _, B)) (at level 99, B at level 200, right associativity).
+
+Definition ofe_fun_map {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
+ (g : ofe_fun B1) : ofe_fun B2 := λ x, f _ (g x).
+
+Lemma ofe_fun_map_ext {A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x)
+ (g : ofe_fun B1) :
+ (∀ x, f1 x (g x) ≡ f2 x (g x)) → ofe_fun_map f1 g ≡ ofe_fun_map f2 g.
+Proof. done. Qed.
+Lemma ofe_fun_map_id {A} {B : A → ofeT} (g : ofe_fun B) :
+ ofe_fun_map (λ _, id) g = g.
+Proof. done. Qed.
+Lemma ofe_fun_map_compose {A} {B1 B2 B3 : A → ofeT}
+ (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : ofe_fun B1) :
+ ofe_fun_map (λ x, f2 x ∘ f1 x) g = ofe_fun_map f2 (ofe_fun_map f1 g).
+Proof. done. Qed.
+
+Instance ofe_fun_map_ne {A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
+ (∀ x, Proper (dist n ==> dist n) (f x)) →
+ Proper (dist n ==> dist n) (ofe_fun_map f).
+Proof. by intros ? y1 y2 Hy x; rewrite /ofe_fun_map (Hy x). Qed.
+
+Definition ofe_funC_map {A} {B1 B2 : A → ofeT} (f : ofe_fun (λ x, B1 x -n> B2 x)) :
+ ofe_funC B1 -n> ofe_funC B2 := CofeMor (ofe_fun_map f).
+Instance ofe_funC_map_ne {A} {B1 B2 : A → ofeT} :
+ NonExpansive (@ofe_funC_map A B1 B2).
+Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
+
+Program Definition ofe_funCF {C} (F : C → cFunctor) : cFunctor := {|
+ cFunctor_car A B := ofe_funC (λ c, cFunctor_car (F c) A B);
+ cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, cFunctor_map (F c) fg)
+|}.
+Next Obligation.
+ intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne.
+Qed.
+Next Obligation.
+ intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
+ apply ofe_fun_map_ext=> y; apply cFunctor_id.
+Qed.
+Next Obligation.
+ intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -ofe_fun_map_compose.
+ apply ofe_fun_map_ext=>y; apply cFunctor_compose.
+Qed.
+
+Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
+
+Instance ofe_funCF_contractive {C} (F : C → cFunctor) :
+ (∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F).
+Proof.
+ intros ? A1 A2 B1 B2 n ?? g.
+ by apply ofe_funC_map_ne=>c; apply cFunctor_contractive.
+Qed.
+
(** Constructing isomorphic OFEs *)
Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B → A)
(g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 169b78a66aea71c24160702ae82502477cf9fb16..3721303550b60a3033b1e82ca6cdbe7ef52b203b 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -77,6 +77,12 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
Proof.
rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
+
+Lemma cmra_update_op_l x y : x â‹… y ~~> x.
+Proof. intros n mz. rewrite comm cmra_opM_assoc. apply cmra_validN_op_r. Qed.
+Lemma cmra_update_op_r x y : x â‹… y ~~> y.
+Proof. rewrite comm. apply cmra_update_op_l. Qed.
+
Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
Proof.
intros H n mz Hmz. apply H, Hmz.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 55f213448edb758142cd0a5ed2cd38267a548e6a..5b1521234df9946d8f53dd3609586738f9342251 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -566,9 +566,9 @@ Proof.
apply plainly_intro', impl_intro_r.
by rewrite plainly_and_sep_l' plainly_elim wand_elim_l.
Qed.
-Lemma wand_impl_plainly P Q : (■P -∗ Q) ⊣⊢ (■P → Q).
+Lemma impl_wand_plainly P Q : (■P → Q) ⊣⊢ (■P -∗ Q).
Proof.
- apply (anti_symm (⊢)); [|by rewrite -impl_wand_1].
+ apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
apply impl_intro_l. by rewrite plainly_and_sep_l' wand_elim_r.
Qed.
Lemma plainly_entails_l' P Q : (P ⊢ ■Q) → P ⊢ ■Q ∗ P.
@@ -1029,7 +1029,7 @@ Qed.
Global Instance wand_plain P Q : Plain P → Plain Q → Plain (P -∗ Q)%I.
Proof.
rewrite /Plain=> HP HQ.
- by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
+ by rewrite {2}HP -{1}(plainly_elim P) -!impl_wand_plainly -plainly_impl_plainly -HQ.
Qed.
Global Instance plainly_plain P : Plain (â– P).
Proof. by intros; apply plainly_intro'. Qed.
@@ -1079,7 +1079,7 @@ Global Instance wand_persistent P Q :
Plain P → Persistent Q → Persistent (P -∗ Q)%I.
Proof.
rewrite /Plain /Persistent=> HP HQ.
- by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -persistently_impl_plainly -HQ.
+ by rewrite {2}HP -{1}(plainly_elim P) -!impl_wand_plainly -persistently_impl_plainly -HQ.
Qed.
Global Instance plainly_persistent P : Persistent (â– P).
Proof. by rewrite /Persistent persistently_plainly. Qed.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 2f27f2965702e536f18326ca77b9a1b208d5a944..e08e113f236c46d7cafb29706117a3784490c289 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -72,6 +72,14 @@ Section to_gen_heap.
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap.
+Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+ (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
+Proof.
+ iMod (own_alloc (◠to_gen_heap σ)) as (γ) "Hh".
+ { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+ iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
+Qed.
+
Section gen_heap.
Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index a36fb468200f92a5b9abfa9d628d918c11f7f548..8f1768137509da9551500bee52f1be2bfa3b1fe3 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,5 +1,5 @@
From iris.base_logic Require Export base_logic.
-From iris.algebra Require Import iprod gmap.
+From iris.algebra Require Import gmap.
From iris.algebra Require cofe_solver.
Set Default Proof Using "Type".
@@ -47,7 +47,7 @@ Definition gname := positive.
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition iResF (Σ : gFunctors) : urFunctor :=
- iprodURF (λ i, gmapURF gname (Σ i)).
+ ofe_funURF (λ i, gmapURF gname (Σ i)).
(** We define functions for the empty list of functors, the singleton list of
@@ -116,7 +116,7 @@ construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors → ofeT.
Definition iResUR (Σ : gFunctors) : ucmraT :=
- iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
+ ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Notation iProp Σ := (uPredC (iResUR Σ)).
Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
@@ -134,7 +134,7 @@ Module Export iProp_solution : iProp_solution_sig.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
Definition iResUR (Σ : gFunctors) : ucmraT :=
- iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
+ ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Notation iProp Σ := (uPredC (iResUR Σ)).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 9381789f3f1b0956ee893cc142049b105123fd51..ed1ab6073ee9ca2b54dec5a9a74673be0d8fcdb8 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import iprod gmap.
+From iris.algebra Require Import functions gmap.
From iris.base_logic Require Import big_op.
From iris.base_logic Require Export iprop.
From iris.proofmode Require Import classes.
@@ -49,7 +49,7 @@ Ltac solve_inG :=
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
- iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
+ ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
@@ -68,11 +68,11 @@ Implicit Types a : A.
(** ** Properties of [iRes_singleton] *)
Global Instance iRes_singleton_ne γ :
NonExpansive (@iRes_singleton Σ A _ γ).
-Proof. by intros n a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
+Proof. by intros n a a' Ha; apply ofe_fun_singleton_ne; rewrite Ha. Qed.
Lemma iRes_singleton_op γ a1 a2 :
iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
Proof.
- by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
+ by rewrite /iRes_singleton ofe_fun_op_singleton op_singleton cmra_transport_op.
Qed.
(** ** Properties of [own] *)
@@ -92,7 +92,7 @@ Proof. intros a1 a2. apply own_mono. Qed.
Lemma own_valid γ a : own γ a ⊢ ✓ a.
Proof.
rewrite !own_eq /own_def ownM_valid /iRes_singleton.
- rewrite iprod_validI (forall_elim (inG_id _)) iprod_lookup_singleton.
+ rewrite ofe_fun_validI (forall_elim (inG_id _)) ofe_fun_lookup_singleton.
rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
(* implicit arguments differ a bit *)
by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
@@ -120,7 +120,7 @@ Proof.
intros Ha.
rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌠∧ uPred_ownM m)%I).
- rewrite /uPred_valid ownM_unit.
- eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
+ eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
@@ -137,7 +137,7 @@ Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌠∧ ow
Proof.
intros Ha. rewrite !own_eq.
rewrite -(bupd_mono (∃ m, ⌜∃ a', m = iRes_singleton γ a' ∧ P a'⌠∧ uPred_ownM m)%I).
- - eapply bupd_ownM_updateP, iprod_singleton_updateP;
+ - eapply bupd_ownM_updateP, ofe_fun_singleton_updateP;
first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
@@ -170,7 +170,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
rewrite /uPred_valid ownM_unit !own_eq /own_def.
- apply bupd_ownM_update, iprod_singleton_update_empty.
+ apply bupd_ownM_update, ofe_fun_singleton_update_empty.
apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
- apply cmra_transport_valid, ucmra_unit_valid.
- intros x; destruct inG_prf. by rewrite left_id.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 9b5f721e7e6577d6f646ac315cbeaa85a5e47e48..c8ee4d412e4f54b7c796e81be8b1fed293152e78 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -111,8 +111,7 @@ Proof. iApply saved_anything_alloc. Qed.
Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
Proof.
- iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI.
- iDestruct (ofe_funC_equivI (CofeMor Next ∘ Φ) (CofeMor Next ∘ Ψ)) as "[FE _]".
- simpl. iApply ("FE" with "[-]").
- iApply (saved_anything_agree with "HΦ HΨ").
+ unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
+ iDestruct (saved_anything_agree with "HΦ HΨ") as "Heq".
+ by iDestruct (ofe_fun_equivI with "Heq") as "?".
Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 1e123fa4bb0058bce0980ab3320647fea1a7f2aa..1c718f84d5de23bb9ba1dd0ba929504d4e661fef 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -1,4 +1,5 @@
From iris.base_logic Require Export upred.
+From stdpp Require Import finite.
From iris.algebra Require Export updates.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -651,12 +652,15 @@ Proof.
Qed.
(* Function extensionality *)
-Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof. by unseal. Qed.
Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof. by unseal. Qed.
+Lemma ofe_fun_equivI `{B : A → ofeT} (g1 g2 : ofe_fun B) : g1 ≡ g2 ⊣⊢ ∀ i, g1 i ≡ g2 i.
+Proof. by uPred.unseal. Qed.
+
+Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. by uPred.unseal. Qed.
-(* Sig ofes *)
+(* Sigma OFE *)
Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sigC P) :
x ≡ y ⊣⊢ proj1_sig x ≡ proj1_sig y.
Proof. by unseal. Qed.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index d712d79fd58e028a585de30a5d48338604ee6ada..51529438b392a93878e3f21458f0be2b7982d7fd 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -19,9 +19,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
adequate s e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
- iMod (own_alloc (◠to_gen_heap σ)) as (γ) "Hh".
- { apply: auth_auth_valid. exact: to_gen_heap_valid. }
- iModIntro. iExists (λ σ, own γ (◠to_gen_heap σ)); iFrame.
- set (Hheap := GenHeapG loc val Σ _ _ _ γ).
+ iMod (gen_heap_init σ) as (?) "Hh".
+ iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iApply (Hwp (HeapG _ _ _)).
Qed.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 5e5ad25edc624b67d558a9a201034a0a16d3d68d..f9059566e4b4ded7c276d72aac613f4ece56f56a 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -31,7 +31,7 @@ Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌠∨
- ∃ v, ⌜lv = SOMEV v⌠∗ (Ψ v ∨ own γ (Excl ()))))%I.
+ ∃ w, ⌜lv = SOMEV w⌠∗ (Ψ w ∨ own γ (Excl ()))))%I.
Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 9da9bb33f18ab4a625e29d50eb145b0a82a882e1..23b63251c0c89912fd501d080765eb22d5000196 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -36,7 +36,7 @@ Section proof.
Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
Proof. solve_proper. Qed.
- Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
+ Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
Proof. solve_proper. Qed.
(** The main proofs. *)
@@ -90,6 +90,6 @@ End proof.
Typeclasses Opaque is_lock locked.
-Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
+Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 7a9f78cd88906256508fae367b401f36579d7ee1..7437f74833d1af6324e16db7e7080036bf757e16 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -166,6 +166,6 @@ End proof.
Typeclasses Opaque is_lock issued locked.
-Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
+Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 14ea78575cd670fba6587c31740591cfc6322ff2..3b875bcde56e0342f54b4d2927989350dc79894b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,6 +5,18 @@ From iris.heap_lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
+Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+ e = e' →
+ envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
+Proof. by intros ->. Qed.
+
+Ltac wp_expr_eval t :=
+ try iStartProof;
+ try (eapply tac_wp_expr_eval; [t; reflexivity|]).
+
+Ltac wp_expr_simpl := wp_expr_eval simpl.
+Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
+
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2 →
φ →
@@ -34,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
[apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
- |simpl_subst; try wp_value_head (* new goal *)
+ |wp_expr_simpl_subst; try wp_value_head (* new goal *)
])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'"
@@ -54,15 +66,23 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_match" := wp_case; wp_let.
+<<<<<<< HEAD
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite /envs_entails=> ->. by apply: wp_bind. Qed.
+=======
+Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e f :
+ f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
+ envs_entails Δ (WP e @ E {{ v, WP f (of_val v) @ E {{ Φ }} }})%I →
+ envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
+>>>>>>> master
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
- | _ => apply (tac_wp_bind K); simpl
+ | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
end.
Tactic Notation "wp_bind" open_constr(efoc) :=
@@ -155,7 +175,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+ wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
@@ -174,7 +194,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
|first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split;
[env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
- |simpl; try wp_value_head]]
+ |wp_expr_simpl; try wp_value_head]]
| _ => fail "wp_alloc: not a 'wp'"
end.
@@ -191,7 +211,7 @@ Tactic Notation "wp_load" :=
[apply _
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| _ => fail "wp_load: not a 'wp'"
end.
@@ -207,7 +227,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity
- |simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
+ |wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
| _ => fail "wp_store: not a 'wp'"
end.
@@ -223,7 +243,7 @@ Tactic Notation "wp_cas_fail" :=
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
|try congruence
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
@@ -240,6 +260,6 @@ Tactic Notation "wp_cas_suc" :=
iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
|try congruence
|env_cbv; reflexivity
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 275c98cf4bbe5475d12c532c7381b5d6927c4290..5763c56f0399cf969855deec9db9ea6e92ddf07b 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -229,6 +229,13 @@ End ectx_language.
Arguments ectx_lang : clear implicits.
Coercion ectx_lang : ectxLanguage >-> language.
+(* This definition makes sure that the fields of the [language] record do not
+refer to the projections of the [ectxLanguage] record but to the actual fields
+of the [ectxLanguage] record. This is crucial for canonical structure search to
+work.
+
+Note that this trick no longer works when we switch to canonical projections
+because then the pattern match [let '...] will be desugared into projections. *)
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
@Language E V St of_val to_val _
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 2771e3101b45f042b7d9a192688028b0fca54c30..829e5d3be7248d0f229aee1986b11de2e6e71d21 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -10,6 +10,16 @@ Section LiftingTests.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
+ Definition simpl_test :
+ ⌜(10 = 4 + 6)%nat⌠-∗
+ WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, ⌜v = #1⌠}}.
+ Proof.
+ iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
+ match goal with
+ | |- context [ (10 = 4 + 6)%nat ] => done
+ end.
+ Qed.
+
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 28f75f6c8a26e77a3c6ceea613114910dac6c48e..01441c800708b8ba694685b2b7bfc5ddf8646215 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -40,7 +40,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
{{{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }}}.
Proof.
iIntros (Φ) "[Hl Ht] HΦ".
- iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
+ iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "[$Hl]").