The Iris Tutorial in Lean

5.4. Composing Programs and Proofs🔗

To compose specifications, we use wp_bind to focus on a sub-expression and wp_wand (a generic WP lemma in Iris.ProgramLogic.WeakestPre) to weaken the postcondition.

The Rocq tutorial's idiomatic style is to give a postcondition- generic specification — one parametric in Φ — that can be applied with iapply. Here is the same idiom applied to our writeread program from the previous section.

theorem writeread_spec_2 (Φ : Val → IProp GF) : (∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v) -∗ WP writeread {{ v, Φ v }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GF⊢ ⊢ (∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v) -∗ WP writeread {{ v, Φ v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GF⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v ⊢ WP writeread {{ v, Φ v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GF⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v ⊢ WP hl(let x := ref(#7); !x) {{ v, Φ v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GF⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v ⊢ WP hl(ref(#7)) {{ v, WP hl(let x := v(&v); !x) {{ v, Φ v }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GF⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v ⊢ ▷ ∀ l, l ↦ some hl_val(#7) -∗ WP hl(let x := #l; !x) {{ v, Φ v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ x, ⌜x = hl_val(#7)⌝ -∗ Φ x ∗Hl : l ↦ some hl_val(#7) ⊢ WP hl(let x := #l; !x) {{ v, Φ v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ x, ⌜x = hl_val(#7)⌝ -∗ Φ x ∗Hl : l ↦ some hl_val(#7) ⊢ WP hl(!#l) {{ v, Φ v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ x, ⌜x = hl_val(#7)⌝ -∗ Φ x ⊢ ▷ (l ↦ some hl_val(#7) -∗ Φ hl_val(#7)) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ x, ⌜x = hl_val(#7)⌝ -∗ Φ x ∗_Hl : l ↦ some hl_val(#7) ⊢ Φ hl_val(#7) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFΦ:Val → IProp GFl:Loc⊢ ∗_Hl : l ↦ some hl_val(#7) ⊢ ⌜hl_val(#7) = hl_val(#7)⌝ All goals completed! 🐙 
-- TODO (upstream — iris-lean): port a `wp_apply` convenience
-- tactic that combines `wp_bind` + `iapply`. The hand-written
-- composition currently used in client proofs works but is
-- uglier than the Rocq tutorial's `wp_apply writeread_spec_2`.

-- Rocq tutorial reference (composing two specs):
--   Lemma prog_add_2_spec'' : ⊢ WP prog + #2 {{ v, ⌜v = #5⌝ }}.
--   Proof.
--     wp_apply prog_spec_2.
--     iIntros "%w ->". wp_pure. done.
--   Qed.