From 610698ecc66d7306593964e7db2e27808ce9ae89 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 12 Mar 2016 09:05:46 +0100
Subject: [PATCH] docs: various nits
---
docs/constructions.tex | 4 ++--
docs/derived.tex | 9 +++++++--
docs/iris.sty | 2 +-
docs/logic.tex | 7 +++----
4 files changed, 13 insertions(+), 9 deletions(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 8853f3043..834f29af7 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -28,9 +28,9 @@ One way to understand this definition is to re-write it a little.
We start by defining the COFE of \emph{step-indexed propositions}:
\begin{align*}
\SProp \eqdef{}& \psetdown{\mathbb{N}} \\
+ \eqdef{}& \setComp{\prop \in \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \prop \Ra m \in \prop } \\
\prop \nequiv{n} \propB \eqdef{}& \All m \leq n. m \in \prop \Lra m \in \propB
\end{align*}
-where $\psetdown{N}$ denotes the set of \emph{down-closed} sets of natural numbers: If $n$ is in the set, then all smaller numbers also have to be in there.
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
\begin{align*}
\UPred(\monoid) \approx{}& \monoid \monra \SProp \\
@@ -80,7 +80,7 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\newcommand{\agc}{\mathrm{c}} % the "c" field of an agreement element
\newcommand{\agV}{\mathrm{V}} % the "V" field of an agreement element
\begin{align*}
- \agm(\cofe) \eqdef{}& \recordComp{\agc : \mathbb{N} \to \cofe , \agV : \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \agV \Ra m \in \agV } \\
+ \agm(\cofe) \eqdef{}& \record{\agc : \mathbb{N} \to \cofe , \agV : \SProp} \\
& \text{quotiented by} \\
\melt \equiv \meltB \eqdef{}& \melt.\agV = \meltB.\agV \land \All n. n \in \melt.\agV \Ra \melt.\agc(n) \nequiv{n} \meltB.\agc(n) \\
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\agV \Lra m \in \meltB.\agV) \land (\All m \leq n. m \in \melt.\agV \Ra \melt.\agc(m) \nequiv{m} \meltB.\agc(m)) \\
diff --git a/docs/derived.tex b/docs/derived.tex
index b303c99f2..aeb47ab44 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -1,5 +1,10 @@
\section{Derived proof rules and other constructions}
+We will below abuse notation, using the \emph{term} meta-variables like $\val$ to range over (bound) \emph{variables} of the corresponding type..
+We omit type annotations in binders and equality, when the type is clear from context.
+We assume that the signature $\Sig$ embeds all the meta-level concepts we use, and their properties, into the logic.
+(The Coq formalization is a \emph{shallow embedding} of the logic, so we have direct access to all meta-level notions within the logic anyways.)
+
\subsection{Base logic}
We collect here some important and frequently used derived proof rules.
@@ -245,10 +250,10 @@ Whenever needed (in particular, for masks at view shifts and Hoare triples), we
We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$.
We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
-We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl\namesp_2 \subseteq \namecl\namesp_1$.
+We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.
Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
-We have that $\namesp_1 \sep \namesp_2 \Ra \namecl\namesp_2 \sep \namecl\namesp_1$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
+We have that $\namesp_1 \sep \namesp_2 \Ra \namecl{\namesp_2} \sep \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
We will overload the usual Iris notation for invariant assertions in the following:
\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
diff --git a/docs/iris.sty b/docs/iris.sty
index 065d62e2b..7f79af763 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -185,7 +185,7 @@
\newcommand{\mask}{\mathcal{E}}
\newcommand{\namesp}{\mathcal{N}}
-\newcommand{\namecl}[1]{{\uparrow#1}}
+\newcommand{\namecl}[1]{{#1^{\kern0.2ex\uparrow}}}
%% various pieces of Syntax
\def\MU #1.{\mu #1.\spac}%
diff --git a/docs/logic.tex b/docs/logic.tex
index 3642b42f1..9d89d639a 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -590,9 +590,8 @@ This is entirely standard.
{\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
\end{mathpar}
-\subsection{Lifting of operational semantics}\label{sec:lifting}
-
-\begin{mathparpagebreakable}
+\paragraph{Lifting of operational semantics.}~
+\begin{mathpar}
\infer[wp-lift-step]
{\mask_2 \subseteq \mask_1 \and
\toval(\expr_1) = \bot \and
@@ -605,7 +604,7 @@ This is entirely standard.
\All \state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr')}
{\later\All \expr_2, \expr'. \pred(\expr_2, \expr') \wand \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
-\end{mathparpagebreakable}
+\end{mathpar}
Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr' = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
--
GitLab