docs: derive Löb induction

CHANGELOG.md

@@ -24,10 +24,10 @@ Changes in and extensions of the theory:
   trace has a matching list of events.  Change WP so that it is told the entire
   future trace of observations from the beginning.  Use this in heap_lang to
   implement prophecy variables.
-* [#] The Löb rule is now a derived rule; it follows from later-intro, later
+* The Löb rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   functions.
-* [#] Add atomic updates and logically atomic triples, including tactic support.
+* Add atomic updates and logically atomic triples, including tactic support.
   See `heap_lang/lib/increment.v` for an example.
 * [#] heap_lang now uses right-to-left evaluation order. This makes it
   significantly easier to write specifications of curried functions.

docs/base-logic.tex

@@ -380,9 +380,9 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlo
   {\prop \proves \propB}
   {\later\prop \proves \later{\propB}}
 \and
-\inferhref{L{\"o}b}{Loeb}
+\infer[$\later$-I]
   {}
-  {(\later\prop\Ra\prop) \proves \prop}
+  {\prop \proves \later\prop}
 \and
 \begin{array}[c]{rMcMl}
   \All x. \later\prop &\proves& \later{\All x.\prop} \\

docs/ghost-state.tex

@@ -6,6 +6,10 @@ These are not ``extensions'' in the sense that they change the proof power of th
 \subsection{Derived Rules about Base Connectives}
 We collect here some important and frequently used derived proof rules.
 \begin{mathparpagebreakable}
+  \inferhref{L{\"o}b}{Loeb}
+  {}
+  {(\later\prop\Ra\prop) \proves \prop}
+
   \infer{}
   {\prop \Ra \propB \proves \prop \wand \propB}
 
@@ -33,14 +37,14 @@ We collect here some important and frequently used derived proof rules.
   \infer{}
   {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
 
-  \infer{}
-  {\prop \proves \later\prop}
-
   \infer{}
   {\TRUE \proves \plainly\TRUE}
 \end{mathparpagebreakable}
 
-Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from Löb induction, and $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
+Noteworthy here is the fact that Löb induction can be derived from $\later$-introduction and the fact that we can take fixed-points of functions where the recursive occurrences are below $\later$.%
+\footnote{See \url{https://en.wikipedia.org/wiki/L\%C3\%B6b\%27s_theorem}.}
+Furthermore, $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
+To derive that existential quantifiers commute with separating conjunction requires an intermediate step using a magic wand: From $P * \exists x, Q \vdash \Exists x. P * Q$ we can deduce $\Exists x. Q \vdash P \wand \Exists x. P * Q$ and then proceed via $\exists$-elimination.
 
 \subsection{Persistent Propositions}
 We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.