diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index f0b97ad9c950ade18eae79cfd362e1052dca58d4..8f0a53269e5578505ca4cdb5b3ced605fdb71a75 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
+ \var \bm\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
@@ -67,7 +74,10 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
{\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$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
@@ -106,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
@@ -115,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'}}
@@ -125,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
@@ -157,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}
}
@@ -286,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.}
@@ -317,8 +339,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\plainly\prop \proves \always\prop}
\and
\begin{array}[c]{rMcMl}
- \TRUE &\proves& \plainly{\TRUE} \\
- (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q)
+ (\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}
@@ -326,8 +348,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\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}
+%\and
+%\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
\end{mathpar}
\paragraph{Laws for the persistence modality.}
@@ -340,8 +362,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\always\prop \proves \prop}
\and
\begin{array}[c]{rMcMl}
- \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
- (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)
+ (\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}
@@ -358,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
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.