From b6fb28b7380320e08ba21c26686f172e8397fd66 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Dec 2017 15:07:45 +0100
Subject: [PATCH] Docs: Do not abbreviate.
---
docs/base-logic.tex | 2 +-
docs/ghost-state.tex | 2 +-
docs/paradoxes.tex | 4 ++--
docs/program-logic.tex | 2 +-
4 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 92e25252c..5e7d54183 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -448,7 +448,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlo
{\upd\plainly\prop \proves \prop}
\end{mathpar}
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
-%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
+%\ralf{Trouble is, we do not actually have $\in$ inside the logic...}
\subsection{Consistency}
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 843b8751a..402a67310 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -44,7 +44,7 @@ Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from
\subsection{Persistent Propositions}
We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
-These are propositions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic propositions.
+These are propositions that ``do not own anything'', so we can (and will) treat them like ``normal'' intuitionistic propositions.
Of course, $\always\prop$ is persistent for any $\prop$.
Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $\TRUE$, $\FALSE$, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$ and $\mval(\melt)$ are persistent.
diff --git a/docs/paradoxes.tex b/docs/paradoxes.tex
index a3bb499a4..8addc115d 100644
--- a/docs/paradoxes.tex
+++ b/docs/paradoxes.tex
@@ -32,7 +32,7 @@ Notice that these are immutable locations, so the maps-to proposition is persist
The rule \ruleref{sprop-alloc} is then thought of as allocation, and the rule \ruleref{sprop-agree} states that a given location $\gname$ can only store \emph{one} proposition, so multiple witnesses covering the same location must agree.
%Compared to saved propositions in prior work, \ruleref{sprop-alloc} is stronger since the stored proposition can depend on the name being allocated.
-%\derek{Can't we cut the above sentence? This makes it sound like we are doing something weird that we ought not to be since prior work didn't do it. But in fact, I thought that in our construction we don't really need to rely on this feature at all! So I'm confused.}
+%\derek{Can't we cut the above sentence? This makes it sound like we are doing something weird that we ought not to be since prior work didn't do it. But in fact, I thought that in our construction we do not really need to rely on this feature at all! So I'm confused.}
The conclusion of \ruleref{sprop-agree} usually is guarded by a $\later$.
The point of this theorem is to show that said later is \emph{essential}, as removing it introduces inconsistency.
%
@@ -43,7 +43,7 @@ $A(\gname) \eqdef \Exists \prop : \Prop. \always\lnot \prop \land \gname \Mapsto
Intuitively, $A(\gname)$ says that the saved proposition named $\gname$ does \emph{not} hold, \ie we can disprove it.
Using \ruleref{sprop-persist}, it is immediate that $A(\gname)$ is persistent.
-Now, by applying \ruleref{sprop-alloc} with $A$, we obtain a proof of $\prop \eqdef \gname \Mapsto A(\gname)$: this says that the proposition named $\gname$ is the proposition saying that it, itself, doesn't hold.
+Now, by applying \ruleref{sprop-alloc} with $A$, we obtain a proof of $\prop \eqdef \gname \Mapsto A(\gname)$: this says that the proposition named $\gname$ is the proposition saying that it, itself, does not hold.
In other words, $\prop$ says that the proposition named $\gname$ expresses its own negation.
Unsurprisingly, that leads to a contradiction, as is shown in the following lemma:
\begin{lem} \label{lem:saved-prop-counterexample-not-agname} We have $\gname \Mapsto A(\gname) \proves \always\lnot A(\gname)$ and $\gname \Mapsto A(\gname) \proves A(\gname)$. \end{lem}
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index f4a4ba7ce..df72785ca 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -521,7 +521,7 @@ Furthermore, as we construct more sophisticated and more interesting things that
For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition:
\[ \Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop) \]
-This accessor is ``idempotent'' in the sense that it doesn't actually change the state. After applying it, we get our $\prop$ back so we end up where we started.
+This accessor is ``idempotent'' in the sense that it does not actually change the state. After applying it, we get our $\prop$ back so we end up where we started.
%%% Local Variables:
%%% mode: latex
--
GitLab