Skip to content
Snippets Groups Projects
Commit 3f321758 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge branch 'jh/upred_alt' into 'master' 

Prove that uPred is complete even if we remove the validity restriction in uPred_closed.

See merge request FP/iris-coq!99
parents bba89517 a603fe3a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
docs/algebra.tex
+ 29
− 16
View file @ 3f321758
......@@ -53,6 +53,16 @@ In particular:
The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
One very important OFE is the OFE of \emph{step-indexed propositions}:
For every step-index, such a proposition either holds or does not hold.
Moreover, if a propositions holds for some $n$, it also has to hold for all smaller step-indices.
\begin{align*}
\SProp \eqdef{}& \psetdown{\nat} \\
\eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y \\
X \nincl{n} Y \eqdef{}& \All m \leq n. m \in X \Ra m \in Y
\end{align*}
\subsection{COFE}
COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains.
......@@ -79,12 +89,14 @@ For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$
This also holds if $f^k$ is contractive for an arbitrary $k$.
Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
$\SProp$ as defined above is complete, \ie it is a COFE.
\subsection{RA}
\begin{defn}
A \emph{resource algebra} (RA) is a tuple \\
$(\monoid, \mval \subseteq \monoid, \mcore{{-}}:
$(\monoid, \mvalFull : \monoid \to \mProp, \mcore{{-}}:
\monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:
\begin{align*}
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\
......@@ -92,16 +104,19 @@ Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkeda
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
\All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
\All \melt, \meltB.& \mvalFull(\melt \mtimes \meltB) \Ra \mvalFull(\melt) \tagH{ra-valid-op} \\
\text{where}\qquad %\qquad\\
\maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
\melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
\end{align*}
\end{defn}
\noindent
Here, $\mProp$ is the set of (meta-level) propositions.
Think of \texttt{Prop} in Coq or $\mathbb{B}$ in classical mathematics.
RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences:
\begin{enumerate}
\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset $\mval$ of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
These valid elements are identified by the \emph{validity predicate} $\mvalFull$.
This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, CMRAs, in the next subsection.
......@@ -122,7 +137,7 @@ Notice also that the core of an RA is a strict generalization of the unit that a
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \maybe{\melt_\f} \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval \]
\[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \mvalFull(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \mvalFull(\maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
......@@ -134,17 +149,15 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\subsection{CMRA}
\begin{defn}
A \emph{CMRA} is a tuple $(\monoid : \OFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
A \emph{CMRA} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
\begin{align*}
\All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
\All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
\All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
\All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
\All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt) \tagH{cmra-valid-op} \\
\All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$n \in \mval(\melt) \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
&\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{cmra-extend} \\
\text{where}\qquad\qquad\\
\melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\
......@@ -154,8 +167,8 @@ Since Iris ensures that the global ghost state is valid, this means that we can
This is a natural generalization of RAs over OFEs.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
\[ \mval \eqdef \bigcap_{n \in \nat} \mval_n \]
We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation:
\[ \mvalFull(\melt) \eqdef \All n. n \in \mval(\melt) \]
\paragraph{The extension axiom (\ruleref{cmra-extend}).}
Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.
......@@ -184,7 +197,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\begin{defn}
An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
\item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
\item $\munit$ is valid: \\ $\All n. n \in \mval(\munit)$
\item $\munit$ is a left-identity of the operation: \\
$\All \melt \in M. \munit \mtimes \melt = \melt$
\item $\munit$ is its own core: \\ $\mcore\munit = \munit$
......@@ -197,7 +210,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All n, \maybe{\melt_\f}. \melt \mtimes \maybe{\melt_\f} \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval_n \]
\[ \All n, \maybe{\melt_\f}. n \in \mval(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. n \in\mval(\meltB \mtimes \maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
......@@ -208,7 +221,7 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update
\begin{enumerate}[itemsep=0pt]
\item $\monoid$ is a discrete COFE
\item $\mval$ ignores the step-index: \\
$\All \melt \in \monoid. \melt \in \mval_0 \Ra \All n, \melt \in \mval_n$
$\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$
\end{enumerate}
\end{defn}
Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
......@@ -223,7 +236,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\item $f$ commutes with the core:\\
$\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$
\item $f$ preserves validity: \\
$\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
$\All n, \melt \in \monoid_1. n \in \mval(\melt) \Ra n \in \mval(f(\melt))$
\end{enumerate}
\end{defn}
......
docs/constructions.tex
+ 37
− 37
View file @ 3f321758
......@@ -21,32 +21,32 @@ $\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
\begin{align*}
\UPred(\monoid) \eqdef{} \setComp{\pred: \nat \times \monoid \to \mProp}{
\begin{inbox}[c]
(\All n, x, y. \pred(n, x) \land x \nequiv{n} y \Ra \pred(n, y)) \land {}\\
(\All n, m, x, y. \pred(n, x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra \pred(m, y))
\end{inbox}
}
\monoid \monnra \SProp \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}
{\All n, \melt, \meltB. \melt \mincl[n] \meltB \Ra \pred(\melt) \nincl{n} \pred(\meltB)} \\
\UPred(\monoid) \eqdef{}& \faktor{\monoid \monnra \SProp}{\equiv} \\
\pred \equiv \predB \eqdef{}& \All m, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff m \in \predB(\melt)) \\
\pred \nequiv{n} \predB \eqdef{}& \All m \le n, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff m \in \predB(\melt))
\end{align*}
where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}.
You can think of uniform predicates as monotone, step-indexed predicates over a CMRA that ``ignore'' invalid elements (as defined by the quotient).
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
One way to understand this definition is to re-write it a little.
We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, the proposition either holds or does not hold.
\begin{align*}
\SProp \eqdef{}& \psetdown{\nat} \\
\eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y
\end{align*}
Notice that this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
We could equivalently require every CMRA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}.
It is worth noting that the above quotient admits canonical
representatives. More precisely, one can show that every
equivalence class contains exactly one element $P_0$ such that:
\[ \All n, \melt. (\mval(\melt) \nincl{n} P_0(\melt)) \Ra n \in P_0(\melt) \tagH{UPred-canonical} \]
Intuitively, this says that $P_0$ trivially holds whenever the resource is invalid.
Starting from any element $P$, one can find this canonical
representative by choosing $P_0(\melt) := \setComp{n}{n \in \mval(\melt) \Ra n \in P(\melt)}$.
Hence, as an alternative definition of $\UPred$, we could use the set
of canonical representatives. This alternative definition would
save us from using a quotient. However, the definitions of the various
connectives would get more complicated, because we have to make sure
they all verify \ruleref{UPred-canonical}, which sometimes requires some adjustments. We
would moreover need to prove one more property for every logical
connective.
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
\begin{align*}
\UPred(\monoid) \cong{}& \monoid \monra \SProp \\
\eqdef{}& \setComp{\pred: \monoid \nfn \SProp}{\All n, m, x, y. n \in \pred(x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra m \in \pred(y)}
\end{align*}
The reason we chose the first definition is that it is easier to work with in Coq.
\clearpage
\section{RA and CMRA constructions}
......@@ -69,16 +69,16 @@ Frame-preserving updates on the $M_i$ lift to the product:
The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
\begin{align*}
\monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\
\mval_n \eqdef{}& \setComp{\cinl(\melt_1)}{\melt_1 \in \mval'_n}
\cup \setComp{\cinr(\melt_2)}{\melt_2 \in \mval''_n} \\
\mval(\mundef) \eqdef{}& \emptyset \\
\mval(\cinl(\melt)) \eqdef{}& \mval_1(\melt) \\
\cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1) \\
% \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
% \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\
\mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases}
\end{align*}
The composition and core for $\cinr$ are defined symmetrically.
Above, $\mval_1$ refers to the validity of $\monoid_1$.
The validity, composition and core for $\cinr$ are defined symmetrically.
The remaining cases of the composition and core are all $\mundef$.
Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this CMRA just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
......@@ -99,7 +99,7 @@ We obtain the following frame-preserving updates, as well as their symmetric cou
{\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}}
\inferH{sum-swap}
{\All \melt_\f, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
{\All \melt_\f \in M, n. n \notin \mval(\melt \mtimes \melt_\f) \and \mvalFull(\meltB)}
{\cinl(\melt) \mupd \cinr(\meltB)}
\end{mathpar}
Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.
......@@ -122,18 +122,18 @@ Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite par
We obtain the following frame-preserving updates:
\begin{mathpar}
\inferH{fpfn-alloc-strong}
{\text{$G$ infinite} \and \melt \in \mval}
{\text{$G$ infinite} \and \mvalFull(\melt)}
{\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}}
\inferH{fpfn-alloc}
{\melt \in \mval}
{\mvalFull(\melt)}
{\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
\inferH{fpfn-update}
{\melt \mupd_\monoid \meltsB}
{\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
Above, $\mval$ refers to the validity of $\monoid$.
Above, $\mvalFull$ refers to the (full) validity of $\monoid$.
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
......@@ -146,7 +146,7 @@ Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
\textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB \\
~\\
% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
\mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ \All x, y \in \melt. x \nequiv{n} y } \\
\mval(\melt) \eqdef{}& \setComp{n}{ \All x, y \in \melt. x \nequiv{n} y } \\
\mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& \melt \cup \meltB
\end{align*}
......@@ -158,11 +158,11 @@ We define a non-expansive injection $\aginj$ into $\agm(\cofe)$ as follows:
\[ \aginj(x) \eqdef \set{x} \]
There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
\begin{mathpar}
\axiomH{ag-val}{\aginj(x) \in \mval_n}
\axiomH{ag-val}{\mvalFull(\aginj(x))}
\axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
\axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Lra x \nequiv{n} y}
\axiomH{ag-agree}{n \in \mval(\aginj(x) \mtimes \aginj(y)) \Ra x \nequiv{n} y}
\end{mathpar}
......@@ -171,7 +171,7 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
Given an OFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
\begin{align*}
\exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
\mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \mundef}
\mval(\melt) \eqdef{}& \setComp{n}{\melt \neq \mundef}
\end{align*}
All cases of composition go to $\mundef$.
\begin{align*}
......@@ -281,7 +281,7 @@ We assume that $M$ has a unit $\munit$, and hence its core is total.
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
\begin{align*}
\authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\
\mval_n \eqdef{}& \setComp{ (x, \meltB) \in \authm(M) }{ \meltB \in \mval_n \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ n \in \mval(\meltB) \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
(x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\
\mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\
(x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2
......@@ -295,7 +295,7 @@ The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
\[ \All n, \maybe{\melt_\f}. \melt_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
\[ \All n, \maybe{\melt_\f}. n \in \mval(\melt_1) \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra n \in \mval(\melt_2) \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
......@@ -327,7 +327,7 @@ We further define \emph{closed} sets of states (given a particular set of tokens
The STS RA is defined as follows
\begin{align*}
\monoid \eqdef{}& \STSauth(s:\STSS, T:\wp(\STST) \mid \STSL(s) \disj T) \mid{}\\& \STSfrag(S: \wp(\STSS), T: \wp(\STST) \mid \STSclsd(S, T) \land S \neq \emptyset) \mid \mundef \\
\mval \eqdef{}& \setComp{\melt\in\monoid}{\melt \neq \mundef} \\
\mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
\STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
\STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\
\mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
......
docs/iris.sty
+ 2
− 1
View file @ 3f321758
......@@ -36,7 +36,7 @@
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }
\newcommand{\spac}{\,} % a space
\newcommand{\spac}{\hskip 0.2em plus 0.1em} % a space
\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
......@@ -117,6 +117,7 @@
\newcommand{\wtt}[2]{#1 : #2} % well-typed term
\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
\newcommand{\nincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\subseteq}}}}
\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
......
docs/model.tex
+ 4
− 4
View file @ 3f321758
......@@ -42,7 +42,7 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
\Sem{\vctx \proves \prop \Ra \propB : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\
\All m, \meltB.& m \leq n \land \melt \mincl \meltB \land m \in \mval(\meltB) \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
\Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
......@@ -54,15 +54,15 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\\
\Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\
\All m, \meltB.& m \leq n \land m \in \mval(\melt\mtimes\meltB) \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 \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 \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \mval(\Sem{\vctx \proves \term : \textlog{M}}_\gamma) \\
\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)
\All m, \melt'. & m \leq n \land m \in \mval(\melt \mtimes \melt') \Ra {}\\& \Exists \meltB. m \in \mval(\meltB \mtimes \melt') \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
\end{aligned}
}
\end{align*}
......
theories/base_logic/double_negation.v
+ 35
− 36
View file @ 3f321758
......@@ -30,11 +30,11 @@ Import uPred.
Lemma laterN_big n a x φ: ✓{n} x → a ≤ n → (▷^a ⌜φ⌝)%I n x → φ.
Proof.
induction 2 as [| ?? IHle].
- induction a; repeat (rewrite //= || uPred.unseal).
- induction a; repeat (rewrite //= || uPred.unseal).
intros Hlater. apply IHa; auto using cmra_validN_S.
move:Hlater; repeat (rewrite //= || uPred.unseal).
move:Hlater; repeat (rewrite //= || uPred.unseal).
- intros. apply IHle; auto using cmra_validN_S.
eapply uPred_closed; eauto using cmra_validN_S.
eapply uPred_mono; eauto using cmra_validN_S.
Qed.
Lemma laterN_small n a x φ: ✓{n} x → n < a → (▷^a ⌜φ⌝)%I n x.
......@@ -46,15 +46,15 @@ Proof.
- induction n as [| n IHn]; [| move: IHle];
repeat (rewrite //= || uPred.unseal).
red; rewrite //=. intros.
eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S.
eapply (uPred_mono _ _ (S n)); eauto using cmra_validN_S.
Qed.
(* It is easy to show that most of the basic properties of bupd that
are used throughout Iris hold for nnupd.
are used throughout Iris hold for nnupd.
In fact, the first three properties that follow hold for any
modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation
here is slightly different, because nnupd is of the form
here is slightly different, because nnupd is of the form
∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly.
*)
......@@ -77,8 +77,8 @@ Proof.
Qed.
Lemma nnupd_ownM_updateP x (Φ : M → Prop) :
x ~~>: Φ → uPred_ownM x =n=> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
Proof.
intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal.
Proof.
intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal.
intros n y ? Hown a.
red; rewrite //= => n' yf ??.
inversion Hown as (x'&Hequiv).
......@@ -87,18 +87,18 @@ Proof.
case (decide (a ≤ n')).
- intros Hle Hwand.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' (y' ⋅ x'))); eauto.
* rewrite comm -assoc. done.
* rewrite comm -assoc. done.
* eexists. split; eapply uPred_mono; red; rewrite //=; eauto.
- intros; assert (n' < a). omega.
* rewrite comm -assoc. done.
* rewrite comm -assoc. done.
* exists y'. split=>//. by exists x'.
- intros; assert (n' < a). omega.
move: laterN_small. uPred.unseal.
naive_solver.
Qed.
(* However, the transitivity property seems to be much harder to
prove. This is surprising, because transitivity does hold for
prove. This is surprising, because transitivity does hold for
modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify
now over n?
now over n?
*)
Remark nnupd_trans P: (|=n=> |=n=> P) ⊢ (|=n=> P).
......@@ -111,7 +111,7 @@ Proof.
(* Oops -- the exponents of the later modality don't match up! *)
Abort.
(* Instead, we will need to prove this in the model. We start by showing that
(* Instead, we will need to prove this in the model. We start by showing that
nnupd is the limit of a the following sequence:
(- -∗ False) - ∗ False,
......@@ -121,12 +121,12 @@ Abort.
Then, it is easy enough to show that each of the uPreds in this sequence
is transitive. It turns out that this implies that nnupd is transitive. *)
(* The definition of the sequence above: *)
Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
((P -∗ ▷^k False) -∗ ▷^k False) ∧
match k with
match k with
O => True
| S k' => uPred_nnupd_k k' P
end.
......@@ -138,11 +138,11 @@ Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
(* One direction of the limiting process is easy -- nnupd implies nnupd_k for each k *)
Lemma nnupd_trunc1 k P: (|=n=> P) ⊢ |=n=>_k P.
Proof.
induction k.
- rewrite /uPred_nnupd_k /uPred_nnupd.
induction k.
- rewrite /uPred_nnupd_k /uPred_nnupd.
rewrite (forall_elim 0) //= right_id //.
- simpl. apply and_intro; auto.
rewrite /uPred_nnupd.
rewrite /uPred_nnupd.
rewrite (forall_elim (S k)) //=.
Qed.
......@@ -190,11 +190,10 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
*** intros. exfalso. assert (n ≤ k'). omega.
assert (n = S k ∨ n < S k) as [->|] by omega.
**** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
**** move:nnupd_k_elim. unseal. intros Hnnupdk.
**** move:nnupd_k_elim. unseal. intros Hnnupdk.
eapply laterN_big; eauto. unseal.
eapply (Hnnupdk n k); first omega; eauto.
exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
eapply cmra_validN_op_l; eauto.
exists x, x'. split_and!; eauto. eapply uPred_mono; eauto.
** intros HP. eapply IHk; auto.
move:HP. unseal. intros (?&?); naive_solver.
Qed.
......@@ -204,13 +203,13 @@ Lemma nnupd_k_intro k P: P ⊢ (|=n=>_k P).
Proof.
induction k; rewrite //= ?right_id.
- apply wand_intro_l. apply wand_elim_l.
- apply and_intro; auto.
- apply and_intro; auto.
apply wand_intro_l. apply wand_elim_l.
Qed.
Lemma nnupd_k_mono k P Q: (P ⊢ Q) → (|=n=>_k P) ⊢ (|=n=>_k Q).
Proof.
induction k; rewrite //= ?right_id=>HPQ.
induction k; rewrite //= ?right_id=>HPQ.
- do 2 (apply wand_mono; auto).
- apply and_mono; auto; do 2 (apply wand_mono; auto).
Qed.
......@@ -228,13 +227,13 @@ Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P).
Proof.
revert P.
induction k; intros P.
- rewrite //= ?right_id. apply wand_intro_l.
- rewrite //= ?right_id. apply wand_intro_l.
rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r.
- rewrite {2}(nnupd_k_unfold k P).
apply and_intro.
* rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
rewrite nnupd_k_unfold. rewrite and_elim_l.
apply wand_intro_l.
apply wand_intro_l.
rewrite {1}(nnupd_k_intro (S k) (P -∗ ▷^(S k) (False)%I)).
rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
* do 2 rewrite nnupd_k_weaken //.
......@@ -263,8 +262,8 @@ Proof.
case (decide (a ≤ n')).
- intros Hle Hwand.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
* rewrite comm. done.
* rewrite comm. done.
* rewrite comm. done.
* rewrite comm. done.
- intros; assert (n' < a). omega.
move: laterN_small. uPred.unseal.
naive_solver.
......@@ -300,23 +299,23 @@ End classical.
Lemma nnupd_dne φ: (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I.
Proof.
rewrite /uPred_nnupd. apply forall_intro=>n.
apply wand_intro_l. rewrite ?right_id.
apply wand_intro_l. rewrite ?right_id.
assert (∀ φ, ¬¬¬¬φ → ¬¬φ) by naive_solver.
assert (Hdne: ¬¬ (¬¬φ → φ)) by naive_solver.
split. unseal. intros n' ?? Hupd.
case (decide (n' < n)).
- intros. move: laterN_small. unseal. naive_solver.
- intros. assert (n ≤ n'). omega.
- intros. assert (n ≤ n'). omega.
exfalso. specialize (Hupd n' ε).
eapply Hdne. intros Hfal.
eapply laterN_big; eauto.
eapply laterN_big; eauto.
unseal. rewrite right_id in Hupd *; naive_solver.
Qed.
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
under classical axioms) directly without passing through the proofs for bupd: *)
Lemma adequacy_helper1 P n k x:
✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x)
✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x)
→ ¬¬ (∃ x', ✓{n + k} (x') ∧ Nat.iter n (λ P, |=n=> ▷ P)%I P (n + k) (x')).
Proof.
revert k P x. induction n.
......@@ -326,12 +325,12 @@ Proof.
specialize (Hf3 (S k) (S k) ε). rewrite right_id in Hf3 *. unseal.
intros Hf3. eapply Hf3; eauto.
intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
unseal.
unseal.
assert (n' < S k ∨ n' = S k) as [|] by omega.
* intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
eapply Hsmall; eauto.
* subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
- intros k P x Hx. rewrite ?Nat_iter_S_r.
- intros k P x Hx. rewrite ?Nat_iter_S_r.
replace (S (S n) + k) with (S n + (S k)) by omega.
replace (S n + k) with (n + (S k)) by omega.
intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by omega. eauto.
......@@ -339,7 +338,7 @@ Proof.
Qed.
Lemma adequacy_helper2 P n k x:
✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x)
✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x)
→ ¬¬ (∃ x', ✓{k} (x') ∧ Nat.iter 0 (λ P, |=n=> ▷ P)%I P k (x')).
Proof.
revert x. induction n.
......
theories/base_logic/primitive.v
+ 19
− 34
View file @ 3f321758
......@@ -35,11 +35,10 @@ Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Next Obligation.
intros M P Q n1 x1 x1' HPQ [x2 Hx1'] n2 x3 [x4 Hx3] ?; simpl in *.
intros M P Q n1 n1' x1 x1' HPQ [x2 Hx1'] Hn1 n2 x3 [x4 Hx3] ?; simpl in *.
rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
eapply HPQ; auto. exists (x2 ⋅ x4); by rewrite assoc.
Qed.
Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. Qed.
Definition uPred_impl {M} := unseal uPred_impl_aux M.
Definition uPred_impl_eq :
......@@ -71,14 +70,9 @@ Definition uPred_internal_eq_eq:
Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Next Obligation.
intros M P Q n x y (x1&x2&Hx&?&?) [z Hy].
intros M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_includedN_l.
by rewrite Hy Hx assoc.
Qed.
Next Obligation.
intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
exists x1, x2; ofe_subst; split_and!;
eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
eapply dist_le, Hn. by rewrite Hy Hx assoc.
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed.
Definition uPred_sep {M} := unseal uPred_sep_aux M.
......@@ -88,11 +82,10 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Next Obligation.
intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
apply uPred_mono with (x1 ⋅ x3);
intros M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in *.
eapply uPred_mono with n3 (x1 ⋅ x3);
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. Qed.
Definition uPred_wand {M} := unseal uPred_wand_aux M.
Definition uPred_wand_eq :
......@@ -103,7 +96,7 @@ Definition uPred_wand_eq :
because Iris is afine. The following is easier to work with. *)
Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_closed, ucmra_unit_validN.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
Definition uPred_plainly {M} := unseal uPred_plainly_aux M.
Definition uPred_plainly_eq :
......@@ -114,7 +107,6 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed.
Definition uPred_persistently {M} := unseal uPred_persistently_aux M.
Definition uPred_persistently_eq :
......@@ -123,10 +115,7 @@ Definition uPred_persistently_eq :
Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation.
intros M P [|n] x1 x2; eauto using uPred_mono, cmra_includedN_S.
Qed.
Next Obligation.
intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia.
intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
Qed.
Definition uPred_later_aux : seal (@uPred_later_def). by eexists. Qed.
Definition uPred_later {M} := unseal uPred_later_aux M.
......@@ -136,10 +125,9 @@ Definition uPred_later_eq :
Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
Next Obligation.
intros M a n x1 x [a' Hx1] [x2 ->].
exists (a' ⋅ x2). by rewrite (assoc op) Hx1.
intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn. eapply cmra_includedN_le=>//.
exists (a' ⋅ x2). by rewrite Hx(assoc op) Hx1.
Qed.
Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed.
Definition uPred_ownM {M} := unseal uPred_ownM_aux M.
Definition uPred_ownM_eq :
......@@ -157,13 +145,12 @@ Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ k yf,
k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
Next Obligation.
intros M Q n x1 x2 HQ [x3 Hx] k yf Hk.
intros M Q n1 n2 x1 x2 HQ [x3 Hx] Hn k yf Hk.
rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy.
destruct (HQ k (x3 ⋅ yf)) as (x'&?&?); [auto|by rewrite assoc|].
exists (x' ⋅ x3); split; first by rewrite -assoc.
apply uPred_mono with x'; eauto using cmra_includedN_l.
eauto using uPred_mono, cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
......@@ -380,7 +367,7 @@ Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
Proof.
unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
naive_solver eauto using uPred_mono, cmra_included_includedN.
Qed.
Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
......@@ -432,7 +419,7 @@ Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
Proof.
unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
exists x, x'; split_and?; auto.
eapply uPred_closed with n; eauto using cmra_validN_op_l.
eapply uPred_mono with n x; eauto using cmra_validN_op_l.
Qed.
Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
Proof.
......@@ -486,14 +473,14 @@ Qed.
Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
Proof.
unseal; split=> /= n x ? HPQ n' x' ????.
eapply uPred_mono with (core x), cmra_included_includedN; auto.
eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
apply (HPQ n' x); eauto using cmra_validN_le.
Qed.
Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
Proof.
unseal; split=> /= n x ? HPQ n' x' ????.
eapply uPred_mono with ε, cmra_included_includedN; auto.
eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
apply (HPQ n' x); eauto using cmra_validN_le.
Qed.
......@@ -505,7 +492,7 @@ Qed.
Lemma löb P : (▷ P → P) ⊢ P.
Proof.
unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
apply HP, IH, uPred_mono with (S n) x; eauto using cmra_validN_S.
Qed.
Lemma later_forall_2 {A} (Φ : A → uPred M) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
Proof. unseal; by split=> -[|n] x. Qed.
......@@ -526,8 +513,7 @@ Qed.
Lemma later_false_excluded_middle P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
Proof.
unseal; split=> -[|n] x ? /= HP; [by left|right].
intros [|n'] x' ????; [|done].
eauto using uPred_closed, uPred_mono, cmra_included_includedN.
intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
Qed.
Lemma persistently_later P : □ ▷ P ⊣⊢ ▷ □ P.
Proof. by unseal. Qed.
......@@ -577,7 +563,7 @@ Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
Lemma bupd_intro P : P ==∗ P.
Proof.
unseal. split=> n x ? HP k yf ?; exists x; split; first done.
apply uPred_closed with n; eauto using cmra_validN_op_l.
apply uPred_mono with n x; eauto using cmra_validN_op_l.
Qed.
Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==∗ Q.
Proof.
......@@ -593,8 +579,7 @@ Proof.
destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
exists (x' ⋅ x2); split; first by rewrite -assoc.
exists x', x2; split_and?; auto.
apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
Qed.
Lemma bupd_ownM_updateP x (Φ : M → Prop) :
x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
......
theories/base_logic/upred.v
+ 63
− 43
View file @ 3f321758
......@@ -6,43 +6,46 @@ Set Default Proof Using "Type".
base_logic.base_logic; that will also give you all the primitive
and many derived laws for the logic. *)
(* A good way of understanding this definition of the uPred OFE is to
consider the OFE uPred0 of monotonous SProp predicates. That is,
uPred0 is the OFE of non-expansive functions from M to SProp that
are monotonous with respect to CMRA inclusion. This notion of
monotonicity has to be stated in the SProp logic. Together with the
usual closedness property of SProp, this gives exactly uPred_mono.
Then, we quotient uPred0 *in the sProp logic* with respect to
equivalence on valid elements of M. That is, we quotient with
respect to the following *sProp* equivalence relation:
P1 ≡ P2 := ∀ x, ✓ x → (P1(x) ↔ P2(x)) (1)
When seen from the ambiant logic, obtaining this quotient requires
definig both a custom Equiv and Dist.
It is worth noting that this equivalence relation admits canonical
representatives. More precisely, one can show that every
equivalence class contains exactly one element P0 such that:
∀ x, (✓ x → P0(x)) → P0(x) (2)
(Again, this assertion has to be understood in sProp). Intuitively,
this says that P0 trivially holds whenever the resource is invalid.
Starting from any element P, one can find this canonical
representative by choosing:
P0(x) := ✓ x → P(x) (3)
Hence, as an alternative definition of uPred, we could use the set
of canonical representatives (i.e., the subtype of monotonous
sProp predicates that verify (2)). This alternative definition would
save us from using a quotient. However, the definitions of the various
connectives would get more complicated, because we have to make sure
they all verify (2), which sometimes requires some adjustments. We
would moreover need to prove one more property for every logical
connective.
*)
Record uPred (M : ucmraT) : Type := IProp {
uPred_holds :> nat → M → Prop;
(* [uPred_mono] is used to prove non-expansiveness (guaranteed by
[uPred_ne]). Therefore, it is important that we do not restrict
it to only valid elements. *)
uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
(* We have to restrict this to hold only for valid elements,
otherwise this condition is no longer limit preserving, and uPred
does no longer form a COFE (i.e., [uPred_compl] breaks). This is
because the distance and equivalence on this cofe ignores the
truth value on invalid elements. This, in turn, is required by
the fact that entailment has to ignore invalid elements, which is
itself essential for proving [ownM_valid].
We could, actually, remove this restriction and make this
condition apply even to invalid elements: we have proved that
uPred is isomorphic to a sub-COFE of the COFE of predicates that
are monotonous both with respect to the step index and with
respect to x. However, that would essentially require changing
(by making it more complicated) the model of many connectives of
the logic, which we don't want.
This sub-COFE is the sub-COFE of monotonous sProp predicates P
such that the following sProp assertion is valid:
∀ x, (V(x) → P(x)) → P(x)
Where V is the validity predicate.
Another way of saying that this is equivalent to this definition of
uPred is to notice that our definition of uPred is equivalent to
quotienting the COFE of monotonous sProp predicates with the
following (sProp) equivalence relation:
P1 ≡ P2 := ∀ x, V(x) → (P1(x) ↔ P2(x))
whose equivalence classes appear to all have one only canonical
representative such that ∀ x, (V(x) → P(x)) → P(x).
*)
uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
uPred_mono n1 n2 x1 x2 :
uPred_holds n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.
Arguments uPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred.
......@@ -77,15 +80,17 @@ Section cofe.
Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.
Program Definition uPred_compl : Compl uPredC := λ c,
{| uPred_holds n x := c n n x |}.
Next Obligation. naive_solver eauto using uPred_mono. Qed.
{| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'}x → c n' n' x |}.
Next Obligation.
intros c n1 n2 x ???; simpl in *.
apply (chain_cauchy c n2 n1); eauto using uPred_closed.
move=> /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono.
eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
eapply cmra_includedN_le=>//; lia. done.
Qed.
Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}.
Next Obligation.
intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
intros n c; split=>i x Hin Hv.
etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
Qed.
End cofe.
Arguments uPredC : clear implicits.
......@@ -100,8 +105,24 @@ Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
P ≡{n2}≡ Q → n2 ≤ n1 → ✓{n2} x → Q n1 x → P n2 x.
Proof.
intros [Hne] ???. eapply Hne; try done.
eapply uPred_closed; eauto using cmra_validN_le.
intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
Qed.
(* Equivalence to the definition of uPred in the appendix. *)
Lemma uPred_alt {M : ucmraT} (P: nat → M → Prop) :
(∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → P n2 x2) ↔
( (∀ x n1 n2, n2 ≤ n1 → P n1 x → P n2 x) (* Pointwise down-closed *)
∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ≤ n → P m x1 ↔ P m x2) (* Non-expansive *)
∧ (∀ n x1 x2, x1 ≼{n} x2 → ∀ m, m ≤ n → P m x1 → P m x2) (* Monotonicity *)
).
Proof.
(* Provide this lemma to eauto. *)
assert (∀ n1 n2 (x1 x2 : M), n2 ≤ n1 → x1 ≡{n1}≡ x2 → x1 ≼{n2} x2).
{ intros ????? H. eapply cmra_includedN_le; last done. by rewrite H. }
(* Now go ahead. *)
split.
- intros Hupred. repeat split; eauto using cmra_includedN_le.
- intros (Hdown & _ & Hmono) **. eapply Hmono; [done..|]. eapply Hdown; done.
Qed.
(** functor *)
......@@ -109,7 +130,6 @@ Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CmraMorphism f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
Next Obligation. naive_solver eauto using uPred_closed, cmra_morphism_validN. Qed.
Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
......@@ -167,7 +187,7 @@ Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Hint Resolve uPred_mono uPred_closed : uPred_def.
Hint Resolve uPred_mono : uPred_def.
(** Notations *)
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment