diff --git a/docs/derived.tex b/docs/derived.tex index cab6b22f68579360d6e8f12187868f6a508f9ccb..6e101413cce734cd9008f1707cb2c28e3a6dd7ab 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -1,8 +1,40 @@ -\section{Derived proof rules} +\section{Derived proof rules and other constructions} \subsection{Base logic} -\ralf{Give the most important derived rules.} +We collect here some important and frequently used derived proof rules. +\begin{mathparpagebreakable} + \infer{} + {\prop \Ra \propB \proves \prop \wand \propB} + + \infer{} + {\prop * \Exists\var.\propB \Lra \Exists\var. \prop * \propB} + + \infer{} + {\prop * \Exists\var.\propB \proves \Exists\var. \prop * \propB} + + \infer{} + {\always(\prop*\propB) \Lra \always\prop * \always\propB} + + \infer{} + {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB} + + \infer{} + {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB} + + \infer{} + {\always(\prop \wand \propB) \Lra \always(\prop \Ra \propB)} + + \infer{} + {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB} + + \infer{} + {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB} + + \infer + {\pfctx, \later\prop \proves \prop} + {\pfctx \proves \prop} +\end{mathparpagebreakable} \paragraph{Persistent assertions.} \begin{defn} @@ -40,8 +72,6 @@ We can show that the following additional closure properties hold for timeless a \subsection{Program logic} -\ralf{Sync this with Coq.} - Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively: \[ \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}{\lambda\Ret\val.\propB}[\mask])} @@ -169,12 +199,9 @@ The following rules can be derived for Hoare triples. {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} \end{mathparpagebreakable} -\clearpage -\section{Derived constructions} - -In this section we describe some derived constructions that are generally useful and language-independent. +\subsection{Global Functor and ghost ownership} +\ralf{Describe this.} -\ralf{Describe at least global monoid and invariant namespaces.} % \subsection{Global monoid} % Hereinafter we assume the global monoid (served up as a parameter to Iris) is obtained from a family of monoids $(M_i)_{i \in I}$ by first applying the construction for finite partial functions to each~(\Sref{sec:fpfunm}), and then applying the product construction~(\Sref{sec:prodm}): @@ -206,6 +233,9 @@ In this section we describe some derived constructions that are generally useful % {\timeless{\ownGhost\gname{\melt : M_i}}} % \end{mathpar} +\subsection{Invariant identifier namespaces} +\ralf{Describe this.} + % \subsection{STSs with interpretation}\label{sec:stsinterp} % Building on \Sref{sec:stsmon}, after constructing the monoid $\STSMon{\STSS}$ for a particular STS, we can use an invariant to tie an interpretation, $\pred : \STSS \to \Prop$, to the STS's current state, recovering CaReSL-style reasoning~\cite{caresl}. diff --git a/docs/logic.tex b/docs/logic.tex index 0365a7e7feccbae85ecfd15d13b42087f1c7e5f2..bad325d06acc2d1684e498c1558b82b09e724ed2 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -460,7 +460,7 @@ This is entirely standard. {\timeless{\ownGGhost\melt}} \infer{} -{}\timeless{\ownPhys\state} +{\timeless{\ownPhys\state}} \infer {\vctx \proves \timeless{\propB}}