From ccf8bc36c329417e093fa6c775c71f30f60363d1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 29 Apr 2019 13:29:15 +0200
Subject: [PATCH] editing
---
docs/ghost-state.tex | 48 +++++++++++++++++++++-----------------------
1 file changed, 23 insertions(+), 25 deletions(-)
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 953a2fea7..b8d55d0fd 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -57,31 +57,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
-
-This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
-\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
-In other words, when working below the except-0 modality, we can \emph{strip
- away} the later from timeless propositions. In fact, we can strip away later
-from timeless propositions even when working under the later modality:
-\begin{mathpar}
- \inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
- {\later\prop \proves \later\propB}
-\end{mathpar}
-This rule looks different from the above ones, because we still do not have that
-\begin{mathpar}
- \inferH{later-fake-rule}{\timeless{\prop}}
- {\later\prop \proves \prop}
-\end{mathpar}
-The proof of the former is $\later \prop \proves \diamond \prop =
-\later\FALSE \lor \prop$, and then by straightforward disjunction elimination:
-% Cut the second part if trivial.
-\begin{mathpar}
- \infer{\later\FALSE \proves \later \propB \and \prop \proves \later \propB}
- {\later\FALSE \lor \prop \proves \propB}
-\end{mathpar}
-
-
-The following rules can be derived about except-0:
+Except-0 satisfies the usual laws of a ``monadic'' modality (similar to, \eg the update modalities):
\begin{mathpar}
\inferH{ex0-mono}
{\prop \proves \propB}
@@ -106,6 +82,28 @@ The following rules can be derived about except-0:
\diamond\later\prop &\proves& \later{\prop}
\end{array}
\end{mathpar}
+In particular, from \ruleref{ex0-mono} and \ruleref{ex0-idem} we can derive a ``bind''-like elimination rule:
+\begin{mathpar}
+ \inferH{ex0-elim}
+ {\prop \proves \diamond\propB}
+ {\diamond\prop \proves \diamond\propB}
+\end{mathpar}
+
+This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
+\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
+In other words, when working below the except-0 modality, we can \emph{strip
+ away} the later from timeless propositions (using \ruleref{ex0-elim}):
+\begin{mathpar}
+ \inferH{ex0-timeless-strip}{\timeless{\prop} \and \prop \proves \diamond\propB}
+ {\later\prop \proves \diamond\propB}
+\end{mathpar}
+
+ In fact, it turns out that we can strip away later from timeless propositions even when working under the later modality:
+\begin{mathpar}
+ \inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
+ {\later\prop \proves \later\propB}
+\end{mathpar}
+This follows from $\later \prop \proves \later\FALSE \lor \prop$, and then by straightforward disjunction elimination.
The following rules identify the class of timeless propositions:
\begin{mathparpagebreakable}
--
GitLab