The Iris Tutorial in Lean

6.2. Proving Persistency🔗

To prove a proposition □ P, we must prove P without assuming any exclusive resources. In other words, we have to throw away the spatial context when proving P.

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

The imodintro tactic introduces a modality in the goal. In this case, since the modality is a □, it throws away the spatial context.

Since the only difference between □ P and P is that the former does not claim the resources are exclusive, it follows that the persistently modality is idempotent.

theorem pers_idemp (P : IProp GF) : □ □ P ⊣⊢ □ P := GF:BundledGFunctorsP:IProp GF⊢ □ □ P ⊣⊢ □ P GF:BundledGFunctorsP:IProp GF⊢ ⊢ □ □ P -∗ □ PGF:BundledGFunctorsP:IProp GF⊢ ⊢ □ P -∗ □ □ P GF:BundledGFunctorsP:IProp GF⊢ ⊢ □ □ P -∗ □ P GF:BundledGFunctorsP:IProp GF⊢ □HP : P ⊢ □ P -- Iris already knows that `□` is idempotent, so it -- automatically removes all persistently modalities from a -- proposition when adding it to the intuitionistic context. -- One may think of all propositions in the intuitionistic -- context as having an implicit `□` in front. All goals completed! 🐙 GF:BundledGFunctorsP:IProp GF⊢ ⊢ □ P -∗ □ □ P GF:BundledGFunctorsP:IProp GF⊢ □HP : P ⊢ □ □ P GF:BundledGFunctorsP:IProp GF⊢ □HP : P ⊢ □ P All goals completed! 🐙

Only propositions that are instances of the Persistent typeclass can be added to the intuitionistic context. As with the typeclasses for pure propositions, Persistent can automatically identify most persistent propositions.

theorem pers_sep (P Q : IProp GF) : □ P ∗ □ Q ⊣⊢ □ (P ∗ Q) := GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □ P ∗ □ Q ⊣⊢ □ (P ∗ Q) GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ P ∗ □ Q -∗ □ (P ∗ Q)GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ (P ∗ Q) -∗ □ P ∗ □ Q GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ P ∗ □ Q -∗ □ (P ∗ Q) GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □HP : P □HQ : Q ⊢ □ (P ∗ Q) GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □HP : P □HQ : Q ⊢ P ∗ Q All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ (P ∗ Q) -∗ □ P ∗ □ Q GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □HP : P □HQ : Q ⊢ □ P ∗ □ Q All goals completed! 🐙

Note the intuitionistic-pattern variant #⟨HP, HQ⟩ that destructs a persistent separation directly in the cases pattern.

Persistency is preserved by quantifications.

theorem pers_all {α : Type} (P : α → IProp GF) [∀ x, Persistent (P x)] : (∀ x, □ P x) ⊢ ∀ y, P y ∗ P y := GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)⊢ (∀ x, □ P x) ⊢ ∀ y, P y ∗ P y GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y ∗ P y GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P yGF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y All goals completed! 🐙 GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y All goals completed! 🐙

For simple predicates such as the one below, Lean's typeclass resolution can automatically infer the Persistent instance.

def myPredicate (x : Val) : IProp GF := iprop(⌜x = hl_val(#5)⌝) instance myPredicate_persistent (x : Val) : Persistent (myPredicate (GF := GF) x) := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Val⊢ Persistent (myPredicate x) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Val⊢ Persistent iprop(⌜x = hl_val(#5)⌝) All goals completed! 🐙

For more complicated predicates, such as ones defined as a fixpoint, the Persistent instance cannot be inferred automatically. The following predicate asserts that all values in a given list are equal to hl_val(#5).

def myPredFix : List Val → IProp GF | [] => iprop(True) | x :: xs' => iprop(⌜x = hl_val(#5)⌝ ∗ myPredFix xs')

Adding such a predicate to the intuitionistic context requires us to register a Persistent instance manually, by induction on the list.

instance myPredFix_persistent (xs : List Val) : Persistent (myPredFix (GF := GF) xs) := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFxs:List Val⊢ Persistent (myPredFix xs) induction xs with hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GF⊢ Persistent (myPredFix []) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GF⊢ Persistent iprop(True); All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Valxs':List Valih:Persistent (myPredFix xs')⊢ Persistent (myPredFix (x :: xs')) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Valxs':List Valih:Persistent (myPredFix xs')⊢ Persistent iprop(⌜x = hl_val(#5)⌝ ∗ myPredFix xs'); All goals completed! 🐙

With the instance in place, iris-lean now recognises myPredFix as persistent.

theorem first_is_5 (x : Val) (xs : List Val) : myPredFix (GF := GF) (x :: xs) -∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) := GF:BundledGFunctorsx:Valxs:List Val⊢ ⊢ myPredFix (x :: xs) -∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) -- After `iintro #H`, the hypothesis `H : myPredFix (x :: xs)` -- sits in the intuitionistic context. Since `myPredFix` unfolds -- by pattern-matching, we can `change` the hypothesis-to-be so -- the destructure exposes the head element. GF:BundledGFunctorsx:Valxs:List Val⊢ ⊢ myPredFix (x :: xs) -∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) GF:BundledGFunctorsx:Valxs:List Val⊢ ⊢ ⌜x = hl_val(#5)⌝ ∗ myPredFix xs -∗ ⌜x = hl_val(#5)⌝ ∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix xs GF:BundledGFunctorsx:Valxs:List Val⊢ □Hx : ⌜x = hl_val(#5)⌝ □Hxs : myPredFix xs ⊢ ⌜x = hl_val(#5)⌝ ∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix xs All goals completed! 🐙