Changelog

leanprover/lean4 · · 11 commits

vcgen gets smarter; instantiateMVars sped up

Lean4 tightened vcgen spec priorities and fixes, made Hoare triples universe-polymorphic, and removed a major instantiateMVars blowup.

sgraf812 TwoFX Garmelon nomeata tydeu

instantiateMVars now caches lifted substitutions to avoid exponential blowups (nomeatae2e5e45)

Lean’s instantiateMVars got a substantial performance fix: lifted substitution values are now cached and canonicalized so repeated references don’t keep copying already-lifted expressions. This addresses an exponential time/memory blowup that could turn into OOMs in proof terms built from repeated assert/intro-style hypotheses.

Hoare Triple is now universe-polymorphic in assertions (sgraf812952e337)

Std.Internal.Do.Triple was generalized so the assertion type can live at a universe independent of the program’s value type. That makes vcgen work over broader specifications, including ones quantifying over assertion-valued predicates like σ → Prop, instead of being tied to a fixed universe setup.

vcgen spec ranking now distinguishes named, *, and unfold specs (sgraf81222ffba4, sgraf812366c0a8)

The vcgen [...] frontend now assigns call-site specs to explicit priority bands: named specs outrank *, which outrank bracketed unfold/equational specs, which in turn outrank ambient @[spec] entries. This fixes cases where an unfold spec or term-supplied spec could incorrectly lose to a lower-priority ambient spec on the same program.

vcgen fixes several recursive and deep-embedding bugs (sgraf812366c0a8, sgraf8128d96b70, sgraf812d4584ed)

vcgen now handles recursive unfold/spec interactions more reliably, avoids a panic when equation specs are used for deep-embedded program types, and internalizes hypotheses earlier in with finish. Together these fixes close off regressions where verification either failed to find the right spec, crashed, or appeared to succeed while leaving kernel-rejected metavariables behind.

dite/ite and Bool naming cleaned up across core (TwoFX7fc3135, TwoFXa2c74ef, TwoFX6c11e48)

Lean renamed and reshuffled a broad set of foundational identifiers to prefer dite/ite over dif/if spellings in names, moved a few Bool helpers into more consistent namespaces, and deprecated letFun. These are mostly API- and naming-level cleanups, but they do affect downstream code and lemma names.

Other misc changes

  • CI/build updates, including adaptation PR labels and cache reuse tweaks.
  • Small namespace/priority refactors for vcgen internals and related lemmas.
  • Test additions and adjustments for the new vcgen behaviors.
  • Minor Bool helper moves and assorted mechanical rewrites.