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 Lean
ascription syntax ⊢@{IProp GF} P plays the same role as the Rocq
local notation ⊢@{iPropI Σ} P used in the original tutorial.
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
(matching Rocq's "%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 classes in the Rocq
version, and the corresponding instances in iris-lean) 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