Refactor proofs of {impl,wand}_timeless
Follow-up to https://mattermost.mpi-sws.org/iris/pl/8fb1whfcstg49mbe7ip4uwwywy
This MR clarifies why Löb induction is used in these proofs: To use a different formulation of timelessness. This notion of timelessness is necessary when using the later_false_em
law.
Timelessness
In iris, a proposition P
is timeless iff \triangleright P \vdash \triangleright \bot \vee P
. Intuitively, when reading P
as a step-index proposition, this means that \forall n.\ P(n) \to P(n+1)
(with the inverse already holding, since P
is down-closed).
An alternative definition, which is more intuitive, is that \forall n.\ P(0) \to P(n)
, i.e. P
is independent of the step-index, and entirely defined by its behavior at index 0
.
Formally, this reads as a proposition P
being timeless iff \forall H, (\triangleright \bot \land H \vdash P) \implies (H \vdash P)
. In other words, to prove P
, we can assume we are at step-index 0
.
Using Löb induction, we can show this law from the original definition. This law could serve as an alternative definition of Timeless
, since it implies the current definition, without Löb
induction.
\triangleright
-timeless Law.
The This law (defined on page 36/figure 11 in "Iris from the ground up") expresses that \triangleright P \vdash \triangleright \bot \lor (\triangleright \bot \Rightarrow P)
. Its meaning is somewhat non-obvious: It allows us to do a case distinction on whether we are at step-index 0:
- If we are, the left side will be true, which just expresses precisely that we are at step-index
0
. - If we are not, the right side will be true. Also, we know that our step-index is
S\ n
for somen
. Thus, we know thatP(n)
is true. SinceP
is down-closed, this also means thatP(0)
is true. We can thus provide an "accessor law" that allows us to accessP(0)
if the step-index ever becomes0
in the future. This is what the right-hand side expresses: Ifn
becomes0
, you knowP
is true.
Using this to make the proofs more elegant
Using this alternative definition, showing that wands and implication preserve timelessness becomes a lot nicer. What needs to be shown is that a proof of P \Rightarrow Q
at index 0
can be turned into one at an arbitrary index. For this, we can simply intros P
, and use the fact that Q
is timeless to assume we are at index 0
. This then allows us to use the original proof of P \Rightarrow Q
at level 0
.
Credit to Robbert, who came up with some of the simplifications.