The Iris Tutorial in Lean

6.1. Introduction🔗

In separation logic, propositions are generally not duplicable. This is because resources are generally exclusive. However, resources do not have to be exclusive. A great example of this is read-only memory. There is no danger in letting many threads access the same location simultaneously if they can only read from it. Hence, it would not make sense to require that ownership of those locations be exclusive. Motivated by this, we introduce a new modality denoted the persistently modality, written □ P, for propositions P. The proposition □ P describes the same resources as P, except it does not claim that the resources are exclusive — hence □ P can be duplicated. Persistent propositions hence act like propositions in an intuitionistic logic, which is why iris-lean's proof mode also refers to the corresponding context as the intuitionistic context.

A proposition is persistent when P ⊢ □ P. That is, assuming P, we need to show that P does not rely on any exclusive resources. Persistency is preserved by most connectives, so proving that a proposition is persistent is usually a matter of showing that the mentioned resources are shareable. Which resources are shareable depends on the specific notions of resources being used. For the resource of heaps, a location can be marked as read-only, making it shareable. The associated points-to predicate hence becomes persistent. We will see an example of this later.

Propositions that do not rely on resources altogether are trivially persistent. We have already given those types of propositions a name: pure. This is also why we do not have to split the non-spatial context when using isplitl/isplitr; all pure propositions are persistent, hence duplicable.

Of course, not all persistent propositions are pure (e.g. persistent points-to predicates). Thus, the Iris Proof Mode provides a third context just for persistent propositions, called the intuitionistic context. Pure propositions can go in all three contexts. Persistent propositions can go in the spatial or intuitionistic context. And all other propositions are limited to the spatial context only. iris-lean uses the typeclass Iris.BI.Persistent to identify persistent propositions.

open Iris Iris.BI Iris.HeapLang namespace Persistently variable {hlc} {GF : BundledGFunctors} [HeapLangGS hlc GF]

The cases pattern #H (matching Rocq's "#H" intro pattern) moves a persistent hypothesis into the intuitionistic context.

theorem pers_context (P Q : IProp GF) [Persistent P] : P -∗ Q -∗ P ∗ Q := GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ⊢ P -∗ Q -∗ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗HQ : Q ⊢ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ PGF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗HQ : Q ⊢ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗HQ : Q ⊢ Q All goals completed! 🐙

The intuitionistic context is shared across both subgoals of an isplitl/isplitr: HP remains available after the split.

By contrast, putting HP into the spatial context discards persistency:

theorem not_in_pers_context (P Q : IProp GF) [Persistent P] : P -∗ Q -∗ P ∗ Q := GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ⊢ P -∗ Q -∗ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HP : P ∗HQ : Q ⊢ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HP : P ⊢ PGF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HQ : Q ⊢ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HP : P ⊢ P All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HQ : Q ⊢ Q All goals completed! 🐙

Persistent propositions are duplicable.

theorem pers_dup (P : IProp GF) [Persistent P] : P ⊢ P ∗ P := GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ P ⊢ P ∗ P GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P ∗ P GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ PGF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙

Persistent propositions satisfy several nice properties simply by being duplicable (P ⊢ P ∗ P). For example, P ∧ Q and P ∗ Q coincide when either P or Q is persistent; likewise, P → Q and P -∗ Q coincide when P is persistent. The relevant iris- lean lemmas are Iris.BI.persistent_and_sep and Iris.BI.impl_wand.

The Iris Proof Mode knows these facts and allows isplit to introduce ∗ when one of its arguments is persistent.