editing

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}