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.

The \triangleright-timeless Law.

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 some n. Thus, we know that P(n) is true. Since P is down-closed, this also means that P(0) is true. We can thus provide an "accessor law" that allows us to access P(0) if the step-index ever becomes 0 in the future. This is what the right-hand side expresses: If n becomes 0, you know P 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.