refactor: separate the generic and the monadic weakest-precondition modules - #14778
Merged
Conversation
…he order library This PR states the frame closure as a map from predicate transformers to predicate transformers. It also moves the closure and `PredTrans` to `Std.Internal.Order`. The closure took a bare post-transformer before. Its type therefore did not show what it was. It is now `PredTrans.frameClosure op : PredTrans Pred EPred β → PredTrans Pred EPred β`. The `WP` instance built from it reduces to `wpTrans x := (base.wpTrans x).frameClosure op`. `Std/Internal/Do/PredTrans.lean` is gone. The structure and its instances are now together in `Lean.Order`, because instances belong with their type. The declarations that name `EPost` remain in `Std.Internal.Do`, because the order library does not import `EPost`. `PredTrans.pushExcept` and `pushOption` join the `WPMonad` instances that use them. The two `EPost.Cons` helpers join the rest of the `EPost` API in `ExceptPost.lean`. Four proofs in `ExceptT` and `OptionT` now use `apply_pushExcept` and `apply_pushOption`. Before, they restated the unfolded form. The split changes one behaviour. It changes the relative declaration order of the three `MonadExceptOf` instances on `PredTrans`. Instance search at equal priority therefore reaches them in a different order. No goal in the tree matches more than one of them.
…odules This PR splits four modules of `Std.Internal.Do` so that each module holds either generic or monadic material. The generic side names no monad. It applies to any program type with a `WP` interpretation, including deep embeddings. `WP`, `wp` and the `wp_consequence` family stay in `Std.Internal.Do.WP.Basic`. `WP.Frames` stays in `Std.Internal.Do.WP.Frame`. The `WPConjunctive` class stays in `Std.Internal.Do.WP.Conjunctive`. `Triple` and its notation stay in `Std.Internal.Do.Triple.Basic`. `WPMonad`, the transformer instances, the adequacy lemmas, the `WPConjunctive` instances and `WPMonad.of_frameClosure` move under `Std.Internal.Do.WP.Monad`. The triples for `pure`, `bind`, `map` and `seq` move to `Std.Internal.Do.Triple.Monad`. `Std.Internal.Do.WP.Lemmas` becomes `Std.Internal.Do.WP.Monad.Lemmas`, because every lemma in it names a monad. The namespaces stay unchanged. Only files move. A later PR will rename the result to `Std.WP` and `Std.WP.Do`. `Std.Internal.Do.WP` publicly imports `Std.Internal.Do.WP.Monad`, so `import Std.Internal.Do` still supplies every instance. This PR stacks on #14774. It must be rebased once that PR merges.
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This PR rewrites the module, class, and field docstrings in `Std.Internal.Do.WP.Conjunctive`. They glossed `wp_meet_wp_le` as mapping a meet of postconditions below the `wp` of their meet, but the left-hand side `wp x Q₁ E₁ ⊓ wp x Q₂ E₂` is a meet of two weakest preconditions. The docstrings now say that this meet lies below the weakest precondition `wp x (Q₁ ⊓ Q₂) (E₁ ⊓ E₂)` of the componentwise meet of the postconditions.
This PR expands the module docstring of `Std.Internal.Do.WP.Basic` with the `outParam` behaviour of the `WP` class and two worked examples, and it states what the frame closure buys a separation logic. The `WP` docstring now says that `Prog` determines `Value`, `Pred` and `EPred`, and gives `EStateM ε σ` and the `Cmd` deep embedding of `tests/elab/vcgenImp.lean` as the two ends of the range of program types. `WPMonad.of_frameClosure` gains a paragraph on the frame obligation moving from the spec application site to the spec proof site. The import of `Std.Internal.Do.WP.Frame` in `RuleConstruction.lean` gains a comment, since the constant it supplies is built by name and no signature in that file mentions it.
Master carries PR 14777, which moved the tactic to `Lean.Elab.Tactic.VCGen`. The import of `Std.Internal.Do.WP.Frame` that this branch adds moves with `RuleConstruction.lean` to the new path.
The conflicts in `Std/Internal/Do/WP/{Basic,Frame}.lean` and `Lean/Elab/Tactic/VCGen/LatticeOp.lean` come from PR 14774 landing as a squash. Master's `src/Std/` is identical to the base of this branch, so the resolution keeps this branch's split for the two `Std` files and master's version of `LatticeOp.lean`.
This PR marks the import that `RuleConstruction.lean` needs for `WP.Frames.op_wp_upperAdjoint_le_wp` as a `meta import`, which states that the constant is needed at elaboration time only. The tactic builds that constant by name with `mkAppOptM`, so no signature in the file mentions it. `meta import` says so in the syntax.
This PR rewrites the closing paragraph of the `WPMonad.of_frameClosure` docstring to state that every frame passes through the `wp` and that a caller of a spec picks a frame and applies the frame rule. It also shortens the deep-embedding paragraph of the `Std.Internal.Do.WP.Basic` module docstring to speak of `wp` and an operational semantics such as an omnisemantics.
sgraf812
marked this pull request as ready for review
August 13, 2026 15:06
sgraf812
enabled auto-merge
August 13, 2026 15:09
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR splits the modules of
Std.Internal.Doso that each one holds generic material or monadic material. The generic modules apply to any program type with aWPinterpretation, including deep embeddings.The monadic material moves under
Std.Internal.Do.WP.MonadandStd.Internal.Do.Triple.Monad. The namespaces stay the same, andimport Std.Internal.Dostill supplies every instance. A later PR renames the result toStd.WPandStd.WP.Do.