Commit 3cf0a5fc authored by Ralf Jung's avatar Ralf Jung

give some derived proof rules

parent 494f0357
Pipeline #288 passed with stage
\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}.
......
......@@ -460,7 +460,7 @@ This is entirely standard.
{\timeless{\ownGGhost\melt}}
\infer{}
{}\timeless{\ownPhys\state}
{\timeless{\ownPhys\state}}
\infer
{\vctx \proves \timeless{\propB}}
......
Markdown is supported
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