From 9fffb0b980afa90f577b92147e45adbd60f9539b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 5 Jun 2019 19:04:30 +0200
Subject: [PATCH] =?UTF-8?q?docs:=20derive=20L=C3=B6b=20induction?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md         |  4 ++--
 docs/base-logic.tex  |  4 ++--
 docs/ghost-state.tex | 12 ++++++++----
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9e762c041..224ed688a 100644
--- a/CHANGELOG.md
+++ b/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.
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 450b6a6ad..344ed6d0a 100644
--- a/docs/base-logic.tex
+++ b/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} \\
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index c774af107..7dbf916a9 100644
--- a/docs/ghost-state.tex
+++ b/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$.
-- 
GitLab