2.2. Iris in Lean🔗

The type of propositions in Iris is IProp GF. All proofs in Iris are performed in a context with a GF : BundledGFunctors, used to specify available resources. The details of GF will come later when we introduce resource algebras. For now, just remember to work inside a variable {GF} block. This corresponds directly to the Rocq tutorial's Section proofs. Context {Σ : gFunctors}. — Lean's BundledGFunctors plays the role of Rocq's gFunctors.

open Iris Iris.BI

namespace Basics
variable {GF : BundledGFunctors}

Iris provides two kinds of propositional statements:

⊢ P asks whether P holds with no assumptions;
P ⊢ Q asks whether Q holds assuming P.

In Lean, we work in the Iris Proof Mode (IPM/MoSeL). The practical implication is that we get a new context, called the spatial context, in addition to the usual Lean context, now called the non-spatial context. Hypotheses from both contexts can be used to prove the goal.

The regular Lean tactics can still be used when we work within the non-spatial context, but, in general, we shall use new tactics that work natively with the spatial context. These new tactics start with the letter i: instead of intro H we use iintro H, and instead of apply H we use iapply H. Note that identifiers for hypotheses in the spatial context are ordinary Lean identifiers — unlike the Rocq version of Iris, the Lean port uses identifiers rather than strings.

To see this in action we will prove the statement P ⊢ P, for all P.

theorem asm (P : IProp GF) : P ⊢ P := byGF:BundledGFunctorsP:IProp GF⊢ P ⊢ P
  iintro HGF:BundledGFunctorsP:IProp GF⊢ 
∗H : P
⊢ P
  iexact HAll goals completed! 🐙

The tactic iintro adds P to the spatial context with the identifier H. To finish the proof, one would normally use either exact or apply. So in Iris, we use either iexact or iapply.

2.2.1. Technical Details🔗

In Lean, the context and the goal form a sequent (writing ⊢ₓ for the Lean entailment to distinguish it from the Iris entailment ⊢):

H₁ : Φ₁, ..., Hₙ : Φₙ  ⊢ₓ  Ψ

This is equivalent to the proposition Φ₁ ∧ ... ∧ Φₙ ⊢ₓ Ψ.

The Iris Proof Mode mimics this in the sense that the spatial context and the goal form an Iris sequent:

H₁ : Φ₁, ..., Hₙ : Φₙ  ⊢  Ψ

However, as Iris is a separation logic, this is equivalent to the entailment Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ.

Technically, since Iris is built on top of Lean, proving an Iris entailment in Lean corresponds to proving ⊢ₓ (P ⊢ Q). In other words, the spatial context is part of the Lean goal. This is the reason why the regular Lean tactics no longer suffice. The new tactics work with both the non-spatial and the spatial contexts.

Iris propositions include many of the usual logical connectives such as conjunction P ∧ Q. The Lean port overloads these notations directly on the IProp GF type, so — unlike the Rocq version — no %I scope annotation is needed.