Add comments explaining intricate later shenanigans

iris/bi/derived_connectives.v

@@ -93,6 +93,21 @@ Notation "◇ P" := (bi_except_0 P) : bi_scope.
 Global Instance: Params (@bi_except_0) 1 := {}.
 Global Typeclasses Opaque bi_except_0.
 
+(* Timeless propositions are propositions that do not depend on the step-index.
+   There are two equivalent ways of expressing that a step-indexed proposition
+   [P : nat → Prop] is timeless:
+   * Option one, used here, says that [∀ n, P n → P (S n)]. In the logic, this
+     is stated as [▷ P ⊢ ◇ P] (which actually reads [∀ n > 0, P (n-1) → P n],
+     but this is trivially equivalent).
+   * Option two says that [∀ n, P 0 → P n]. In the logic, this is stated as a
+     meta-entailment [∀ P, (▷ False ∧ P ⊢ Q) → (P ⊢ Q)]. The assumption
+     [▷ False] expresses that the step-index is 0.
+
+   Both formulations are equivalent. In the logic, this can be shown using Löb
+   induction and [later_false_em]. In the model, this follows from regular
+   natural induction.
+   The law [timeless_alt] in [derived_laws_later.v] provides option two, by
+   proving that both versions are equivalent in the logic.  *)
 Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
 Global Arguments Timeless {_} _%I : simpl never.
 Global Arguments timeless {_} _%I {_}.

iris/bi/derived_laws_later.v

@@ -337,11 +337,13 @@ Proof. rewrite /bi_except_0; apply _. Qed.
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
 
-(* To prove a timeless proposition Q, we can additionally assume
-   that we are at step-index 0 (hypothesis ▷ False).
-   In fact, this can also serve as a definition of timelessness. *)
+(* The left-to-right direction of this lemma shows that to prove a timeless
+   proposition [Q], we can additionally assume that we are at step-index 0, i.e.
+   we can add [▷ False] to our assumptions. The right-to-left direction shows
+   that this is in fact an exact characterization of timeless propositions.
+   See also the comment above the definition of [Timeless]. *)
 Lemma timeless_alt `{!BiLöb PROP} Q :
-  Timeless Q ↔ ∀ P, (▷ False ∧ P ⊢ Q) → (P ⊢ Q).
+  Timeless Q ↔ (∀ P, (▷ False ∧ P ⊢ Q) → (P ⊢ Q)).
 Proof.
   split; rewrite /Timeless => H.
   * intros P Hpr.

iris/bi/interface.v

@@ -222,6 +222,12 @@ Section bi_mixin.
     bi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
     bi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;
 
+    (* In a step-index model, this law allows case distinctions on whether
+       the step-index is 0 (expressed as [▷ False] in the logic):
+       * If it is 0, the left side is true, and we know nothing about [P].
+       * If not, then it is [S n] for some [n], and [P] holds at [n]. By down-
+         closure, it also holds at [0]. Thus, we get to use [P], but only if
+         the step-index is 0 ([▷ False] is true). *)
     bi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
   }.