feat: new foundations for `mvcgen` tactic by volodeyka · Pull Request #12965 · leanprover/lean4

volodeyka · 2026-03-18T11:18:33Z

This PR Introduces new foundations for reasoning about monadic Lean code. Eventually we will port mvcgen on top of these new foundations, to make the framework more general and robust.

Key issues, new metatheory is supposed to solve are

It gives more flexibility over what an assertion language for pre-/post-conditions of monadic Hoare triples can be. In particular, any CompleteLattice might become a pre-/post-condtions language, not only SPred. It potentially gives an opportunity to reason about probabilistic monads, where assertion language are distributions. This also simplifies the metatheory of monadic Hoare triples, as it does not require defining the notion of SPred, and allows users to work in a fairly common interface of CompleteLattice
It splits the post-conditions of Hoare triples/ WPs into two: (1) post for post-conditions on terminating paths and (2) epost for post-conditions on abrupt paths. Current foundations always bundle them into a pair, which inevitably leads to constructing and eliminating such pairs everywhere in the code.
It relaxes some conditions that the current foundations require for instantiating WPMonad type class. In particular we do not require wp to distribute over bind any more. Instead, we require just wp x (fun x => wp (f x) post epost) epost ⊑ wp (x >>= f) post epost, i.e. the distributed wp must only imply the non-distributed one (and not necessarily vice versa). With this we can define WPMonad for Separation Logic, where wp only distributes over bind on local-footprint computations.
It solves some universe polymorphism issues. As now universe levels of assertion languages are independent of universe levels in the monad, one can define WPMonad Id.{u} Prop EPost⟨⟩, which means that for arbitrary level Id the language for pre-/post-conditions is going to be just Prop and the language for post-conditions on abrupt exits is idle.

sgraf812

Generally fine, but there are a couple of smaller things worth of cleanup that I didn't bother addressing. Let Claude have a second-opinion/review pass on this for cleanup.

…OptionT WP, remove dead code Structural changes: - Make PredTrans a structure with `apply` field, add extensionality lemma - Add apply_* simp framework (apply_pure, apply_bind, apply_map, etc.) - Add pushOption/EPost.cons.pushOption for OptionT support Renames (per Sebastian Graf's review of PR #12965): - WPMonad → WP (class name) - wp_cons → wp_consequence (and derived names) - wp_trans_pure/bind/monotone → wpTrans_pure/bind/monotone - LawfulWPMonadLift → LawfulWPLift, etc. Class merge and parameter renames: - Merge AssertionLang + ExceptAssertionLang into single `Assertion` - Rename type params: l → Pred, el/e → EPred OptionT support: - Add OptionT.instWP using pushOption with EPost.cons Pred EPred - Uncomment all OptionT WP lemmas and Triple specs Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

… args Change AssertionLang and ExceptAssertionLang from standalone classes to class abbrevs over CompleteLattice, and require them as class arguments to WPMonad rather than using extends. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- LatticeExt: wrap in `namespace Lean.Order`, scope ⊤ ⊓ ⊔ ⌜⌝ notations - Frame: move from `namespace Loom` to `namespace Lean.Order`, scope ⇨ - Frame: rename field `inf_sup` → `meet_sup` Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- Convert `inductive EPost.nil` and `inductive EPost.cons` to `structure` - Remove manual head/tail projections (now auto-generated) - Simplify PartialOrder/CompleteLattice instances using PProd - Rename `mk_rel` → `rel_mk` Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…OptionT WP, remove dead code Structural changes: - Make PredTrans a structure with `apply` field, add extensionality lemma - Add apply_* simp framework (apply_pure, apply_bind, apply_map, etc.) - Add pushOption/EPost.cons.pushOption for OptionT support Renames (per Sebastian Graf's review of PR #12965): - WPMonad → WP (class name) - wp_cons → wp_consequence (and derived names) - wp_trans_pure/bind/monotone → wpTrans_pure/bind/monotone - LawfulWPMonadLift → LawfulWPLift, etc. Class merge and parameter renames: - Merge AssertionLang + ExceptAssertionLang into single `Assertion` - Rename type params: l → Pred, el/e → EPred OptionT support: - Add OptionT.instWP using pushOption with EPost.cons Pred EPred - Uncomment all OptionT WP lemmas and Triple specs Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…nts by removing redundant attributes. Introduce `open Classical` for improved readability.

…emmas.lean`. Update documentation for clarity and consistency, replacing `EPred` with `eInvariant EPred` in relevant theorem signatures.

sgraf812

More tomorrow. I'm slowly coming to think that it will be more efficient to merge soon and then guide an AI to do the changes that I request here rather then writing comments on GH to have you implement them.

sgraf812 · 2026-04-16T13:36:37Z

+/-- Hoare triple notation without exception postcondition (defaults to `⊥`). -/
+notation:60 "⦃ " pre " ⦄ " x " ⦃ " post " ⦄" => Triple pre x post ⊥
+/-- Hoare triple notation with a binder for the return value. -/
+notation:60 "⦃ " pre " ⦄ " x " ⦃ " v ", " post " ⦄" => Triple pre x (fun v => post) ⊥


This is a breaking change to every existing use of notation... We should ensure that it is actually better than what we currently have. Let's discuss this in our next meeting.

What I like about what we currently have is that ⦃pre⦄ x ⦃⇓r => post⦄ evokes similarity to Lean's fun r => post syntax. On the other hand, ⦃pre⦄ x ⦃r, post⦄ looks neater and is closer to what people might be used to from pen and paper proofs. However, it's quite un-Lean-ish.

Furthermore, ⦃pre⦄ x ⦃⇓? r => post⦄ can be used to say Triple $pre $x (fun r => $post) T and there presently is no notation to say this in your patch. Generally it seems that you lose notation whenever the epost is non-bottom.

Maybe the cleanest solution is:

⦃pre⦄ x ⦃post⦄ => Triple pre x post ⊥ (your first notation)

⦃pre⦄ x ⦃post⦄? => Triple pre x post T

⦃pre⦄ x ⦃post⦄ ⦃eposts...⦄ => Triple pre x post epost<eposts...> (likely needs to be a macro)

⦃pre⦄ x ⦃r => post⦄ => ⦃pre⦄ x ⦃fun r => post⦄ (compositional expansion; the fun is effectively optional. Not sure if that's worth it. I tend to think it isn't.)

As for my taste, I would want to avoid unicode whenever possible. I like ⇓and ⇓? symbols, but I feel it requires a little too much of a context. If we add it, it will be giving Coq-SSReflect vibes, where there are tons of conventions, which are really smart and useful, but make the overall framework highly exclusive. You really need to get into the head of developers to understand what's going on.

for , versus =>, I was thinking of it a lot, and finally deceid on , because it is already used in big operator notations. It is so standard in maths, that it kinda overrides Lean style for me sometimes.
I think we should either use , or jut go with ⦃fun r => post⦄. Omitting fun might confuse people

I don't have any super strong opinion about ⦃pre⦄ x ⦃post⦄?. We can add it if you think it is going to be used

I would change ⦃pre⦄ x ⦃post⦄ ⦃eposts...⦄ into ⦃pre⦄ x ⦃post; eposts...⦄ and also separate eposts with ;. Then it would be somewhat uniform.

Agreed on unicode. we should ensure that ⦃ can be typed as {{ as well.

, sounds fine then.

⦃post⦄? is useful because you can't really write T in the syntax I proposed

I would change ⦃pre⦄ x ⦃post⦄ ⦃eposts...⦄ into ⦃pre⦄ x ⦃post; eposts...⦄ and also separate eposts with ;

Hmm, I fear that ; is not enough signalling. It is also ambiguous with ⦃v, match v with none => ...; some _ => ...; blah⦄. Note that Iris separates into two {{}} as well. Also do you expect users to write ⦃post; epost<e1,e2,e3>⦄ (note that we switched from , to ;) or is it more like ⦃post; e1; e2; e3⦄?

…e CompleteLattice.pure to Assertion.ofProp Move `class abbrev Assertion` and CCPO instance from WP/Basic.lean into the renamed Assertion.lean. Rename `CompleteLattice.pure` to `Assertion.ofProp` and rename all related lemmas (`trueE` → `ofProp_true`, `falseE` → `ofProp_false`, `LE.pure_imp` → `ofProp_imp`, `LE.pure_intro` → `ofProp_intro`, `pure_intro_l` → `ofProp_intro_l`, `pure_intro_r` → `ofProp_intro_r`).

Add Gadget to Triple umbrella import. Remove duplicate List.Cursor and Std.Legacy.Range.toList definitions from Experimental SpecLemmas, importing them from the non-Experimental Std.Do.Triple.SpecLemmas instead.

leanprover-bot · 2026-04-17T09:17:19Z

Reference manual CI status:

✅ Reference manual branch lean-pr-testing-12965 has successfully built against this PR. (2026-04-17 09:17:17) View Log
🟡 Reference manual branch lean-pr-testing-12965 build against this PR didn't complete normally. (2026-04-17 09:18:51) View Log
✅ Reference manual branch lean-pr-testing-12965 has successfully built against this PR. (2026-04-17 11:08:43) View Log
🟡 Reference manual branch lean-pr-testing-12965 build against this PR didn't complete normally. (2026-04-17 11:10:30) View Log

mathlib-lean-pr-testing · 2026-04-17T10:14:01Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12965 has successfully built against this PR. (2026-04-17 10:13:59) View Log

mathlib-lean-pr-testing · 2026-04-17T11:58:35Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12965 has successfully built against this PR. (2026-04-17 11:58:34) View Log

volodeyka requested review from TwoFX and sgraf812 as code owners March 18, 2026 11:18

sgraf812 reviewed Mar 24, 2026

View reviewed changes

volodeyka added the changelog-library Library label Mar 25, 2026

volodeyka marked this pull request as draft March 25, 2026 08:48

volodeyka changed the title ~~feat: New foundations for mvcgen tactic~~ feat: new foundations for mvcgen tactic Mar 25, 2026

volodeyka mentioned this pull request Mar 27, 2026

Apply PR #12965 review: renames, structures, OptionT WP verse-lab/loom2#4

Merged

1 task

github-actions Bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Apr 16, 2026

volodeyka and others added 10 commits April 16, 2026 17:47

add new mvcgen foundations

da29364

remove some garbage

566dec2

add missing lemmas

4be8d8d

revert changes to toolchain

e519abd

more to new Std/Experimental folder

19048cc

rename WP to WPMonad

847630b

volodeyka force-pushed the vova/new-do-foundations branch from b446ea9 to 847630b Compare April 16, 2026 09:52

volodeyka removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Apr 16, 2026

volodeyka added 6 commits April 16, 2026 17:56

remove redundant instance

c9d704f

minimise import in Frame

17f8ac7

Refactor CompleteLattice.pure definition and simplify theorem stateme…

a37fe94

…nts by removing redundant attributes. Introduce `open Classical` for improved readability.

add grind annotation

2bbcd29

Refactor loop invariant and exception invariant definitions in `SpecL…

6edfabe

…emmas.lean`. Update documentation for clarity and consistency, replacing `EPred` with `eInvariant EPred` in relevant theorem signatures.

revert test_vcgen.lean to master version

df0b0a5

sgraf812 reviewed Apr 16, 2026

View reviewed changes

volodeyka added 2 commits April 17, 2026 15:03

remove unused withName syntax/macro from Frame.lean

41a8776

improve Frame class docstring

b8d9dd1

volodeyka added 10 commits April 17, 2026 15:04

fix duplicate Assertion in WP/Basic.lean docstring

a2433d3

add variable block to clean up WP/Basic.lean theorem signatures

8bc38dd

add missing docstrings to WP/Basic.lean

e9eee74

rename latticeTop to top, remove latticeBot in favor of CCPO.bot

bc5999a

change Triple from inductive to structure

428fb83

remove redundant @[simp] from EStateM lemmas in Lemmas.lean

76ef0c4

move apply_pushExcept and apply_pushArg to PredTrans namespace

30eda59

factor out common variables into sections in WP/Lemmas.lean

eba79c1

fix orphaned Experimental modules in import structure

485d2be

Add Gadget to Triple umbrella import. Remove duplicate List.Cursor and Std.Legacy.Range.toList definitions from Experimental SpecLemmas, importing them from the non-Experimental Std.Do.Triple.SpecLemmas instead.

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 17, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 17, 2026

Update lean-toolchain for testing leanprover/lean4#12965

f1c2c2b

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 17, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 17, 2026

Update lean-toolchain for testing leanprover/lean4#12965

1873df4

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 17, 2026

Update lean-toolchain for testing leanprover/lean4#12965

0dce63c

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Apr 17, 2026

volodeyka added 3 commits April 17, 2026 17:35

add Experimental module imports to Std.Do

46f9fdb

rename Std.Experimental to Std.Internal

b1d5d5c

scope triple notation

7012d7c

mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 17, 2026

move internal imports

4bb412b

volodeyka marked this pull request as ready for review April 17, 2026 10:59

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 17, 2026

Update lean-toolchain for leanprover/lean4#12965

252d431

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 17, 2026

Update lean-toolchain for leanprover/lean4#12965

bfae839

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 17, 2026

Update lean-toolchain for leanprover/lean4#12965

47f9632

Conversation

volodeyka commented Mar 18, 2026 • edited by sgraf812 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgraf812 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

sgraf812 Apr 16, 2026

Choose a reason for hiding this comment

Uh oh!

volodeyka Apr 17, 2026

Choose a reason for hiding this comment

Uh oh!

sgraf812 Apr 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leanprover-bot commented Apr 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 17, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

volodeyka commented Mar 18, 2026 •

edited by sgraf812

Loading

sgraf812 Apr 17, 2026 •

edited

Loading

leanprover-bot commented Apr 17, 2026 •

edited

Loading