This PR adds an `@[mvcgen_invariant_type]` tag attribute so that users
can mark
custom types as invariant types for the `mvcgen` tactic. Goals whose
type is an
application of a tagged type are classified as invariants rather than
verification
conditions. The hard-coded check for `Std.Do.Invariant` is kept as a
fallback
until a stage0 update allows applying the attribute directly.
A follow-up PR (after a stage0 update) will apply
`@[mvcgen_invariant_type]` to
`Std.Do.Invariant` and remove the hard-coded fallback.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `cbv_simproc` system for the `cbv` tactic, mirroring
simp's `simproc` infrastructure but tailored to cbv's three-phase
pipeline (`↓` pre, `cbv_eval` eval, `↑` post). User-defined
simplification procedures are indexed by discrimination tree patterns
and dispatched during cbv normalization.
New syntax:
- `cbv_simproc [↓|↑|cbv_eval] name (pattern) := body` — define and
register a cbv simproc
- `cbv_simproc_decl name (pattern) := body` — define without registering
- `attribute [cbv_simproc [↓|↑|cbv_eval]] name` — register an existing
declaration
- `builtin_cbv_simproc` variants for the internal use
New files:
- `src/Init/CbvSimproc.lean` — syntax and macros
- `src/Lean/Meta/Tactic/Cbv/CbvSimproc.lean` — types, env extensions,
registration, dispatch
- `src/Lean/Elab/Tactic/CbvSimproc.lean` — pattern elaboration and
command elaborators
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a warning to any `def` of class type that does not also
declare an appropriate reducibility.
The warning check runs after elaboration (checking the actual
reducibility status via `getReducibilityStatus`) rather than
syntactically checking modifiers before elaboration. This is necessary
to accommodate patterns like `@[to_additive (attr :=
implicit_reducible)]` in Mathlib, where the reducibility attribute is
applied during `.afterCompilation` by another attribute, and would be
missed by a purely syntactic check.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces the `isImplicitReducible` check with `Meta.isInstance`
in the `shouldInline` function within `inlineCandidate?`.
At the base phase, we skip inlining instances tagged with
`[inline]`/`[always_inline]`/`[inline_if_reduce]` because their local
functions will be lambda lifted during the base phase. The goal is to
keep instance code compact so the lambda lifter can extract
cheap-to-inline declarations. Inlining instances prematurely expands the
code and creates extra work for the lambda lifter — producing many
additional lambda-lifted closures.
The previous check used `isImplicitReducible`, which does not capture
the original intent: some `instanceReducible` declarations are not
instances. `Meta.isInstance` correctly targets only actual type class
instances. Although `Meta.isInstance` depends on the scoped extension
state, this is safe because `shouldInline` runs during LCNF compilation
at `addDecl` time — any instance referenced in the code was resolved
during elaboration when the scope was active, and LCNF compilation
occurs before the scope changes.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR enables the module system, in cooperation with the linker, to
separate meta and non-meta code in native binaries. In particular, this
ensures tactics merely used in proofs do not make it into the final
binary. A simple example using `meta import Lean` has its binary size
reduced from 130MB to 1.7MB.
# Breaking change
`importModules (loadExts := true)` must now be preceded by
`enableInitializersExecution`. This was always the case for correct
importing but is now enforced and checked eagerly.
This PR allows for a leightweight version of dependent `match` in the
new `do` elaborator: discriminant types get abstracted over previous
discriminants. The match result type and the local context still are not
considered for abstraction. For example, if both `i : Nat` and `h : i <
len` are discrminants, then if an alternative matches `i` with `0`, we
also have `h : 0 < len`:
```lean
example {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
match i, h with
| 0, _ => pure b
| i+1, h =>
have h' : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
have : as.size - 1 < as.size := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
match (← f as[as.size - 1 - i] (Array.getElem_mem this) b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop i (Nat.le_of_lt h') b
loop as.size (Nat.le_refl _) b
```
This feature turns out to be enough to save quite a few adaptations
(6/16) during bootstrep.
This PR fixes spurious unused variable warnings for variables used in
non-atomic match discriminants in `do` notation. For example, in `match
Json.parse s >>= fromJson? with`, the variable `s` would be reported as
unused.
The root cause is that `expandNonAtomicDiscrs?` eagerly elaborates the
discriminant via `Term.elabTerm`, which creates TermInfo for variable
references. The result is then passed to `elabDoElem` for further
elaboration. When the match elaboration is postponed (e.g. because the
discriminant type contains an mvar from `fromJson?`), the result is a
postponed synthetic mvar. The `withTermInfoContext'` wrapper in
`elabDoElemFns` checks `isTacticOrPostponedHole?` on this result,
detects a postponed mvar, and replaces the info subtree with a `hole`
node — discarding all the TermInfo that was accumulated during
discriminant elaboration.
The fix applies `mkSaveInfoAnnotation` to the result, which prevents
`isTacticOrPostponedHole?` from recognizing it as a hole. This is the
same mechanism that `elabLetMVar` uses to preserve info trees when the
body is a metavariable.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes `getStuckMVar?` to detect stuck metavariables through
auxiliary parent projections created for diamond inheritance. These
coercions (e.g., `AddMonoid'.toAddZero'`) are not registered as regular
projections because they construct the parent value from individual
fields rather than extracting a single field. Previously,
`getStuckMVar?` would give up when encountering them, preventing TC
synthesis from being triggered.
- Add `AuxParentProjectionInfo` environment extension to `ProjFns.lean`
recording `numParams` and `fromClass` for these coercions
- Register the info during structure elaboration in
`mkCoercionToCopiedParent`
- Consult the new extension in `getStuckMVar?` as a fallback when
`getProjectionFnInfo?` returns `none`
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR enables `backward.whnf.reducibleClassField` for v4.29.
The support is particularly important when the user marks a class field
as `[reducible]` and
the transparency mode is `.reducible`. For example, suppose `e` is `a ≤
b` where `a b : Nat`,
and `LE.le` is marked as `[reducible]`. Simply unfolding `LE.le` would
give `instLENat.1 a b`,
which would be stuck because `instLENat` has transparency
`[instance_reducible]`. To avoid this, when we unfold
a `[reducible]` class field, we also unfold the associated projection
`instLENat.1` using
`.instances` reducibility, ultimately returning `Nat.le a b`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR is part 2 of the `implicit_reducible` refactoring (part 1:
#12567).
**Background.** When Lean checks definitional equality of function
applications
`f a₁ ... aₙ =?= f b₁ ... bₙ`, it compares arguments `aᵢ =?= bᵢ` at a
transparency level determined by the binder type. Previously, only
instance-implicit (`[C]`) arguments received a transparency bump to
`.instances`. With `backward.isDefEq.implicitBump` enabled, ALL implicit
arguments (`{x}`, `⦃x⦄`, and `[x]`) are bumped to `.instances`, so that
definitions marked `[implicit_reducible]` unfold when comparing implicit
arguments. This is important because implicit arguments often carry type
information (e.g., `P (i + 0)` vs `P i`) where the mismatch is in
non-proof positions (Sort arguments to `cast`) — proof irrelevance does
not
help here, so the relevant definitions must actually unfold.
**`[implicit_reducible]`** (renamed from `[instance_reducible]` in part
1) marks
definitions that should unfold at `TransparencyMode.instances` — between
`[reducible]` (unfolds at `.reducible` and above) and the default
`[semireducible]` (unfolds only at `.default` and above). This is the
right
level for core arithmetic operations that appear in type indices.
## Changes
- **Enable `backward.isDefEq.implicitBump` by default** and set it in
`stage0/src/stdlib_flags.h` so stage0 also compiles with it
- **Mark `Nat.add`, `Nat.mul`, `Nat.sub`, `Array.size` as
`[implicit_reducible]`**
so they unfold when comparing implicit arguments at `.instances`
transparency
- **Remove redundant unification hints** (`n + 0 =?= n`, `n - 0 =?= n`,
`n * 0 =?= 0`) that are now handled by `[implicit_reducible]`
- **Rename all remaining `[instance_reducible]` attribute usages** to
`[implicit_reducible]` across the codebase (the old name remains as an
alias)
- **Remove 28 `set_option backward.isDefEq.respectTransparency false
in`**
workarounds that are no longer needed
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes `computed_field` respect the inline attributes on the
function for computing the
field. This means we can inline the accessor for the field, allowing
quicker access.
This PR renames `instance_reducible` to `implicit_reducible` and adds a
new
`backward.isDefEq.implicitBump` option to prepare for treating all
implicit
arguments uniformly during definitional equality checking.
## Changes
**Rename `instance_reducible` → `implicit_reducible`:**
- Rename `ReducibilityStatus.instanceReducible` constructor to
`implicitReducible`
- Register new `[implicit_reducible]` attribute, keep
`[instance_reducible]` as alias
- Rename `isInstanceReducible` → `isImplicitReducible` (with deprecated
aliases)
- Update all references across src/ and tests/
The rename reflects that this reducibility level is used not just for
instances
but for any definition that needs unfolding during implicit argument
resolution
(e.g., `Nat.add`, `Array.size`).
**Add `backward.isDefEq.implicitBump` option:**
- When `true` (+ `respectTransparency`), bumps transparency to
`.instances` for
ALL implicit arguments in `isDefEqArgs`, not just instance-implicit ones
- Defaults to `false` for staging compatibility — will be flipped to
`true` after
stage0 update
- Adds `// update me!` to `stage0/src/stdlib_flags.h` to trigger CI
stage0 update
## Follow-up (after stage0 update)
- Flip `backward.isDefEq.implicitBump` default to `true`
- Fix resulting test/module failures
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ensures `isDefEq` does not increase the transparency mode to
`.default` when checking whether implicit arguments are definitionally
equal. The previous behavior was creating scalability problems in
Mathlib. That said, this is a very disruptive change. The previous
behavior can be restored using the command
```
set_option backward.isDefEq.respectTransparency false
```
This PR fixes#12245 where `grind` works on `Fin n` but fails on `Fin (n
+ 1)`.
The `outParam` argument (e.g., the `range` parameter of `ToInt`) was
included as a relevant position in the e-matching pattern. The `grind`
normalizer rewrites `↑(n + 1)` to `↑n + 1` inside the range expression,
causing the pattern to no longer match. Since `outParam` arguments are
uniquely determined by type class resolution, they can be safely
wildcarded in patterns — the same reasoning that already applies to
instance-implicit arguments.
Reproducer from the issue:
```lean
example {n : Nat} {a : Fin (n + 1)} {b : Nat} (hb : b < n + 1)
(h : (a : Nat) < b) : a < ⟨b, hb⟩ := by grind -- fails without fix
```
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
