From 7894e9b73d2dec5164c3e2801e5dbdd1266b69f4 Mon Sep 17 00:00:00 2001 From: fresheed Date: Thu, 16 Jul 2026 14:15:16 +0200 Subject: [PATCH 1/6] half of Later chapter --- IrisTutorial/Later.lean | 107 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 105 insertions(+), 2 deletions(-) diff --git a/IrisTutorial/Later.lean b/IrisTutorial/Later.lean index 5ea9ff8..ceca40b 100644 --- a/IrisTutorial/Later.lean +++ b/IrisTutorial/Later.lean @@ -1,6 +1,13 @@ import VersoManual import BookGen.Meta.Lean +import Iris.Instances.UPred +import Iris.ProofMode +import Iris.HeapLang +import Iris.HeapLang.Lib.Par +import Iris.HeapLang.PrimitiveLaws +import Iris.HeapLang.ProofMode + open Verso.Genre Manual open Verso.Genre.Manual.InlineLean open BookGen @@ -9,5 +16,101 @@ set_option pp.rawOnError true #doc (Manual) "The Later Modality and Recursive Functions" => -This chapter has not yet been ported. The Rocq source is -`iris-tutorial/theories/later.v`. +# Introduction + +Iris is a step-indexed logic, meaning it has a built-in notion of +time. This can be expressed with the later modality `▷ P` signifying +that `P` holds after one time step. With the reading of propositions +as describing owned resources, `▷ P` asserts that we will own the +resources described by `P` after one time step. + +The later modality is used quite extensively in Iris. We have already +seen that it is used to define Hoare triples, but it has many more +uses. For instance, it is a prime tool for reasoning about recursive +programs. It can be used to write specifications that capture the +minimum number of steps taken by a program. It is also an integral +part of working with invariants, which we introduce in a later +chapter. + +```savedImport +import Iris.Instances.UPred +import Iris.ProofMode +import Iris.HeapLang +import Iris.HeapLang.Lib.Par +import Iris.HeapLang.PrimitiveLaws +import Iris.HeapLang.ProofMode +``` + +```savedLean +section later_general +open Iris +variable (σ : BundledGFunctors) +``` + +# Basics of later modality + +The later modality is monotone, meaning that if we know `P ⊢ Q`, then +we can also conclude `▷ P ⊢ ▷ Q`. In words, if we know that `P` +entails `Q`, then we also know that if we get `P` after one step, we +will also get `Q` after one step. This is captured by the `inext` +tactic, which introduces a later while stripping laters from our +hypotheses. + +```savedLean +theorem later_mono (P Q : IProp σ): (Q ⊢ P) → (▷ Q ⊢ ▷ P) := by + intro qp + iintro q + inext + iapply qp $$ q +``` + +The `inext` tactic is actually a specialisation of the more general +`imodintro` tactic, which works with all modalities. The `imodintro` +tactic can be invoked with the introduction pattern `!>`, making it +less verbose to handle the later modality. + +```savedLean +theorem later_mono' (P Q : IProp σ) : (Q ⊢ P) → (▷ Q ⊢ ▷ P) := by + intro qp + iintro q !> + iapply qp $$ q +``` + +The later modality weakens propositions; owning resources now is +stronger than owning them later. In other words, `P ⊢ ▷ P`. This means +that we can always remove a later from the goal, regardless of whether +our hypotheses have a later. + +```savedLean +theorem later_weak (P : IProp σ) : P ⊢ ▷ P := by + iintro p + inext + itrivial +``` + +The later modality distributes over `∧`, `∨`, `∗`, and is preserved +by `∃` and `∀`. This means we can destruct these constructs +regardless of being prefaced by any laters. + +```savedLean +theorem later_sep (P Q: IProp σ): ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q := by + isplit + . iintro ⟨p, q⟩ + iframe + . iintro ⟨p, q⟩ !> + iframe +``` + +As a consequence of monotonicity, weakening, and distribution over +`∗`, the `inext` tactic can simply ignore hypotheses in the context +that do not have a later on them. + +```savedLean +theorem later_impl (P Q : IProp σ) : P ∗ ▷ (P -∗ Q) -∗ ▷ Q := by + -- Exercise + sorry +``` + +```savedLean +end later_general +``` From 2d0364df0cea51d9a8b48524bba69302c0a9cfa9 Mon Sep 17 00:00:00 2001 From: fresheed Date: Thu, 16 Jul 2026 14:38:04 +0200 Subject: [PATCH 2/6] second part of Later chapter --- IrisTutorial/Later.lean | 103 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 103 insertions(+) diff --git a/IrisTutorial/Later.lean b/IrisTutorial/Later.lean index ceca40b..1767609 100644 --- a/IrisTutorial/Later.lean +++ b/IrisTutorial/Later.lean @@ -114,3 +114,106 @@ theorem later_impl (P Q : IProp σ) : P ∗ ▷ (P -∗ Q) -∗ ▷ Q := by ```savedLean end later_general ``` + +# Tying Later to Program Steps + +A somewhat important clarification is that the later modality exists +independently of the specific language Iris is instantiated with; the +later modality is part of the Iris base logic. However, when +instantiating Iris with a language, the obvious choice is to tie a +single `▷` to a single program step. This is also the choice that has +been made for HeapLang – every time we use one of the `wp_*` tactics to +symbolically execute a single step, we let time tick one unit forward, +stripping away a single `▷` from our hypotheses. + +To see this in action, let us look at a simple program: `#1 + #2 * #3`. +This program takes two steps to evaluate, so we can prove that if a +proposition holds after two steps, it will hold after the program has +terminated. + +```savedLean +section later_specs +open Iris HeapLang Par +variable [HeapLangGS hlc GF] +``` + +```savedLean +theorem take_2_steps (P: IProp GF): + ▷ ▷ P -∗ WP (hl(#1 + #2 * #3)) {{ _v, P }} := by + iintro P + wp_pure; wp_pure + itrivial +``` + +The reason this works is that under the hood of `WP`, there is a later +for every step of the program. Thus, the `wp_*` tactics can use the +properties mentioned in the previous section to remove laters from the +context, similarly to `inext`. + +Further, it turns out that in many cases, a `▷` on an assumption can +be safely ignored. For instance, in the example below, we only own the +points-to predicate *later*, yet we can still perform the load. + +```savedLean +theorem later_points_to (l : Loc): + ▷ (l ↦ hl_val(#5)) -∗ WP hl(!#l + #1) {{v, ⌜v = hl_val(#6)⌝}} := by + iintro Hl + wp_bind !#l + iapply wp_load $$ Hl + iintro !> Hl + wp_pure + itrivial +``` + +The technical reason for this is that points-to predicates are +so-called *timeless* propositions, and the `wp_*` tactics are aware of +this fact. We study timeless propositions further in a separate +chapter. + +## Löb Induction + +The later modality allows for a strong induction principle called Löb +induction. Essentially, Löb induction states that to prove a +proposition `P`, we are allowed to assume that `P` holds later, i.e. +`▷ P`. Formally, we have `□ (▷ P -∗ P) -∗ P`. Recall that `▷` +represents a single step in the logic. Löb induction essentially +performs induction in the number of steps. Intuitively, Löb induction +states that if we can show that whenever `P` holds for strictly +smaller than `n` steps, we can prove that `P` holds for `n` steps, +then `P` holds for all steps. + +We can use this principle to prove many properties of recursive +programs. To see this in action, we will define a simple recursive +function that increments a counter. + +```savedLean +def count: Val := hl_val% + rec cnt x := cnt (x + #1) +``` + +This function never terminates for any input as it will keep calling +itself with larger and larger inputs. To show this, we pick the +postcondition `False`. We can now use Löb induction, along with +`wp_rec`, to prove this specification. + +```savedLean +theorem count_spec (x : Int): ⊢@{IProp GF} WP hl(&count #x) {{_v, False}} := by + /- The tactic for Löb induction, `iloeb`, requires us to specify the + name of the induction hypothesis, which we here call `IH`. + Optionally, it can also universally quantify over any of our variables + before performing induction. We here universally quantify over `x` as it + changes for every recursive call. -/ + iloeb as IH generalizing %x + /- `iloeb` automatically introduces the universally quantified variables in + the goal, so we can proceed to execute the function. -/ + wp_rec + wp_pures + /- Since we have taken steps, the `▷` in our induction hypothesis has + been stripped, allowing us to apply the hypothesis for the recursive + call. -/ + iapply IH +``` + +```savedLean +end later_specs +``` From 37fa19df46d3d9851215fb851c8ee2ef86fabb09 Mon Sep 17 00:00:00 2001 From: fresheed Date: Thu, 16 Jul 2026 15:17:51 +0200 Subject: [PATCH 3/6] small changes --- IrisTutorial/Later.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/IrisTutorial/Later.lean b/IrisTutorial/Later.lean index 1767609..7483e7c 100644 --- a/IrisTutorial/Later.lean +++ b/IrisTutorial/Later.lean @@ -170,7 +170,7 @@ so-called *timeless* propositions, and the `wp_*` tactics are aware of this fact. We study timeless propositions further in a separate chapter. -## Löb Induction +# Löb Induction The later modality allows for a strong induction principle called Löb induction. Essentially, Löb induction states that to prove a From 31d096ad90b9a2f6d96f752dd757ad005ce6bf5f Mon Sep 17 00:00:00 2001 From: fresheed Date: Mon, 20 Jul 2026 13:37:37 +0200 Subject: [PATCH 4/6] updated README --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 853665b..2741e3b 100644 --- a/README.md +++ b/README.md @@ -24,6 +24,7 @@ type-checked: - **Specifications** - **Persistently** - **Linked Lists** +- **Later** The remaining chapters are stubs ("This chapter has not yet been ported") pending translation from their Rocq sources. From 40168f9b2570792ec461c2168b88e9b8fb0b7557 Mon Sep 17 00:00:00 2001 From: fresheed Date: Mon, 20 Jul 2026 13:46:41 +0200 Subject: [PATCH 5/6] fixed long lines warning --- IrisTutorial/Later.lean | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/IrisTutorial/Later.lean b/IrisTutorial/Later.lean index 7483e7c..b08fa63 100644 --- a/IrisTutorial/Later.lean +++ b/IrisTutorial/Later.lean @@ -57,7 +57,8 @@ tactic, which introduces a later while stripping laters from our hypotheses. ```savedLean -theorem later_mono (P Q : IProp σ): (Q ⊢ P) → (▷ Q ⊢ ▷ P) := by +theorem later_mono (P Q : IProp σ) : + (Q ⊢ P) → (▷ Q ⊢ ▷ P) := by intro qp iintro q inext @@ -70,7 +71,8 @@ tactic can be invoked with the introduction pattern `!>`, making it less verbose to handle the later modality. ```savedLean -theorem later_mono' (P Q : IProp σ) : (Q ⊢ P) → (▷ Q ⊢ ▷ P) := by +theorem later_mono' (P Q : IProp σ) : + (Q ⊢ P) → (▷ Q ⊢ ▷ P) := by intro qp iintro q !> iapply qp $$ q @@ -93,7 +95,8 @@ by `∃` and `∀`. This means we can destruct these constructs regardless of being prefaced by any laters. ```savedLean -theorem later_sep (P Q: IProp σ): ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q := by +theorem later_sep (P Q : IProp σ) : + ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q := by isplit . iintro ⟨p, q⟩ iframe @@ -106,7 +109,8 @@ As a consequence of monotonicity, weakening, and distribution over that do not have a later on them. ```savedLean -theorem later_impl (P Q : IProp σ) : P ∗ ▷ (P -∗ Q) -∗ ▷ Q := by +theorem later_impl (P Q : IProp σ) : + P ∗ ▷ (P -∗ Q) -∗ ▷ Q := by -- Exercise sorry ``` @@ -156,7 +160,8 @@ points-to predicate *later*, yet we can still perform the load. ```savedLean theorem later_points_to (l : Loc): - ▷ (l ↦ hl_val(#5)) -∗ WP hl(!#l + #1) {{v, ⌜v = hl_val(#6)⌝}} := by + ▷ (l ↦ hl_val(#5)) -∗ + WP hl(!#l + #1) {{v, ⌜v = hl_val(#6)⌝}} := by iintro Hl wp_bind !#l iapply wp_load $$ Hl @@ -197,20 +202,23 @@ postcondition `False`. We can now use Löb induction, along with `wp_rec`, to prove this specification. ```savedLean -theorem count_spec (x : Int): ⊢@{IProp GF} WP hl(&count #x) {{_v, False}} := by - /- The tactic for Löb induction, `iloeb`, requires us to specify the - name of the induction hypothesis, which we here call `IH`. - Optionally, it can also universally quantify over any of our variables - before performing induction. We here universally quantify over `x` as it +theorem count_spec (x : Int) : + ⊢@{IProp GF} WP hl(&count #x) {{_v, False}} := by + /- The tactic for Löb induction, `iloeb`, requires us to + specify the name of the induction hypothesis, which we + here call `IH`. Optionally, it can also universally + quantify over any of our variables before performing + induction. We here universally quantify over `x` as it changes for every recursive call. -/ iloeb as IH generalizing %x - /- `iloeb` automatically introduces the universally quantified variables in - the goal, so we can proceed to execute the function. -/ + /- `iloeb` automatically introduces the universally + quantified variables in the goal, so we can proceed to + execute the function. -/ wp_rec wp_pures - /- Since we have taken steps, the `▷` in our induction hypothesis has - been stripped, allowing us to apply the hypothesis for the recursive - call. -/ + /- Since we have taken steps, the `▷` in our induction + hypothesis has been stripped, allowing us to apply + the hypothesis for the recursive call. -/ iapply IH ``` From 3e0a92af05e9faaeaa9bf3ba629b3be8ef3f4e19 Mon Sep 17 00:00:00 2001 From: fresheed Date: Wed, 5 Aug 2026 15:04:56 +0200 Subject: [PATCH 6/6] used wp_* heap tactics --- IrisTutorial/Later.lean | 6 ++---- lake-manifest.json | 24 ++++++++++++------------ lakefile.toml | 8 ++++---- lean-toolchain | 2 +- 4 files changed, 19 insertions(+), 21 deletions(-) diff --git a/IrisTutorial/Later.lean b/IrisTutorial/Later.lean index b08fa63..3ccc9f3 100644 --- a/IrisTutorial/Later.lean +++ b/IrisTutorial/Later.lean @@ -162,10 +162,8 @@ points-to predicate *later*, yet we can still perform the load. theorem later_points_to (l : Loc): ▷ (l ↦ hl_val(#5)) -∗ WP hl(!#l + #1) {{v, ⌜v = hl_val(#6)⌝}} := by - iintro Hl - wp_bind !#l - iapply wp_load $$ Hl - iintro !> Hl + iintro _ + wp_load wp_pure itrivial ``` diff --git a/lake-manifest.json b/lake-manifest.json index cd5f130..72e317e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,47 +5,47 @@ "type": "git", "subDir": "Iris", "scope": "", - "rev": "5a790aed0dcad30219aa218c88a7fd306c092fae", + "rev": "6a9d0cfd5d8d2fdfc36d7eb8c47d3b4bc7bea491", "name": "iris", "manifestFile": "lake-manifest.json", - "inputRev": "5a790aed0dcad30219aa218c88a7fd306c092fae", + "inputRev": "6a9d0cfd5d8d2fdfc36d7eb8c47d3b4bc7bea491", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "", - "rev": "b677415e8a0becccc0b850137c2d8f6205132a91", + "rev": "e09d21a5f7f66c9fc985b73197708298569bf583", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa08db58b30eb033edcdab331bba000827f9f785", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/illuminate", "type": "git", "subDir": null, "scope": "", - "rev": "20b8493528eed2fac9827ce18d41c475f0e1c50a", + "rev": "b3debfe6b629192033ef87257e1c60201881646f", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041", + "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 480804d..b095814 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,15 +8,15 @@ defaultTargets = ["textbook"] [[require]] name = "verso" git = "https://github.com/leanprover/verso" -rev = "v4.31.0" +rev = "v4.32.0" -# iris-lean has no v4.30.0 release tag, so we pin to an exact commit that -# is compatible with the Lean toolchain in `lean-toolchain` (leanprover/lean4:4.31.0). +# iris-lean's v4.32.0 tag, compatible with the Lean toolchain in +# `lean-toolchain` (leanprover/lean4:v4.32.0). [[require]] name = "iris" git = "https://github.com/leanprover-community/iris-lean.git" subDir = "Iris" -rev = "5a790aed0dcad30219aa218c88a7fd306c092fae" +rev = "6a9d0cfd5d8d2fdfc36d7eb8c47d3b4bc7bea491" # Book generation machinery inherited from the Verso textbook template # (savedLean/savedImport elaborators, bibliography helpers). No root module diff --git a/lean-toolchain b/lean-toolchain index 18640c8..e29f71d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 +leanprover/lean4:v4.32.1 \ No newline at end of file