feat: support well-founded and state-dependent termination measures in Spec.repeatM - #14507
Merged
Conversation
sgraf812
force-pushed
the
sg/vcgen-variant
branch
from
July 23, 2026 14:14
41bb8f5 to
8b2f3b5
Compare
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
sgraf812
changed the title
sgraf812
marked this pull request as ready for review
August 7, 2026 17:40
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Aug 7, 2026
This PR lets `vcgen` loop measures depend on monadic state, matching the strength of legacy mvcgen's `WhileVariant`. `Assertion.NondetFun` equips an assertion lattice with total nondeterministic functions into an `outParam` type (`Prop ↦ α`, `σ → Pred ↦ σ → Fun`), with covering law `P ⊑ ⨆ a, evalsTo f a ⊓ P`. `Spec.repeatM` quantifies the current measure value via `evalsTo`, so measures such as `σ → Nat` work without baking `PostShape`/`SVal` into the abstract lattice. Co-authored-by: Cursor <cursoragent@cursor.com>
This PR generalizes the termination measure of `vcgen`'s loop specifications `Spec.repeatM` and `Spec.forIn_loop`: a `RepeatVariant` now bundles a type of measure values together with a well-founded relation and a lattice-embedded evaluation, so loop measures can map into any type with a `WellFoundedRelation` instance (such as lexicographic products) and may read monadic state. Build one from a measure function with `RepeatVariant.ofMeasure`; decrease proof obligations for state-independent `Nat`-valued measures keep their `⌜f a' < ma⌝ ⊓ P` shape and remain `grind`/`finish`-friendly, while other measure types collapse via `RepeatVariant.decreasesTo_ofMeasure` to the goal shape produced by `termination_by`, so `decreasing_tactic` applies. `NondetFun` now computes the type of pinned measure values as an `outParam` from the assertion lattice and the measure's function type, so elaborating `RepeatVariant.ofMeasure f` determines the value type from `f` alone. The pure instance works in any assertion lattice at low priority, so state-independent measures need no dummy state binder under stateful lattices. The bundled `RepeatVariant` structure keeps the value type and both instances implicit at construction, so the spec theorems carry no instance arguments that rule application would have to synthesize. The step postcondition is stated via `RepeatVariant.decreasesTo`, which pins the next measure value under a join; for state-independent measures the simp/grind lemmas `decreasesTo_ofMeasure` and `decreasesTo_ofMeasure_nat` eliminate the join, so VCs contain no existential. `ofMeasure` is `@[instance_reducible]` with a packed simp/grind API (`γ_ofMeasure`, `eval_ofMeasure`, `rel_ofMeasure`, `rel_ofMeasure_nat`, `NondetFun.evalsTo_pure`): patterns stay valid because attribute-time pattern compilation only unfolds reducible definitions, while simp matching and type class resolution see through the constructor at instances transparency. The proof of `Spec.repeatM` performs `Acc` induction on pinned measure values.
…heory
The join that pins the next measure value now occurs exactly once, inside `RepeatVariant.EvalsTo v a Ψ` ("the measure at cursor `a` evaluates to some value `ma` with `Ψ ma`"); `DecreasesTo` is defined in terms of it and no exposed lemma mentions the join. The theory follows the `ofProp_apply` scheme: general pointwise lemmas (`NondetFun.evalsTo_apply`, `RepeatVariant.evalsTo_ofMeasure_apply`) are `simp`-only because an ematch pattern cannot bind the lattice parameter under the arrow, and fixed-arity `Prop`-grounded specializations (`_apply_1` to `_apply_3`) supply the `grind` rules. With `decreasesTo_def` and the pure collapse `evalsTo_ofMeasure` both `simp` and `grind` lemmas, state-dependent measures now discharge with plain `simp at *` followed by `grind`, and the `σ`-indexed `NondetFun` instance drops to `@[instance_reducible]` like the pure one.
…esis The step postcondition of `Spec.repeatM` and `Spec.forIn_loop` is now `measure.EvalsBelow a' ma ⊓ inv (.inl a')`: the invariant sits outside the join pinning the next measure value, so the exposed statement mentions no existential and no predicate parameter. Pushing the invariant into the join during the proof uses `Lean.Order.iSup_meet_le`, frame elimination derived from `PreservesSup (meet P)`; the specs take a `[∀ P : Pred, PreservesSup (meet P)]` binder, which instance synthesis discharges for every lattice in the `Prop`-based tower. `Pred`-valued names are PascalCase uniformly: the class field `NondetFun.EvalsTo`, the structure field `RepeatVariant.EvalsTo` (pins the pre-state measure value) and `RepeatVariant.EvalsBelow` (bounds the post-state value). The collapse theory follows the `ofProp_apply` scheme with fixed-arity `Prop`-grounded `grind` rules up to five state layers (`evalsTo_apply_1` to `_5`, `evalsBelow_ofMeasure_apply_1` to `_5`); the generic `evalsBelow_ofMeasure` collapse stays out of the simp set so that `Nat`-valued measures reach `⌜f a' < ma⌝` via `evalsBelow_ofMeasure_nat` instead of a `WellFoundedRelation.rel` application.
The cursor `α`, the measure value type `γ` and the assertion lattice `Pred` of `RepeatVariant` now live in independent universes, and `NondetFun`'s function type `Fun` is freed from the lattice universe (only the state layers `σ` live there), so measures can map into codomains of any universe such as ordinals. The specs' extra universe parameters are undetermined by their conclusions; rule application leaves them as level metavariables that elaborating the invariant assigns.
The `σ`-indexed `NondetFun` instance and the pointwise lemmas `evalsTo_apply` and `evalsBelow_ofMeasure_apply` now take the state layer `σ` in a universe independent of the inner lattice, matching the generality of the pointwise `CompleteLattice` instance, so towers such as `BigState → Prop` with `BigState : Type 1` support state-dependent measures.
…string Instances carry instance reducibility by declaration, so the attribute on the two `NondetFun` instances is redundant. The module docstring opens with the concrete `Pred = Nat → Prop` example and states the reason `α` is the `outParam`: elaboration knows `Pred` from the goal and `Fun` from the type of the user-written measure, and instance resolution computes the value type.
The `total` law of `NondetFun` and `RepeatVariant` is now `(⨆ a, EvalsTo f a) = ⊤`. The distributed form `P ⊑ ⨆ a, EvalsTo f a ⊓ P` moves into `le_of_total_le`, which derives it from the law and frame elimination under a `[PreservesSup (meet P)]` hypothesis; `Spec.repeatM` discharges that hypothesis from its frame binder. The instance proofs shrink accordingly.
sgraf812
force-pushed
the
sg/vcgen-variant
branch
from
August 7, 2026 18:23
1462c6b to
9fade3e
Compare
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Aug 7, 2026
sgraf812
enabled auto-merge
August 8, 2026 10:42
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
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 generalizes the termination measures of
vcgen'swhileloop specifications. A measure may map into any type with aWellFoundedRelationinstance and may read monadic state:Decrease obligations for
Nat-valued measures have the shapef a' < maand fall togrind; other measure types reduce withRepeatVariant.evalsBelow_ofMeasureto the goalstermination_byproduces, wheredecreasing_tacticapplies.A
RepeatVariantbundles the type of measure values, its well-founded relation and the evaluation of the measure inside the assertion lattice. The step ofSpec.repeatMpins the measure valuemaof the current iteration withmeasure.EvalsTo a main its precondition and bounds the value of the next iteration withmeasure.EvalsBelow a' main its postcondition. Simp andgrindlemmas collapseEvalsToandEvalsBelowapplications ofofMeasuremeasures, following theofProp_applyscheme.