The Iris Tutorial in Lean

3. Pure Propositions🔗

The implementation of Iris in Lean has a unique class of propositions called pure. This class arises from the fact that Lean propositions can be embedded into the logic of Iris. Any Lean proposition φ : Prop can be turned into an Iris proposition through the pure embedding ⌜φ⌝ : IProp GF. This allows us to piggyback on much of the functionality and theory developed for the logic of Lean. The proposition ⌜φ⌝ is thus an Iris proposition, and we can use it as we would any other Iris proposition.

open Iris Iris.BI namespace Pure variable {GF : BundledGFunctors} theorem asm_pure (φ : Prop) : ⌜φ⌝ ⊢@{IProp GF} ⌜φ⌝ := GF:BundledGFunctorsφ:Prop⊢ ⌜φ⌝ ⊢ ⌜φ⌝ GF:BundledGFunctorsφ:Prop⊢ ∗H : ⌜φ⌝ ⊢ ⌜φ⌝ All goals completed! 🐙

When stating lemmas that do not depend on generic Iris propositions mentioning GF, we have to specify the carrier type. The ascription syntax ⊢@{IProp GF} P records that the entailment lives in the proposition type IProp GF.

A pure proposition is then any Iris proposition P for which there exists a Lean proposition φ, such that P ⊣⊢ ⌜φ⌝.

Pure propositions can be introduced using ipureintro. This exits the Iris Proof Mode (discarding the spatial context) and turns the goal into a Lean proposition.

theorem eq_5_5 : ⊢@{IProp GF} ⌜5 = 5⌝ := GF:BundledGFunctors⊢ ⊢ ⌜5 = 5⌝ GF:BundledGFunctors⊢ 5 = 5 All goals completed! 🐙

To eliminate a pure proposition, we can use the cases pattern %name. This moves the proposition into the non-spatial Lean context as a Lean proposition.

theorem eq_elm {α : Type} (P : α → IProp GF) (x y : α) : ⌜x = y⌝ -∗ P x -∗ P y := GF:BundledGFunctorsα:TypeP:α → IProp GFx:αy:α⊢ ⊢ ⌜x = y⌝ -∗ P x -∗ P y GF:BundledGFunctorsα:TypeP:α → IProp GFx:αy:αHeq:x = y⊢ ∗HP : P x ⊢ P y GF:BundledGFunctorsα:TypeP:α → IProp GFx:αy:αHeq:x = y⊢ ∗HP : P x ⊢ P x All goals completed! 🐙

It is quite easy to show that the propositions ⌜5 = 5⌝ and ⌜x = y⌝ from above are pure. However, it can become quite burdensome for more complicated Iris propositions. Fortunately, Iris has machinery (the IntoPure / FromPure type classes and their instances) that identifies pure propositions automatically — ipureintro makes use of them.

True is pure.

theorem true_intro : ⊢@{IProp GF} True := GF:BundledGFunctors⊢ ⊢ True GF:BundledGFunctors⊢ True All goals completed! 🐙

Conjunction preserves pureness.

theorem and_pure : ⊢@{IProp GF} ⌜5 = 5⌝ ∧ ⌜8 = 8⌝ := GF:BundledGFunctors⊢ ⊢ ⌜5 = 5⌝ ∧ ⌜8 = 8⌝ GF:BundledGFunctors⊢ 5 = 5 ∧ 8 = 8 All goals completed! 🐙

Separating conjunction preserves pureness.

theorem sep_pure : ⊢@{IProp GF} ⌜5 = 5⌝ ∗ ⌜8 = 8⌝ := GF:BundledGFunctors⊢ ⊢ ⌜5 = 5⌝ ∗ ⌜8 = 8⌝ GF:BundledGFunctors⊢ 5 = 5 ∧ 8 = 8 All goals completed! 🐙

Wand preserves pureness.

theorem wand_pure {α : Type} (x y : α) : ⊢@{IProp GF} ⌜x = y⌝ -∗ ⌜y = x⌝ := GF:BundledGFunctorsα:Typex:αy:α⊢ ⊢ ⌜x = y⌝ -∗ ⌜y = x⌝ GF:BundledGFunctorsα:Typex:αy:α⊢ x = y → y = x GF:BundledGFunctorsα:Typex:αy:αHeq:x = y⊢ y = x All goals completed! 🐙

Arbitrary Iris propositions are not pure.

theorem abstr_not_pure (P : IProp GF) : ⊢ P -∗ ⌜8 = 8⌝ := GF:BundledGFunctorsP:IProp GF⊢ ⊢ P -∗ ⌜8 = 8⌝ GF:BundledGFunctorsP:IProp GF⊢ ∗_HP : P ⊢ ⌜8 = 8⌝ GF:BundledGFunctorsP:IProp GF⊢ 8 = 8 All goals completed! 🐙

The pure embedding allows us to state an important property, namely soundness: anything proved inside the Iris logic is as true as anything proved in Lean. In iris-lean this is witnessed by the soundness theorems for UPred.

⌜_⌝ turns Lean propositions into Iris propositions, while ⊢ _ turns Iris propositions into Lean propositions. These operations are not inverses, but they are related.

theorem pure_adj1 (φ : Prop) : φ → ⊢@{IProp GF} ⌜φ⌝ := GF:BundledGFunctorsφ:Prop⊢ φ → ⊢ ⌜φ⌝ GF:BundledGFunctorsφ:PropH:φ⊢ ⊢ ⌜φ⌝ GF:BundledGFunctorsφ:PropH:φ⊢ φ All goals completed! 🐙 theorem pure_adj2 (P : IProp GF) : ⌜⊢ P⌝ -∗ P := GF:BundledGFunctorsP:IProp GF⊢ ⊢ ⌜⊢ P⌝ -∗ P GF:BundledGFunctorsP:IProp GFH:⊢ P⊢ ⊢ P All goals completed! 🐙 end Pure