Timeless Propositions

Definition and Uses

A large class of propositions do not depend on time; they are either always true or always false. An example is equalities; 2 + 2 = 4 is always true. We call such propositions timeless. All pure propositions are timeless, and ownership of a resource is timeless if the resource comes from a resource algebra (this includes points-to predicates). Further, timelessness is preserved by most connectives. As a rule of thumb, a predicate is timeless if

• it does not contain a ▷
• it does not mention an invariant
• it is first-order

Naively, one might assume that if P is timeless, then ▷ P ⊢ P. However, together with Löb induction, this would actually imply that P is True. Instead, the power of timeless propositions is reflected in the rule: ▷ P ⊢ |={⊤}=> P, whenever P is timeless. This rule allows us to strip laters from timeless propositions whenever the goal contains a fancy update modality. To identify timeless propositions, Iris uses the typeclass Timeless.

As ▷ is a modality, we can use the iMod tactic to strip it from our hypothesis. In this case, this is allowed as the goal contains a fancy update modality and P is timeless.

As usual, we can use the notation ">" to invoke iMod. This is how we will usually invoke iMod to strip laters. The above proof can hence be shortened as follows.

We may always add a fancy update modality in front of a WP (concretely with the fupd_wp lemma), so we can also remove laters from timeless propositions in our context if the goal is a weakest precondition.

Since the points-to predicate is well supported, we do not actually have to remove the later manually; the tactics work even when the predicate has a later.

The last scenario we mention is when the goal contains a later. In this case, we may remove laters from timeless hypotheses without removing the later from the goal.

Timeless Propositions and Invariants

Timeless propositions are especially useful in connection with invariants. Recall from the invariants chapter that when we open an invariant, inv N P, we only get the resources later, ▷P. Often, however, we require the resources now. Consider the following example.

To prove that the CAS succeeds, we need to know that w equals 5. Thus, we must open the invariant.

Opening the invariant only gives us that w equals 5 later. However, as pure propositions are timeless, we can strip the later.

Now we can prove that the CAS succeeds.

When opening invariants, we usually strip laters from timeless parts of the invariant immediately.

Open the invariant, strip the later from the equality (achieved by ">"), and rewrite with the equality (achieved by "->").