Forked from
Iris / Iris
2823 commits behind the upstream repository.
base-logic.tex 15.47 KiB
\section{Base Logic}
\label{sec:base-logic}
The base logic is parameterized by an arbitrary camera $\monoid$ having a unit $\munit$.
By \lemref{lem:camera-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.
This defines the structure of resources that can be owned.
As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
You have to make sure that $\SigType$ includes the base types:
\[
\SigType \supseteq \{ \textlog{M}, \Prop \}
\]
Elements of $\SigType$ are ranged over by $\sigtype$.
Each function symbol in $\SigFn$ has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ types $\type$ (the grammar of $\type$ is defined below, and depends only on $\SigType$).
We write
\[
\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn
\]
to express that $\sigfn$ is a function symbol with the indicated arity.
Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type $\Prop$.
Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$.
Elements of $\SigAx$ are ranged over by $\sigax$.
\subsection{Grammar}\label{sec:grammar}
\paragraph{Syntax.}
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\Var$ of variables (ranged over by metavariables $\var$, $\varB$, $\varC$).
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
\\&
\FALSE \mid
\TRUE \mid
\term =_\type \term \mid
\prop \Ra \prop \mid
\prop \land \prop \mid
\prop \lor \prop \mid
\prop * \prop \mid
\prop \wand \prop \mid
\\&
\MU \var:\type. \term \mid
\Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid
%\\&
\ownM{\term} \mid \mval(\term) \mid
\always\prop \mid
\plainly\prop \mid
{\later\prop} \mid
\upd \prop
\end{align*}
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$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
\paragraph{Variable conventions.}
We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence.
\subsection{Types}\label{sec:types}
Iris terms are simply-typed.
The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$.
A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types.
In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$.
\judgment[Well-typed terms]{\vctx \proves_\Sig \wtt{\term}{\type}}
\begin{mathparpagebreakable}
%%% variables and function symbols
\axiom{x : \type \proves \wtt{x}{\type}}
\and
\infer{\vctx \proves \wtt{\term}{\type}}
{\vctx, x:\type' \proves \wtt{\term}{\type}}
\and
\infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}}
{\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}}
\and
\infer{\vctx_1, x:\type', y:\type'', \vctx_2 \proves \wtt{\term}{\type}}
{\vctx_1, x:\type'', y:\type', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\type}}
\and
\infer{
\vctx \proves \wtt{\term_1}{\type_1} \and
\cdots \and
\vctx \proves \wtt{\term_n}{\type_n} \and
\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn
}{
\vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}}
}
%%% 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
\infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}}
{\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}
\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'}}
{\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}}
\and
\infer
{\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}}
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
\infer{}{\vctx \proves \wtt\melt{\textlog{M}}}
\and
\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}}
{\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}}
%%% props and predicates
\\
\axiom{\vctx \proves \wtt{\FALSE}{\Prop}}
\and
\axiom{\vctx \proves \wtt{\TRUE}{\Prop}}
\and
\infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}}
{\vctx \proves \wtt{\term =_\type \termB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \Ra \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \land \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \lor \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop * \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \wand \propB}{\Prop}}
\and
\infer{
\vctx, \var:\type \proves \wtt{\term}{\type} \and
\text{$\var$ is guarded in $\term$} \and
\text{$\type$ is complete and inhabited}
}{
\vctx \proves \wtt{\MU \var:\type. \term}{\type}
}
\and
\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}}
\and
\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\ownM{\melt}}{\Prop}}
\and
\infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a camera}}
{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
\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}}
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop}
}{
\vctx \proves \wtt{\upd \prop}{\Prop}
}
\end{mathparpagebreakable}
\subsection{Proof Rules}
\label{sec:proof-rules}
The judgment $\vctx \mid \prop \proves \propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds.
Most of the rules will entirely omit the variable contexts $\vctx$.
In this case, we assume the same arbitrary context is used for every constituent of the rules.
%Furthermore, an arbitrary \emph{boxed} proposition context $\always\pfctx$ may be added to every constituent.
Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ are proof rules of the logic.
\judgment{\vctx \mid \prop \proves \propB}
\paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard.
\begin{mathparpagebreakable}
\infer[Asm]
{}
{\prop \proves \prop}
\and
\infer[Cut]
{\prop \proves \propB \and \propB \proves \propC}
{\prop \proves \propC}
\and
\infer[Eq]
{\vctx,\var:\type \proves \wtt\propB\Prop \\ \vctx\mid\prop \proves \propB[\term/\var] \\ \vctx\mid\prop \proves \term =_\type \term'}
{\vctx\mid\prop \proves \propB[\term'/\var]}
\and
\infer[Refl]
{}
{\TRUE \proves \term =_\type \term}
\and
\infer[$\bot$E]
{}
{\FALSE \proves \prop}
\and
\infer[$\top$I]
{}
{\prop \proves \TRUE}
\and
\infer[$\wedge$I]
{\prop \proves \propB \\ \prop \proves \propC}
{\prop \proves \propB \land \propC}
\and
\infer[$\wedge$EL]
{\prop \proves \propB \land \propC}
{\prop \proves \propB}
\and
\infer[$\wedge$ER]
{\prop \proves \propB \land \propC}
{\prop \proves \propC}
\and
\infer[$\vee$IL]
{\prop \proves \propB }
{\prop \proves \propB \lor \propC}
\and
\infer[$\vee$IR]
{\prop \proves \propC}
{\prop \proves \propB \lor \propC}
\and
\infer[$\vee$E]
{\prop \proves \propC \\
\propB \proves \propC}
{\prop \lor \propB \proves \propC}
\and
\infer[$\Ra$I]
{\prop \land \propB \proves \propC}
{\prop \proves \propB \Ra \propC}
\and
\infer[$\Ra$E]
{\prop \proves \propB \Ra \propC \\ \prop \proves \propB}
{\prop \proves \propC}
\and
\infer[$\forall$I]
{ \vctx,\var : \type\mid\prop \proves \propB}
{\vctx\mid\prop \proves \All \var: \type. \propB}
\and
\infer[$\forall$E]
{\vctx\mid\prop \proves \All \var :\type. \propB \\
\vctx \proves \wtt\term\type}
{\vctx\mid\prop \proves \propB[\term/\var]}
\\
\infer[$\exists$I]
{\vctx\mid\prop \proves \propB[\term/\var] \\
\vctx \proves \wtt\term\type}
{\vctx\mid\prop \proves \exists \var: \type. \propB}
\and
\infer[$\exists$E]
{\vctx,\var : \type\mid\prop \proves \propB}
{\vctx\mid\Exists \var: \type. \prop \proves \propB}
% \and
% \infer[$\lambda$]
% {}
% {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
% \and
% \infer[$\mu$]
% {}
% {\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, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$.
\paragraph{Laws of (affine) bunched implications.}
\begin{mathpar}
\begin{array}{rMcMl}
\TRUE * \prop &\provesIff& \prop \\
\prop * \propB &\proves& \propB * \prop \\
(\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)
\end{array}
\and
\infer[$*$-mono]
{\prop_1 \proves \propB_1 \and
\prop_2 \proves \propB_2}
{\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
\and
\inferB[$\wand$I-E]
{\prop * \propB \proves \propC}
{\prop \proves \propB \wand \propC}
\end{mathpar}
\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}
\inferhref{$\always$-mono}{pers-mono}
{\prop \proves \propB}
{\always{\prop} \proves \always{\propB}}
\and
\inferhref{$\always$-E}{pers-elim}
{}
{\always\prop \proves \prop}
\and
\begin{array}[c]{rMcMl}
(\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB
\end{array}
\and
\begin{array}[c]{rMcMl}
\always{\prop} &\proves& \always\always\prop \\
\All x. \always{\prop} &\proves& \always{\All x. \prop} \\
\always{\Exists x. \prop} &\proves& \Exists x. \always{\prop}
\end{array}
\end{mathpar}
\paragraph{Laws for the later modality.}
\begin{mathpar}
\inferhref{$\later$-mono}{later-mono}
{\prop \proves \propB}
{\later\prop \proves \later{\propB}}
\and
\inferhref{$\later$-I}{later-intro}
{}
{\prop \proves \later\prop}
\and
\begin{array}[c]{rMcMl}
\All x. \later\prop &\proves& \later{\All x.\prop} \\
\later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop} \\
\later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)
\end{array}
\and
\begin{array}[c]{rMcMl}
\later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
\always{\later\prop} &\provesIff& \later\always{\prop} \\
\plainly{\later\prop} &\provesIff& \later\plainly{\prop}
\end{array}
\end{mathpar}
\paragraph{Laws for resources and validity.}
\begin{mathpar}
\begin{array}{rMcMl}
\ownM{\melt} * \ownM{\meltB} &\provesIff& \ownM{\melt \mtimes \meltB} \\
\ownM\melt &\proves& \always{\ownM{\mcore\melt}} \\
\TRUE &\proves& \ownM{\munit} \\
\later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB)
\end{array}
% \and
% \infer[valid-intro]
% {\melt \in \mval}
% {\TRUE \vdash \mval(\melt)}
% \and
% \infer[valid-elim]
% {\melt \notin \mval_0}
% {\mval(\melt) \proves \FALSE}
\and
\begin{array}{rMcMl}
\ownM{\melt} &\proves& \mval(\melt) \\
\mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\
\mval(\melt) &\proves& \plainly\mval(\melt)
\end{array}
\end{mathpar}
\paragraph{Laws for the basic update modality.}
\begin{mathpar}
\inferH{upd-mono}
{\prop \proves \propB}
{\upd\prop \proves \upd\propB}
\inferhref{upd-I}{upd-intro}
{}{\prop \proves \upd \prop}
\inferH{upd-trans}
{}
{\upd \upd \prop \proves \upd \prop}
\inferH{upd-frame}
{}{\propB * \upd\prop \proves \upd (\propB * \prop)}
\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 do not actually have $\in$ inside the logic...}
\subsection{Consistency}
The consistency statement of the logic reads as follows: For any $n$, we have
\begin{align*}
\lnot(\TRUE \proves (\later)^n\spac\FALSE)
\end{align*}
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$ 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:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: