Iris-Lean

Separation logic proofs are performed in the Iris Proof Mode.

Entering Proof Mode: Use the istart tactic. Note that most separation logic tactics call istart automatically, so explicit invocation is often unnecessary.

Tactic State: When in Iris Proof Mode, the Lean tactic state displays two additional contexts beneath the standard Lean context:

1. Intuitionistic context (denoted by □)
2. Spatial context (denoted by ∗)

Tactics: Tactics in this mode follow Lean conventions but are prefixed with i (e.g., iintro, isplit, iexact, ispecialize, icases, iexists).

theorem proof_example [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
  P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
:= by
  iintro ⟨HP, HQ, □HR⟩ □HRΦ
  ispecialize HRΦ HR as HΦ
  icases HΦ with ⟨x, HΦ⟩
  iexists x
  isplit r
  · iassumption
  isplit l [HP]
  · iexact HP
  · iexact HQ

The tool operates in three main stages:

1. Lean Data Extraction: Running lake exe dumpPortingData scans the compiled Lean environment and writes a JSON file (default .lake/porting_data.json) containing all @[rocq_alias] mappings, #rocq_ignore entries, #rocq_ignore_file entries, and #rocq_concept entries.
2. Rocq Data Acquisition: The script downloads the Iris-Rocq source tarball at the revision specified in scripts/ROCQ_REVISION, parses .v files for definition names, and caches them in --cache-dir.
3. Comparison (Diff): Definitions are classified as:
   • ported: Has a matching @[rocq_alias] in Lean.
   • ignored: Listed via #rocq_ignore, #rocq_ignore_file, or in a package's ignoredDirs.
   • missing: No alias or ignore entry found.
   • stale_alias / stale_ignore: Lean-side aliases or ignores that point to Rocq targets that no longer exist upstream.

Iris-Lean requires a specific directory structure for module organization:

1. Entry Point Modules: Every directory Foo/ must have a corresponding module Foo.lean acting as its entry point (e.g., Iris/BI/BigOp/ must have Iris/BI/BigOp.lean).
2. Transitive Imports: The entry-point module must transitively import every module within its directory. For example, Iris/ProofMode.lean must be able to reach Iris/ProofMode/Tactics/Frame.lean through its hierarchy.
3. Exceptions: Directories named Iris/*/Lib (specifically Iris.Algebra.Lib, Iris.BI.Lib, Iris.HeapLang.Lib, and Iris.Instances.Lib) are exempt; their entry points are not imported by their parents.
4. Iris.Init: Every module must import Iris.Init (directly or transitively) to ensure a consistent environment (options, notation, etc.). New leaf modules that import nothing from the project must add import Iris.Init explicitly.

Using the separation logic framework involves four main steps:

1. Instantiate the separation logic interface: Provide instances for the BIBase and BI typeclasses. BIBase defines operators (entailment, conjunction, etc.), while BI provides proofs for axioms. You can instantiate BI directly to provide both.
2. Add custom notation (optional): Define new syntax for your logic using syntax and macro_rules. Note that logic syntax must be wrapped in iprop quotations to distinguish it from Lean propositions.
3. Instantiate existing typeclasses (optional): Provide instances for properties like Affine for custom constructs or logic-wide properties using typeclasses like BIAffine.
4. Write proofs: Use the istart tactic to enter the Iris Proof Mode, where you can use separation logic-specific tactics (e.g., iintro, isplit, iexact).

-- 1. Instantiate the interface
instance : BIBase (HeapProp Val) where
  entails P Q := ∀ σ, P σ → Q σ
  emp         := fun σ => σ = ∅
  and P Q     := fun σ => P σ ∧ Q σ
  sep P Q     := fun σ => ∃ σ1 σ2 , σ = σ1 ∪ σ2 ∧ σ1 || σ2 ∧ P σ1 ∧ Q σ2
  ...

instance : BI (HeapProp Val) where
  entails_preorder := { ... }
  and_elim_l       := by ...
  ...

-- 4. Write a proof
theorem proof_example [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
  P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
:= by
  iintro ⟨HP, HQ, □HR⟩ □HRΦ
  ispecialize HRΦ HR as HΦ
  icases HΦ with ⟨x, HΦ⟩
  iexists x
  isplit r
  · iassumption
  isplit l [HP]
  · iexact HP
  · iexact HQ