From 3cf0a5fc1ed93dfd4d454a807a9cc1996d53e31e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 17:05:53 +0100
Subject: [PATCH] give some derived proof rules
---
docs/derived.tex | 48 +++++++++++++++++++++++++++++++++++++++---------
docs/logic.tex | 2 +-
2 files changed, 40 insertions(+), 10 deletions(-)
diff --git a/docs/derived.tex b/docs/derived.tex
index cab6b22f6..6e101413c 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 0365a7e7f..bad325d06 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}}
--
GitLab