From a1e65b32e655d8a48ece0d367b1d48f689f15cb8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2026 21:29:30 +0000 Subject: [PATCH 01/17] feat: keep `have`s above a split `match` in equation lemmas This PR makes the equation lemmas `f.eq_` keep the `have`s and `let`s of the right-hand side when they split a `match` below them, instead of inlining their values into each equation. Inlining duplicated the values, exponentially for nested `have`s, and lost the sharing of the join points that `do` notation introduces, which `vcgen +jp [f]` needs (#16122). The generated equations are otherwise the same: inlining the `have`s gives back the previous equations. `mkEqnTypes` now introduces the root `have`s as let-declarations, and commits a step only if it simplifies or splits a `match`. A `match` in the value of a `have` is reduced or split in place, and the `have` is inlined only where splitting requires it, for example when its value depends on a split variable and the `match` elaborator made it a discriminant. `saveEqn` puts the used declarations back into the right-hand side. Breaking change: after `rw [f]`, the goal can contain `have`s above a split `match`. Use `dsimp only` after `rw [f]`, or `simp only [f]` instead of `rw [f]`. Co-Authored-By: Claude Opus 5.5 --- src/Lean/Elab/PreDefinition/Eqns.lean | 497 ++++++++++++++++-- tests/elab/eqns_keep_have.lean | 521 ++++++++++++++++++- tests/elab/structuralEqns2.lean.out.expected | 10 +- tests/elab/vcgenJPs.lean | 25 + 4 files changed, 1008 insertions(+), 45 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index cd48b7d467bb..9b082f316353 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Joachim Breitner -/ module - prelude - import Lean.Elab.PreDefinition.EqnsUtils import Lean.Meta.Match.NamedPatterns import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.Split +import Lean.Meta.Tactic.SplitIf import Lean.Meta.Tactic.CasesOnStuckLHS +import Lean.Meta.LetToHave /-! This module implements the generation of equational theorems, given unfolding theorems. @@ -152,12 +152,41 @@ where runST (go e) +/-- Zeta-reduces the `let`s in the binder prefix of `∀ xs, lhs = rhs`. -/ +def zetaReduceLets (type : Expr) : MetaM Expr := do + let mut e := type + let mut subst := #[] + let mut xs := #[] + let mut lctx : LocalContext := {} + repeat + match e with + | .forallE n d b bi => + let fvarId ← mkFreshFVarId + lctx := lctx.mkLocalDecl fvarId n (d.instantiateRev subst) bi + xs := xs.push (mkFVar fvarId) + subst := subst.push (mkFVar fvarId) + e := b + | .letE _ _ v b _ => + subst := subst.push (v.instantiateRev subst) + e := b + | _ => break + return lctx.mkForall xs (e.instantiateRev subst) + +/-- +Saves the equation type for the goal `mvarId`, whose target is `lhs = rhs`, where `mkEqnTypes` +stopped splitting. The equation abstracts the local declarations that the target depends on, +including through the types and values of other declarations, and the hypotheses about them that +the split produced (see `isIrrelevant`). See `mkEqnType` for how let-declarations are handled. +-/ partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := mvarId.withContext do let target ← mvarId.getType' let fvarState := collectFVars {} target let fvarState ← (← getLCtx).foldrM (init := fvarState) fun decl fvarState => do if fvarState.fvarSet.contains decl.fvarId then - return collectFVars fvarState (← instantiateMVars decl.type) + -- We need to track `let`-declarations. `introRootLets` keeps them now. + let fvarState := collectFVars fvarState (← instantiateMVars decl.type) + let some value := decl.value? (allowNondep := true) | return fvarState + return collectFVars fvarState (← instantiateMVars value) else return fvarState let mut fvarIdSet := fvarState.fvarSet @@ -174,10 +203,72 @@ partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := mva modified := true (fvarIdSet, fvarIds) ← pushDecl fvarIdSet fvarIds decl until !modified - let type ← mkForallFVars (fvarIds.map mkFVar) target + let type ← mkEqnType fvarIds target let type ← simpEqnType type modify (·.push type) where + /-- + Returns the equation type for the goal `target`, which is `lhs = rhs`, abstracting the local + declarations `fvarIds` that the equation depends on, in context order. The let-declarations among + `fvarIds`, which `introRootLets` introduced, become `have`s (or `let`s, if dependent) of the + right-hand side: the result is `∀ xs, lhs = let ls := vs; rhs`, where the `xs` are the other + declarations. A let-declaration that `lhs` or the type of some `x` depends on is zeta-reduced + instead. + + For example, given + ``` + n : Nat + y : Nat := n + 1 + ⊢ f n = y * 2 + ``` + and `fvarIds := #[n, y]`, the result is + ``` + ∀ n, f n = + have y := n + 1 + y * 2 + ``` + If `fvarIds` also contains `h : y ≠ 0`, then `y` is zeta-reduced, and the result is + ``` + ∀ n, n + 1 ≠ 0 → f n = (n + 1) * 2 + ``` + The alternative is a `let` among the binders, `∀ n, let y := n + 1; y ≠ 0 → f n = y * 2`, but + `rw` and `simp` expect an equation lemma to be a telescope of `∀`s ending in an equation, with + the left-hand side's arguments visible to them. Zeta-reducing is rarely needed: the hypotheses of a + split are about the discriminants, which are variables of the left-hand side, not about `have`s. + -/ + mkEqnType (fvarIds : Array FVarId) (target : Expr) : MetaM Expr := do + let isLet (fvarId : FVarId) : MetaM Bool := return (← fvarId.getDecl).isLet + if (← fvarIds.allM fun x => notM (isLet x)) then + mkForallFVars (fvarIds.map mkFVar) target + else + let some (_, lhs, rhs) := target.eq? + | zetaReduceLets (← mkForallFVars (fvarIds.map mkFVar) target) + -- `outer` is closed under dependencies: it contains the lets that `lhs`, the type of a + -- non-let, or the value of an `outer` let depends on. + -- All variables in `outer` are inlined. + -- A declaration's dependencies come before it in `fvarIds`, so one reverse pass suffices. + let mut outer : FVarIdSet := {} + let mut need := collectFVars {} (← instantiateMVars lhs) + for fvarId in fvarIds.reverse do + let decl ← fvarId.getDecl + if decl.isLet then + if need.fvarSet.contains fvarId then + outer := outer.insert fvarId + need := collectFVars need (← instantiateMVars decl.value) + else + need := collectFVars need (← instantiateMVars decl.type) + let mut xs := #[] + let mut ls := #[] + for fvarId in fvarIds do + if (← isLet fvarId) && !outer.contains fvarId then + ls := ls.push (mkFVar fvarId) + else + xs := xs.push (mkFVar fvarId) + let rhs ← mkLetFVars ls rhs (generalizeNondepLet := false) + -- `intro` turns a `have` into a dependent let-declaration, so we restore the `have`s. + let rhs ← if (← getOptions).getBool `cleanup.letToHave true then letToHave rhs else pure rhs + zetaReduceLets (← mkForallFVars xs (← mkEq lhs rhs) (generalizeNondepLet := false)) + /-- We say the type/proposition is "irrelevant" if 1- It does not contain any variable in `fvarIdSet` OR @@ -194,6 +285,9 @@ where pushDecl (fvarIdSet : FVarIdSet) (fvarIds : Array FVarId) (localDecl : LocalDecl) : MetaM (FVarIdSet × Array FVarId) := do let (fvarIdSet, fvarIds) ← collectDeps fvarIdSet fvarIds (← instantiateMVars localDecl.type) + let (fvarIdSet, fvarIds) ← match localDecl.value? (allowNondep := true) with + | some value => collectDeps fvarIdSet fvarIds (← instantiateMVars value) + | none => pure (fvarIdSet, fvarIds) return (fvarIdSet.insert localDecl.fvarId, fvarIds.push localDecl.fvarId) collectDeps (fvarIdSet : FVarIdSet) (fvarIds : Array FVarId) (type : Expr) : MetaM (FVarIdSet × Array FVarId) := do @@ -206,41 +300,91 @@ where (fvarIdSet, fvarIds) ← pushDecl fvarIdSet fvarIds (← fvarId.getDecl) return (fvarIdSet, fvarIds) -/-- -Zeta reduces `let` and `have` while consuming metadata. -Returns true if progress is made. --/ -partial def expand (progress : Bool) (e : Expr) : Bool × Expr := - match e with - | Expr.letE _ _ v b _ => expand true (b.instantiate1 v) - | Expr.mdata _ b => expand true b - | e => (progress, e) +/-- Zeta-reduces the `let`s and `have`s at the root of `e`, and consumes metadata. -/ +partial def expand (e : Expr) : Expr := Id.run do + let mut e := e + let mut subst := #[] + repeat + match e with + | .letE _ _ v b _ => + subst := subst.push (v.instantiateRev subst) + e := b + | .mdata _ b => e := b + | _ => break + let r := e.instantiateRev subst + -- The substitution may expose another root `let`, as in `let y := (let z := x; t); y`. + if r.isLet || r.isMData then expand r else r -def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do - let target ← mvarId.getType' - let some (_, lhs, rhs) := target.eq? | return none - let (true, rhs') := expand false rhs | return none - return some (← mvarId.replaceTargetDefEq (← mkEq lhs rhs')) +/-- +Follows a chain of let-variables to the first value that is not one. + +`introRootLets` keeps the `let`s and `have`s of the right-hand side as let-declarations, so a +`match` discriminant may be a let-variable that stands for a variable or a constructor application. +We use this function to decide whether such a discriminant is a variable, which `match` can be +split on, or a constructor application, which `match` can be reduced on. + +For example, given +``` +x : Nat +y : Option Nat := some x +z : Option Nat := y +⊢ f x = match z with + | some n => n + | none => 0 +``` +`resolveLetVar letValue? z` is `some x`, so the `match` reduces to `x`. +-/ +partial def resolveLetVar (letValue? : FVarId → Option Expr) (e : Expr) : Expr := + if let .fvar fvarId := e then + match letValue? fvarId with + | some v => resolveLetVar letValue? v + | none => e + else + e /-- Quick filter for deciding whether to use `simpMatch?` at `mkEqnTypes`. If the result is `false`, then it is not worth trying `simpMatch`. -/ -def shouldUseSimpMatch (e : Expr) : MetaM Bool := do +def shouldUseSimpMatch (e : Expr) (letValue? : FVarId → Option Expr := fun _ => none) : MetaM Bool := do let env ← getEnv let find (root : Expr) : ExceptT Unit MetaM Unit := root.forEach fun e => do if let some info := isMatcherAppCore? env e then let args := e.getAppArgs for discr in args[info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)] do - if (← Meta.isConstructorApp discr) then + if (← Meta.isConstructorApp (resolveLetVar letValue? discr)) then throwThe Unit () return (← (find e).run) matches .error _ +/-- +Finds a `match` to split in `e`, the first one in a pre-order traversal. Returns `(m, none)` if the +`match` `m` occurs in `e`, and `(m, some x)` if it occurs in the value of the let-variable `x`. + +- `declNames`: the functions being defined, empty for a non-recursive definition. For a recursive + definition, unless `deepRecursiveSplit` is set, only a `match` with an alternative that has a + recursive call is split. +- `exceptionSet`: the `match`es to skip, because splitting them already failed. +- `letValue?`: the value of a let-variable, used to decide whether a discriminant that is a + let-variable stands for a variable (see `resolveLetVar`). A `match` is only split if one of its + discriminants is a variable. +- `letMatch?`: the `match` to split in the value of a let-variable, if any. The search treats an + occurrence of a let-variable `x` as an occurrence of its value: if `letMatch? x` is `some m`, the + search stops at `x` and returns `(m, some x)`. This finds the same `match`, in the same order, as + a search in `e` with its let-variables zeta-reduced. + + `letMatch?` memoizes this function on the let-values: `mkLetMatches` calls it on the value of + each let-declaration, in context order, passing the results for the earlier ones. `splitMatch?` + then calls it on the target with all results. This way each value is searched once, instead of + at each occurrence of its let-variable. +-/ def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e : Expr) - (declNames : Array Name) (exceptionSet : ExprSet) : Option Expr := - e.findExt? fun e => Id.run do + (declNames : Array Name) (exceptionSet : ExprSet) (letValue? : FVarId → Option Expr := fun _ => none) + (letMatch? : FVarId → Option Expr := fun _ => none) : Option (Expr × Option FVarId) := + let r? := e.findExt? fun e => Id.run do + if let .fvar fvarId := e then + return if (letMatch? fvarId).isSome then .found else .done if e.hasLooseBVars || exceptionSet.contains e then return Expr.FindStep.visit else if let some info := isMatcherAppCore? env e then @@ -249,7 +393,7 @@ def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e : Expr) let mut hasFVarDiscr := false for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do let discr := args[i]! - if discr.isFVar then + if (resolveLetVar letValue? discr).isFVar then hasFVarDiscr := true break unless hasFVarDiscr do @@ -274,40 +418,317 @@ def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e : Expr) return Expr.FindStep.done else return Expr.FindStep.visit + match r? with + | some (.fvar fvarId) => (letMatch? fvarId).map (·, some fvarId) + | some e => some (e, none) + | none => none + +/-- +Returns the value of `fvarId` if it is a let-variable in `lctx`, and `none` otherwise. Nondependent +let-declarations (`have`s) are included. Partially applied to `lctx`, it is the `letValue?` +argument of the pure functions `findMatchToSplit?` and `resolveLetVar`, which cannot access the +local context. +-/ +def letValueIn (lctx : LocalContext) (fvarId : FVarId) : Option Expr := + (lctx.find? fvarId).bind (·.value? (allowNondep := true)) + +/-- `letValueIn` for the local context of `mvarId`. -/ +def _root_.Lean.MVarId.letValueIn (mvarId : MVarId) : MetaM (FVarId → Option Expr) := + return Eqns.letValueIn (← mvarId.getDecl).lctx + +/-- The discriminants of the `match` application `e` that are let-variables according to `letValue?`. -/ +def letVarDiscrs (env : Environment) (letValue? : FVarId → Option Expr) (e : Expr) : Array FVarId := Id.run do + let some info := isMatcherAppCore? env e | return #[] + let mut fvarIds := #[] + for discr in e.getAppArgs[info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)] do + if let .fvar fvarId := discr then + if (letValue? fvarId).isSome then + fvarIds := fvarIds.push fvarId + return fvarIds + +/-- The let-declarations that the target depends on, in context order. -/ +def usedLetDecls (mvarId : MVarId) : MetaM (Array LocalDecl) := mvarId.withContext do + let lctx ← getLCtx + unless lctx.any (·.isLet) do return #[] + let used := collectFVars {} (← instantiateMVars (← mvarId.getType)) + -- A declaration precedes the ones that depend on it, so one reverse pass suffices. + let (_, decls) ← lctx.foldrM (init := (used, #[])) fun decl (used, decls) => do + let some v := decl.value? (allowNondep := true) | return (used, decls) + if used.fvarSet.contains decl.fvarId then + return (collectFVars used (← instantiateMVars v), decls.push decl) + else + return (used, decls) + return decls.reverse + +/-- +Returns the map `letMatch?` for `findMatchToSplit?`: for each let-declaration `x` in `decls` whose +value has a `match` to split, maps `x` to the first such `match`, as found by `findMatchToSplit?` +on the value. The other arguments are passed to `findMatchToSplit?`. + +`decls` must be in context order, since the search in the value of `x` uses the results for the +let-declarations before `x`: if the value of `x` mentions `y`, and the value of `y` has a `match` +to split, then `x` is mapped to that `match`. + +For example, given +``` +x : Nat +a : Nat := match x with + | 0 => 1 + | _ + 1 => 2 +c : Nat := a + a +``` +both `a` and `c` are mapped to the `match` in the value of `a`. +-/ +def mkLetMatches (deep : Bool) (env : Environment) (declNames : Array Name) (exceptionSet : ExprSet) + (letValue? : FVarId → Option Expr) (decls : Array LocalDecl) : MetaM (FVarIdMap Expr) := do + let mut letMatches : FVarIdMap Expr := {} + for decl in decls do + -- The `match` may be below `let`s at the root of the value. + let v := expand (← instantiateMVars decl.value) + if let some (e, _) := findMatchToSplit? deep env v declNames exceptionSet letValue? letMatches.get? then + letMatches := letMatches.insert decl.fvarId e + return letMatches + +/-- +Splits the `match` application `e`, which is in the value of the let-declaration `fvarId`, keeping +the declaration. A split substitutes constructors for the discriminants, and `reduceLetValues?` +then reduces `e`. If the discriminants are not all variables, or the patterns overlap, so that +reducing `e` needs the hypotheses of the split, zeta-reduces `fvarId` in the target instead, to +move `e` toward the target. +-/ +def splitLetValueMatch (mvarId : MVarId) (fvarId : FVarId) (e : Expr) : MetaM (List MVarId) := + mvarId.withContext do + let some app ← matchMatcherApp? e | throwError "unexpected `match` application{indentExpr e}" + let letValue? ← mvarId.letValueIn + let discrs := app.discrs.map (resolveLetVar letValue?) + let matchEqns ← Match.getEquationsFor app.matcherName + if discrs.all (·.isFVar) && matchEqns.splitterMatchInfo.altInfos.all (·.numOverlaps == 0) then + Split.applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params discrs + else + let target ← mvarId.getType' + return [← mvarId.replaceTargetDefEq (← zetaDeltaFVars target #[fvarId])] partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do let target ← mvarId.getType' + let letValue? ← mvarId.letValueIn + let decls ← usedLetDecls mvarId + let deep := backward.eqns.deepRecursiveSplit.get (← getOptions) + let env ← getEnv let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do - if let some e := findMatchToSplit? (backward.eqns.deepRecursiveSplit.get (← getOptions)) (← getEnv) - target declNames badCases then + let letMatches ← mkLetMatches deep env declNames badCases letValue? decls + if let some (e, fvarId?) := findMatchToSplit? deep env target declNames badCases letValue? + letMatches.get? then + -- `splitMatch` may assign `mvarId` before failing. + let saved ← saveState try - Meta.Split.splitMatch mvarId e + match fvarId? with + | some fvarId => splitLetValueMatch mvarId fvarId e + | none => Meta.Split.splitMatch mvarId e catch ex => + saved.restore trace[Elab.definition.eqns] "cannot split {e}\n{ex.toMessageData}" + -- Splitting may fail on a let-variable discriminant. We zeta-reduce these and retry. + let fvarIds := letVarDiscrs (← getEnv) letValue? e + unless fvarIds.isEmpty do + let target' ← mvarId.withContext <| zetaDeltaFVars target fvarIds + if let some mvarIds ← commitWhenSome? do + splitMatch? (← mvarId.replaceTargetDefEq target') declNames then + return some mvarIds go (badCases.insert e) else trace[Elab.definition.eqns] "did not find term to split\n{MessageData.ofGoal mvarId}" return none go {} +/-- +Returns `true` if `simpMatch?` reduces the `match` application `e` itself. This is the step that +`Split.simpMatch` applies to each `match`, but applied only to `e`, without simplifying its +subterms. +-/ +def reducesMatch (e : Expr) : MetaM Bool := do + if (← reduceRecMatcher? e).isSome then return true + let some matcherName := e.getAppFn.constName? | return false + let methods : Simp.Methods := { discharge? := (← SplitIf.mkDischarge?) } + let (step, _) ← Simp.SimpM.run (← Split.getSimpMatchContext) (methods := methods) + (k := Simp.simpMatchCore matcherName e) + return !(step matches .continue) + +/-- +Replaces each `match` discriminant that is a let-variable whose value is a constructor application +with that value, so that `simpMatch?` can reduce the `match`. Other occurrences of the +let-variable are kept. The discriminants of a `match` are only replaced if the `match` then +reduces, so that a value is not copied into a `match` that stays, as `big` below: +``` +x w : Nat +big : Option Nat := some (x * x) +y : Option Nat := some x +⊢ f x w = (match y with | some n => n | none => 0) + (match g w, big with ...) +``` +Here `y` is replaced, and `big` is not, since `g w` is not a constructor application. +-/ +def inlineCtorLetDiscrs? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do + unless (← getLCtx).any (·.isLet) do return none + let target ← mvarId.getType' + let letValue? ← mvarId.letValueIn + let env ← getEnv + let post (e : Expr) : MetaM TransformStep := do + let some info := isMatcherAppCore? env e | return .done e + let mut args := e.getAppArgs + let mut modified := false + for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do + let discr := args[i]! + unless discr.isFVar && (letValue? discr.fvarId!).isSome do continue + let v := resolveLetVar letValue? discr + if (← isConstructorApp v) then + args := args.set! i v + modified := true + unless modified do return .done e + let e' := mkAppN e.getAppFn args + if (← reducesMatch e') then + return .done e' + else + return .done e + -- `Meta.transform`, since `reducesMatch` needs a term without loose bound variables. + let target' ← Meta.transform target (post := post) + if target' == target then return none + return some (← mvarId.replaceTargetDefEq target') + +/-- Applies `inlineCtorLetDiscrs?` only if `simpMatch?` then reduces the `match`. -/ +def simpCtorLetDiscrs? (mvarId : MVarId) : MetaM (Option MVarId) := commitWhenSome? do + let some mvarId ← inlineCtorLetDiscrs? mvarId | return none + simpMatch? mvarId + +/-- +Introduces the `let`s and `have`s at the root of the right-hand side as let-declarations, so that a +`match` below them can be split while the equations keep them instead of copying their values into +each use. Also consumes metadata. +-/ +def introRootLets (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do + let target ← mvarId.getType' + let some (_, lhs, rhs) := target.eq? | return mvarId + if !rhs.isLet && !rhs.isMData then return mvarId + let mut lctx ← getLCtx + let mut fvars := #[] + let mut e := rhs + repeat + match e with + | .mdata _ b => e := b + | .letE n t v b _ => + let fvarId ← mkFreshFVarId + lctx := lctx.mkLetDecl fvarId n (t.instantiateRev fvars) (v.instantiateRev fvars) + fvars := fvars.push (mkFVar fvarId) + e := b + | _ => break + let newMVar ← mkFreshExprMVarAt lctx (← getLocalInstances) (← mkEq lhs (e.instantiateRev fvars)) .syntheticOpaque (← mvarId.getTag) + mvarId.assign (← withLCtx lctx {} (mkLetFVars fvars newMVar)) + return newMVar.mvarId! + +/-- +Reduces the `match`es with constructor discriminants in `e`, where a discriminant may also be a +let-variable whose value is a constructor application, including one bound in `e`. +-/ +def reduceCtorMatches (e : Expr) : MetaM Expr := do + let env ← getEnv + -- `usedLetOnly` drops the `let`s that only a reduced discriminant used. + Meta.transform e (usedLetOnly := true) (post := fun e => do + let some info := isMatcherAppCore? env e | return .done e + let letValue? := letValueIn (← getLCtx) + let mut args := e.getAppArgs + for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do + let discr := resolveLetVar letValue? args[i]! + if (← isConstructorApp discr) then + args := args.set! i discr + match (← reduceMatcher? (mkAppN e.getAppFn args)) with + | .reduced e => return .visit e.headBeta + | _ => return .done e) + +/-- +Reduces the `match`es with constructor discriminants in the values of the let-declarations that the +target depends on, keeping the declarations. A split creates such `match`es by substituting a +constructor for a variable in a value. + +For example, splitting `x` in +``` +x : Nat +y : Nat := match x with + | 0 => 1 + | n + 1 => n +⊢ f x = y + y +``` +produces the goal +``` +n : Nat +y : Nat := match n + 1 with + | 0 => 1 + | n + 1 => n +⊢ f (n + 1) = y + y +``` +and this function replaces the value of `y` with `n`. + +If a `match` does not reduce, as for an inaccessible pattern of an indexed family, the +let-declaration and the ones that depend on it are zeta-reduced in the target instead, so that +`simpMatch?` can reduce the `match` there. +-/ +def reduceLetValues? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do + let decls ← usedLetDecls mvarId + if decls.isEmpty then return none + let letValue? ← mvarId.letValueIn + let mut lctx ← getLCtx + let mut modified := false + -- The declarations whose values still have such a `match`, and the ones that depend on them. + let mut stuck : Array FVarId := #[] + let mut stuckSet : FVarIdSet := {} + for decl in decls do + let v ← instantiateMVars decl.value + if v.hasAnyFVar stuckSet.contains then + stuck := stuck.push decl.fvarId + stuckSet := stuckSet.insert decl.fvarId + else if (← shouldUseSimpMatch (expand v) letValue?) then + let v' ← reduceCtorMatches v + if v' != v then + lctx := lctx.modifyLocalDecl decl.fvarId (·.setValue v') + modified := true + if (← shouldUseSimpMatch (expand v') letValue?) then + stuck := stuck.push decl.fvarId + stuckSet := stuckSet.insert decl.fvarId + if !modified && stuck.isEmpty then + return none + let mut target ← mvarId.getType + -- `reduceCtorMatches` may get stuck where `simpMatch?` succeeds, as for an inaccessible pattern + -- of an indexed family, so we zeta-reduce these declarations to move the `match` to the target. + unless stuck.isEmpty do + target ← withLCtx lctx (← getLocalInstances) <| zetaDeltaFVars target stuck + let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) target .syntheticOpaque (← mvarId.getTag) + mvarId.assign mvarNew + return some mvarNew.mvarId! + +/-- +Simplifies or splits a `match` of the right-hand side, after introducing its root `let`s with +`introRootLets`. Commits only if this makes progress, so that a goal without a `match` to split +keeps its root `let`s and `have`s. +-/ +def tryStep? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := + commitWhenSome? do + let mvarId ← introRootLets mvarId + if let some mvarId ← reduceLetValues? mvarId then + return some [mvarId] + if let some mvarId ← simpCtorLetDiscrs? mvarId then + return some [mvarId] + if (← shouldUseSimpMatch (← mvarId.getType')) then + if let some mvarId ← simpMatch? mvarId then + return some [mvarId] + splitMatch? mvarId declNames + partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do let (_, eqnTypes) ← go mvarId |>.run #[] return eqnTypes where go (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := do trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}" - - -- The `let`s and `have`s at the root of the RHS are zeta-reduced only to expose a `match`. - let mvarId' := (← expandRHS? mvarId).getD mvarId - - if (← shouldUseSimpMatch (← mvarId'.getType')) then - if let some mvarId ← simpMatch? mvarId' then - return (← go mvarId) - - if let some mvarIds ← splitMatch? mvarId' declNames then - return (← mvarIds.forM go) - - saveEqn mvarId + if let some mvarIds ← tryStep? mvarId declNames then + mvarIds.forM go + else + saveEqn mvarId /-- Some of the hypotheses added by `mkEqnTypes` may not be used by the actual proof (i.e., `value` argument). diff --git a/tests/elab/eqns_keep_have.lean b/tests/elab/eqns_keep_have.lean index a317097583a4..640424eef5c6 100644 --- a/tests/elab/eqns_keep_have.lean +++ b/tests/elab/eqns_keep_have.lean @@ -1,7 +1,8 @@ /-! -Tests that equation lemmas zeta-reduce the `have`s at the root of the right-hand side only when -this exposes a `match` to split, so that `vcgen +jp [f]` sees the join points of `f` (#16122). +Tests that equation lemmas keep the `have`s at the root of the right-hand side, also above a split +`match`, so that `vcgen +jp [f]` sees the join points of `f` (#16122). -/ +set_option linter.unusedVariables false def f (x : Nat) : Nat := have y := x + 1 @@ -33,16 +34,199 @@ info: prog2.eq_1 (b : Nat → Bool) : -/ #guard_msgs in #check prog2.eq_1 --- The `have` is zeta-reduced to split the `match`. +-- The `have` stays above the split `match`, and is dropped where it is unused. def h (x : Option Nat) : Nat := have y := 1 + have z := y + 1 match x with - | some a => a + y + | some v => v + z + z | none => y -/-- info: h.eq_1 (a : Nat) : h (some a) = a + 1 -/ +/-- +info: h.eq_1 (v : Nat) : + h (some v) = + have y := 1; + have z := y + 1; + v + z + z +-/ #guard_msgs in #check h.eq_1 +/-- +info: h.eq_2 : + h none = + have y := 1; + y +-/ +#guard_msgs in #check h.eq_2 + +-- The join point of `do` stays above the split `match` and the `if`. +def rootMatch (x : Nat) (b : Bool) : StateM Nat Nat := do + let mut y := 0 + match x with + | 0 => y := 1 + | _ + 1 => if b then y := 2 else y := 3 + let s ← get + return y + s + +/-- +info: rootMatch.eq_2 (b : Bool) (n : Nat) : + rootMatch n.succ b = + have __do_jp := fun __r y => do + let s ← get + pure (y + s); + if b = true then + have y := 2; + __do_jp () y + else + have y := 3; + __do_jp () y +-/ +#guard_msgs in #check rootMatch.eq_2 + +-- Nested join points. +def seqIfs (x : Nat) (b c : Bool) : StateM Nat Nat := do + let mut y := 0 + match x with + | 0 => y := 1 + | _ + 1 => if b then y := 2 else y := 3 + if c then y := y + 1 + let s ← get + return y + s + +/-- +info: seqIfs.eq_2 (b c : Bool) (n : Nat) : + seqIfs n.succ b c = + have __do_jp := fun __r y => + have __do_jp := fun __r y => do + let s ← get + pure (y + s); + if c = true then + have y := y + 1; + __do_jp () y + else __do_jp () y; + if b = true then + have y := 2; + __do_jp () y + else + have y := 3; + __do_jp () y +-/ +#guard_msgs in #check seqIfs.eq_2 + +-- Zeta-reducing chained `have`s would be exponential. +def chain (f : Nat → Nat) (x : Option Nat) : Nat := + have p := f 0 + have q := p + p + have r := q + q + match x with + | some a => r + a + | none => 0 + +/-- +info: chain.eq_1 (f : Nat → Nat) (a : Nat) : + chain f (some a) = + have p := f 0; + have q := p + p; + have r := q + q; + r + a +-/ +#guard_msgs in #check chain.eq_1 + +-- The value of the `have` depends on the discriminant. +def dep (x : Nat) : Nat := + have y := x + 1 + match x with + | 0 => y + | n + 1 => n + y + +/-- +info: dep.eq_2 (n : Nat) : + dep n.succ = + have y := n.succ + 1; + n + y +-/ +#guard_msgs in #check dep.eq_2 + +-- A dependent `let` stays a `let`. +def depLet (x : Nat) : Fin 5 := + let n := 4 + match x with + | 0 => (⟨n, by decide⟩ : Fin (n + 1)) + | _ + 1 => 0 + +/-- +info: depLet.eq_1 : + depLet 0 = + let n := 4; + ⟨n, depLet._proof_1⟩ +-/ +#guard_msgs in #check depLet.eq_1 + +-- The `have` is zeta-reduced if it is a discriminant. +def discr (x : Nat) : Nat := + have y := x + match y with + | 0 => 1 + | n + 1 => n + +/-- info: discr.eq_2 (n : Nat) : discr n.succ = n -/ +#guard_msgs in #check discr.eq_2 + +def discr2 (x : Nat) : Nat := + have k := x + 2 + match x, k with + | 0, _ => 1 + | n + 1, m => n + m + +/-- info: discr2.eq_2 (n : Nat) : discr2 n.succ = n + (n.succ + 2) -/ +#guard_msgs in #check discr2.eq_2 + +-- The `match` in the value of the `have` is split, and the `have` is kept. +def inValue (x : Option Nat) : Nat := + have y := match x with + | some a => a + | none => 0 + y + 1 + +/-- +info: inValue.eq_1 (a : Nat) : + inValue (some a) = + have y := a; + y + 1 +-/ +#guard_msgs in #check inValue.eq_1 + +-- Structural and well-founded recursion. +def srec (f : Nat → Nat) (n : Nat) : Nat := + have v := f n + match n with + | 0 => v + v + | m + 1 => srec f m + v + v + +/-- +info: srec.eq_2 (f : Nat → Nat) (n_1 : Nat) : + srec f n_1.succ = + have v := f n_1.succ; + srec f n_1 + v + v +-/ +#guard_msgs in #check srec.eq_2 + +def wrec (f : Nat → Nat) (n : Nat) : Nat := + have v := f n + match n with + | 0 => v + v + | m + 1 => wrec f (m / 2) + v + v +termination_by n +decreasing_by grind + +/-- +info: wrec.eq_2 (f : Nat → Nat) (n_1 : Nat) : + wrec f n_1.succ = + have v := f n_1.succ; + wrec f (n_1 / 2) + v + v +-/ +#guard_msgs in #check wrec.eq_2 + -- A `have` in a `match` alternative. def k (x : Option Nat) : Nat := match x with @@ -83,3 +267,330 @@ info: w.eq_1 (n : Nat) : y + y -/ #guard_msgs in #check w.eq_1 + +-- A `have` with a constructor value is inlined as a discriminant, so the `match` reduces. +def ctorLet (x : Nat) : Nat := + have y := some x + match y with + | none => 42 + | some n => + match n with + | 0 => 0 + | m + 1 => m + +/-- info: ctorLet.eq_2 (n : Nat) : ctorLet n.succ = n -/ +#guard_msgs in #check ctorLet.eq_2 + +-- The value of the `have` has the `match` below a nested `have`. +def nestedLet (x : Nat) : Nat := + have y := + have z := x + match z with + | 0 => 42 + | n + 1 => n + y + +/-- +info: nestedLet.eq_2 (n : Nat) : + nestedLet n.succ = + have y := n; + y +-/ +#guard_msgs in #check nestedLet.eq_2 + +-- The constructor value is reached through an alias. +def ctorAlias (x : Nat) : Nat := + have y := some x + have z := y + match z with + | none => 42 + | some n => + match n with + | 0 => 0 + | m + 1 => m + +/-- info: ctorAlias.eq_2 (n : Nat) : ctorAlias n.succ = n -/ +#guard_msgs in #check ctorAlias.eq_2 + +def g (n : Nat) : Option Nat := if n = 0 then none else some n + +-- An unused `have` above a `match` that is not split is kept. +def unusedRoot (x : Nat) : Nat := + have k := x + 1 + match g x with + | some a => a + | none => 0 + +/-- +info: unusedRoot.eq_1 (x : Nat) : + unusedRoot x = + have k := x + 1; + match g x with + | some a => a + | none => 0 +-/ +#guard_msgs in #check unusedRoot.eq_1 + +-- Also inside a split branch. +def unusedBranch (x : Nat) (y : Option Nat) : Nat := + match y with + | some b => + have k := b + 1 + match g x with + | some a => a + | none => 0 + | none => 0 + +/-- +info: unusedBranch.eq_1 (x a : Nat) : + unusedBranch x (some a) = + have k := a + 1; + match g x with + | some a => a + | none => 0 +-/ +#guard_msgs in #check unusedBranch.eq_1 + +-- Splitting `x` exposes a `match` in the value of `c`, which must then be split too. The `match` +-- generalizes the `have`s, whose values depend on `x`, so they are zeta-reduced to split it. +def nestedValueCases (x : Nat) : Nat := + have a := + have b := x + 1 + match x with + | 0 => b + | n + 1 => b + (match n with | 0 => 10 | m + 1 => m) + have c := a + a + match x with + | 0 => c + | n + 1 => c + n + +/-- +info: nestedValueCases.eq_3 (n_1 : Nat) : + nestedValueCases n_1.succ.succ = + ((have b := n_1.succ.succ + 1; + b + n_1) + + have b := n_1.succ.succ + 1; + b + n_1) + + n_1.succ +-/ +#guard_msgs in #check nestedValueCases.eq_3 + +-- The target reaches the `match` in the value of `c` only through `d`. +def nestedValueChain (x : Nat) : Nat := + have a := + have b := x + 1 + match x with + | 0 => b + | n + 1 => b + (match n with | 0 => 10 | m + 1 => m) + have c := a + a + have d := c + c + match x with + | 0 => d + | n + 1 => d + n + +/-- +info: nestedValueChain.eq_3 (n_1 : Nat) : + nestedValueChain n_1.succ.succ = + ((have b := n_1.succ.succ + 1; + b + n_1) + + have b := n_1.succ.succ + 1; + b + n_1) + + ((have b := n_1.succ.succ + 1; + b + n_1) + + have b := n_1.succ.succ + 1; + b + n_1) + + n_1.succ +-/ +#guard_msgs in #check nestedValueChain.eq_3 + +-- Literal patterns overlap, so the `have` is zeta-reduced to split the `match` in its value. +def valNatLit (x : Nat) : Nat := + have y := match x with + | 5 => 1 + | 7 => 3 + | _ => 2 + y + y +/-- +info: equations: +@[backward_defeq] theorem valNatLit.eq_1 : valNatLit 5 = 1 + 1 +@[backward_defeq] theorem valNatLit.eq_2 : valNatLit 7 = 3 + 3 +theorem valNatLit.eq_3 : ∀ (x : Nat), (x = 5 → False) → (x = 7 → False) → valNatLit x = 2 + 2 +-/ +#guard_msgs in #print equations valNatLit + +-- The `match`es in the values are split in the order in which they occur in the right-hand side. +def twoVals (x z : Nat) : Nat := + have a := match x with + | 0 => 1 + | _ + 1 => 2 + have b := match z with + | 0 => a + | _ + 1 => a + 1 + b + b +/-- +info: equations: +@[backward_defeq] theorem twoVals.eq_1 : twoVals 0 0 = + have a := 1; + a + a +@[backward_defeq] theorem twoVals.eq_2 : ∀ (n : Nat), + twoVals n.succ 0 = + have a := 2; + a + a +@[backward_defeq] theorem twoVals.eq_3 : ∀ (n : Nat), + twoVals 0 n.succ = + have a := 1; + a + 1 + (a + 1) +@[backward_defeq] theorem twoVals.eq_4 : ∀ (n n_1 : Nat), + twoVals n_1.succ n.succ = + have a := 2; + a + 1 + (a + 1) +-/ +#guard_msgs in #print equations twoVals + +-- Overlapping patterns in a value. +def valOverlap (x y : Nat) : Nat := + have r := match x, y with + | 0, _ => 1 + | _, 0 => 2 + | n + 1, m + 1 => n + m + r + r +/-- +info: equations: +@[backward_defeq] theorem valOverlap.eq_1 : ∀ (y : Nat), valOverlap 0 y = 1 + 1 +theorem valOverlap.eq_2 : ∀ (x : Nat), (x = 0 → False) → valOverlap x 0 = 2 + 2 +@[backward_defeq] theorem valOverlap.eq_3 : ∀ (n m : Nat), valOverlap n.succ m.succ = n + m + (n + m) +-/ +#guard_msgs in #print equations valOverlap + +-- A `match` in a value whose discriminants are not all variables. +def valMixedDiscr (x : Nat) : Nat := + have y := match x, x + 1 with + | 0, _ => 1 + | n + 1, m => n + m + y + y +/-- +info: equations: +@[backward_defeq] theorem valMixedDiscr.eq_1 : valMixedDiscr 0 = 1 + 1 +@[backward_defeq] theorem valMixedDiscr.eq_2 : ∀ (n : Nat), valMixedDiscr n.succ = n + (n.succ + 1) + (n + (n.succ + 1)) +-/ +#guard_msgs in #print equations valMixedDiscr + +-- The same variable is matched in a value and in the right-hand side. +def valAndTarget (x : Nat) : Nat := + have y := match x with + | 0 => 1 + | _ + 1 => 2 + match x with + | 0 => y + y + | n + 1 => y + n +/-- +info: equations: +@[backward_defeq] theorem valAndTarget.eq_1 : valAndTarget 0 = 1 + 1 +@[backward_defeq] theorem valAndTarget.eq_2 : ∀ (n : Nat), valAndTarget n.succ = 2 + n +-/ +#guard_msgs in #print equations valAndTarget + +-- Structural recursion through a `match` in a value. +def listVal (xs : List Nat) : Nat := + have r := match xs with + | [] => 0 + | x :: ys => x + listVal ys + r + r +/-- +info: equations: +@[backward_defeq] theorem listVal.eq_1 : listVal [] = + have r := 0; + r + r +@[backward_defeq] theorem listVal.eq_2 : ∀ (x : Nat) (ys : List Nat), + listVal (x :: ys) = + have r := x + listVal ys; + r + r +-/ +#guard_msgs in #print equations listVal + +-- Well-founded recursion through a `match` in a value. +def wfVal (n : Nat) : Nat := + have r := match n with + | 0 => 0 + | m + 1 => wfVal (m / 2) + r + r +termination_by n +decreasing_by grind +/-- +info: equations: +@[backward_defeq] theorem wfVal.eq_1 : wfVal 0 = + have r := 0; + r + r +theorem wfVal.eq_2 : ∀ (n_1 : Nat), + wfVal n_1.succ = + have r := wfVal (n_1 / 2); + r + r +-/ +#guard_msgs in #print equations wfVal + +inductive Vec (α : Type) : Nat → Type + | nil : Vec α 0 + | cons : α → Vec α n → Vec α (n + 1) + +-- Indexed discriminants in a value: the reduction of the `match` gets stuck, so the `have` is zeta-reduced. +def vecTwo (n : Nat) (v w : Vec Nat n) : Nat := + have r := match v, w with + | .nil, .nil => 0 + | .cons a _, .cons b _ => match a with + | 0 => b + | k + 1 => k + b + r + r +/-- +info: equations: +@[backward_defeq] theorem vecTwo.eq_1 : vecTwo 0 Vec.nil Vec.nil = + have r := 0; + r + r +@[backward_defeq] theorem vecTwo.eq_2 : ∀ (n_2 : Nat) (a_1 : Vec Nat n_2) (b : Nat) (a_2 : Vec Nat n_2), + vecTwo (n_2 + 1) (Vec.cons 0 a_1) (Vec.cons b a_2) = b + b +@[backward_defeq] theorem vecTwo.eq_3 : ∀ (n_2 : Nat) (a_1 : Vec Nat n_2) (b : Nat) (a_2 : Vec Nat n_2) (n : Nat), + vecTwo (n_2 + 1) (Vec.cons n.succ a_1) (Vec.cons b a_2) = n + b + (n + b) +-/ +#guard_msgs in #print equations vecTwo + +-- `y` is inlined as a discriminant, since `match y` then reduces. `big` is not, since +-- `match g w, big` does not reduce. +def ctorDiscrIrrelevant (x w : Nat) : Nat := + have big := some (x * x + x * x) + have y := some x + (match y with + | some n => n + | none => 0) + + (match g w, big with + | some a, some k => a + k + | _, _ => 0) + + (match g w, big with + | some a, some k => a - k + | _, _ => big.get!) + +/-- +info: equations: +@[backward_defeq] theorem ctorDiscrIrrelevant.eq_1 : ∀ (x w : Nat), + ctorDiscrIrrelevant x w = + have big := some (x * x + x * x); + (x + + match g w, big with + | some a, some k => a + k + | x, x_1 => 0) + + match g w, big with + | some a, some k => a - k + | x, x_1 => big.get! +-/ +#guard_msgs in #print equations ctorDiscrIrrelevant + +-- The `match` has the index `n + 1` as a discriminant, which `simpMatch?` reduces. +def ctorDiscrIndexed (n a : Nat) (v w : Vec Nat n) : Nat := + have p := Vec.cons a v + have q := Vec.cons a w + match p, q with + | .cons b _, .cons c _ => b + c + +/-- +info: equations: +@[backward_defeq] theorem ctorDiscrIndexed.eq_1 : ∀ (n a : Nat) (v w : Vec Nat n), ctorDiscrIndexed n a v w = a + a +-/ +#guard_msgs in #print equations ctorDiscrIndexed diff --git a/tests/elab/structuralEqns2.lean.out.expected b/tests/elab/structuralEqns2.lean.out.expected index df4559555524..fffeac9030d3 100644 --- a/tests/elab/structuralEqns2.lean.out.expected +++ b/tests/elab/structuralEqns2.lean.out.expected @@ -7,8 +7,14 @@ g.eq_def (i j : Nat) : match j with | Nat.zero => 1 | j.succ => g i j -h.eq_1 (i : Nat) : h i Nat.zero = 1 + 1 -h.eq_2 (i j_2 : Nat) : h i j_2.succ = h i j_2 + h i j_2 +h.eq_1 (i : Nat) : + h i Nat.zero = + have z := 1; + z + z +h.eq_2 (i j_2 : Nat) : + h i j_2.succ = + have z := h i j_2; + z + z h.eq_def (i j : Nat) : h i j = have z := diff --git a/tests/elab/vcgenJPs.lean b/tests/elab/vcgenJPs.lean index 9afd0385e794..5ddad37263df 100644 --- a/tests/elab/vcgenJPs.lean +++ b/tests/elab/vcgenJPs.lean @@ -326,3 +326,28 @@ def match_in_match (o p : Option Nat) : StateM Nat Nat := do theorem match_in_match_triple : ⦃ fun _ => True ⦄ match_in_match o p ⦃ fun r => ⌜r > 0⌝ ⦄ := by vcgen +jp [match_in_match] with finish + +-- The join point above a split `match` is kept by `root_match.eq_2` and shared by `vcgen +jp`. +def root_match (x : Nat) (b : Bool) : StateM Nat Nat := do + let mut y := 0 + match x with + | 0 => y := 1 + | _ + 1 => if b then y := 2 else y := 3 + let s ← get + return y + s + +/-- +trace: case vc1 +k : Nat +b : Bool +s✝ : Nat +x✝¹ : PUnit +x✝ s : Nat +h✝ : b = true ∧ x✝ = 2 ∧ s = s✝ ∨ ¬b = true ∧ x✝ = 3 ∧ s = s✝ +⊢ 0 < x✝ + s +-/ +#guard_msgs in +example : ⦃fun _ => True⦄ root_match (k + 1) b ⦃fun r => ⌜r > 0⌝⦄ := by + vcgen +jp [root_match] + trace_state + all_goals grind From 4d39918ecc87754c05f6e3fad78ee5381a1013e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2026 22:06:05 +0000 Subject: [PATCH 02/17] fix: drop unused root `have`s in equation lemmas Unused `have`s at the root of the right-hand side are now dropped from the equation lemmas, also when no `match` is split below them. Co-Authored-By: Claude Opus 5.5 --- src/Lean/Elab/PreDefinition/Eqns.lean | 10 +++---- tests/elab/eqns_keep_have.lean | 38 ++++++++++++++++++++++++--- 2 files changed, 39 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 9b082f316353..887cec1f2b55 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -702,14 +702,9 @@ def reduceLetValues? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withCon mvarId.assign mvarNew return some mvarNew.mvarId! -/-- -Simplifies or splits a `match` of the right-hand side, after introducing its root `let`s with -`introRootLets`. Commits only if this makes progress, so that a goal without a `match` to split -keeps its root `let`s and `have`s. --/ +/-- Simplifies or splits a `match` of the right-hand side. Commits only if this makes progress. -/ def tryStep? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do - let mvarId ← introRootLets mvarId if let some mvarId ← reduceLetValues? mvarId then return some [mvarId] if let some mvarId ← simpCtorLetDiscrs? mvarId then @@ -725,6 +720,9 @@ partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array where go (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := do trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}" + -- `saveEqn` only puts back the let-declarations that the equation uses, so the unused root + -- `let`s and `have`s are dropped. + let mvarId ← introRootLets mvarId if let some mvarIds ← tryStep? mvarId declNames then mvarIds.forM go else diff --git a/tests/elab/eqns_keep_have.lean b/tests/elab/eqns_keep_have.lean index 640424eef5c6..ceb7a1b75ae5 100644 --- a/tests/elab/eqns_keep_have.lean +++ b/tests/elab/eqns_keep_have.lean @@ -314,7 +314,7 @@ def ctorAlias (x : Nat) : Nat := def g (n : Nat) : Option Nat := if n = 0 then none else some n --- An unused `have` above a `match` that is not split is kept. +-- An unused `have` is dropped, also above a `match` that is not split. def unusedRoot (x : Nat) : Nat := have k := x + 1 match g x with @@ -324,7 +324,6 @@ def unusedRoot (x : Nat) : Nat := /-- info: unusedRoot.eq_1 (x : Nat) : unusedRoot x = - have k := x + 1; match g x with | some a => a | none => 0 @@ -344,7 +343,6 @@ def unusedBranch (x : Nat) (y : Option Nat) : Nat := /-- info: unusedBranch.eq_1 (x a : Nat) : unusedBranch x (some a) = - have k := a + 1; match g x with | some a => a | none => 0 @@ -594,3 +592,37 @@ info: equations: @[backward_defeq] theorem ctorDiscrIndexed.eq_1 : ∀ (n a : Nat) (v w : Vec Nat n), ctorDiscrIndexed n a v w = a + a -/ #guard_msgs in #print equations ctorDiscrIndexed + + +def haveNested (x y : Nat) := + have a := y + y + y + have a' := a + 1 + match x with + | 0 => + have b := a + a + b + b + | _ => + have c := a' + a' + have d := c + c + c + +/-- +info: haveNested.eq_1 (y : Nat) : + haveNested 0 y = + have a := y + y + y; + have b := a + a; + b + b +-/ +#guard_msgs in +#check haveNested.eq_1 + +/-- +info: haveNested.eq_2 (x y : Nat) (x_3 : x = 0 → False) : + haveNested x y = + have a := y + y + y; + have a' := a + 1; + have c := a' + a'; + c + c +-/ +#guard_msgs in +#check haveNested.eq_2 From 05b182509d54460c46d4e03d760474167724a5f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2026 22:24:19 +0000 Subject: [PATCH 03/17] fix: split a `match` in a `have` value in the right-hand side A `have` whose value has a `match` to split or simplify is moved back into the right-hand side, where `Split.splitMatch` and `simpMatch?` rewrite its value, also with the hypotheses of overlapping patterns. The `have` is kept instead of inlined. Co-Authored-By: Claude Opus 5.5 --- src/Lean/Elab/PreDefinition/Eqns.lean | 170 ++++++++++++-------------- tests/elab/eqns_keep_have.lean | 101 ++++++++++++--- 2 files changed, 161 insertions(+), 110 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 887cec1f2b55..30a7b600c3ac 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -469,7 +469,8 @@ on the value. The other arguments are passed to `findMatchToSplit?`. let-declarations before `x`: if the value of `x` mentions `y`, and the value of `y` has a `match` to split, then `x` is mapped to that `match`. -For example, given +Each `x` is also mapped to the let-declaration whose value has the `match`, which `splitMatch?` +moves back into the right-hand side to split it. For example, given ``` x : Nat a : Nat := match x with @@ -477,36 +478,58 @@ a : Nat := match x with | _ + 1 => 2 c : Nat := a + a ``` -both `a` and `c` are mapped to the `match` in the value of `a`. +both `a` and `c` are mapped to the `match` in the value of `a`, and to `a`. -/ def mkLetMatches (deep : Bool) (env : Environment) (declNames : Array Name) (exceptionSet : ExprSet) - (letValue? : FVarId → Option Expr) (decls : Array LocalDecl) : MetaM (FVarIdMap Expr) := do - let mut letMatches : FVarIdMap Expr := {} + (letValue? : FVarId → Option Expr) (decls : Array LocalDecl) : + MetaM (FVarIdMap (Expr × FVarId)) := do + let mut letMatches : FVarIdMap (Expr × FVarId) := {} for decl in decls do -- The `match` may be below `let`s at the root of the value. let v := expand (← instantiateMVars decl.value) - if let some (e, _) := findMatchToSplit? deep env v declNames exceptionSet letValue? letMatches.get? then - letMatches := letMatches.insert decl.fvarId e + let letMatch? := fun fvarId => (letMatches.get? fvarId).map (·.1) + if let some (e, y?) := findMatchToSplit? deep env v declNames exceptionSet letValue? letMatch? then + let owner := match y? with + | some y => (letMatches.get? y).get!.2 + | none => decl.fvarId + letMatches := letMatches.insert decl.fvarId (e, owner) return letMatches /-- -Splits the `match` application `e`, which is in the value of the let-declaration `fvarId`, keeping -the declaration. A split substitutes constructors for the discriminants, and `reduceLetValues?` -then reduces `e`. If the discriminants are not all variables, or the patterns overlap, so that -reducing `e` needs the hypotheses of the split, zeta-reduces `fvarId` in the target instead, to -move `e` toward the target. +Moves the let-declarations `fvarIds`, and the let-declarations that depend on them, from the local +context back into the right-hand side: the target `lhs = rhs` becomes `lhs = let xs := vs; rhs`. +There, `Split.splitMatch` and `simpMatch?` rewrite the values `vs`, using the hypotheses of a split. +A moved value `v` becomes `expand v`, so that a `match` below the `let`s at the root of `v` has no +loose bound variables. Returns `none` if `lhs` or a declaration that is not a let-declaration +depends on them. -/ -def splitLetValueMatch (mvarId : MVarId) (fvarId : FVarId) (e : Expr) : MetaM (List MVarId) := +def moveLetsToRHS? (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM (Option MVarId) := mvarId.withContext do - let some app ← matchMatcherApp? e | throwError "unexpected `match` application{indentExpr e}" - let letValue? ← mvarId.letValueIn - let discrs := app.discrs.map (resolveLetVar letValue?) - let matchEqns ← Match.getEquationsFor app.matcherName - if discrs.all (·.isFVar) && matchEqns.splitterMatchInfo.altInfos.all (·.numOverlaps == 0) then - Split.applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params discrs - else - let target ← mvarId.getType' - return [← mvarId.replaceTargetDefEq (← zetaDeltaFVars target #[fvarId])] + let target ← mvarId.getType' + let some (_, lhs, rhs) := target.eq? | return none + let mut lctx ← getLCtx + let mut moved : FVarIdSet := {} + let mut xs := #[] + for decl in (← getLCtx) do + let mut dep := fvarIds.contains decl.fvarId + unless dep do + dep := (← instantiateMVars decl.type).hasAnyFVar moved.contains + if let some v := decl.value? (allowNondep := true) then + dep := dep || (← instantiateMVars v).hasAnyFVar moved.contains + unless dep do continue + let some v := decl.value? (allowNondep := true) | return none + moved := moved.insert decl.fvarId + xs := xs.push (mkFVar decl.fvarId) + lctx := lctx.modifyLocalDecl decl.fvarId (·.setValue (expand (← instantiateMVars v))) + if xs.isEmpty || (← instantiateMVars lhs).hasAnyFVar moved.contains then return none + let rhs ← withLCtx lctx (← getLocalInstances) do + mkLetFVars xs rhs (generalizeNondepLet := false) + let target ← mkEq lhs rhs + let lctxNew := xs.foldr (init := lctx) fun x lctx => lctx.erase x.fvarId! + let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) target .syntheticOpaque + (← mvarId.getTag) + mvarId.assign mvarNew + return some mvarNew.mvarId! partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do let target ← mvarId.getType' @@ -517,16 +540,24 @@ partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Opti let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do let letMatches ← mkLetMatches deep env declNames badCases letValue? decls if let some (e, fvarId?) := findMatchToSplit? deep env target declNames badCases letValue? - letMatches.get? then + (fun fvarId => (letMatches.get? fvarId).map (·.1)) then -- `splitMatch` may assign `mvarId` before failing. let saved ← saveState try match fvarId? with - | some fvarId => splitLetValueMatch mvarId fvarId e + | some fvarId => + -- `e` is in the value of `owner`, which we move back into the right-hand side. + let some (_, owner) := letMatches.get? fvarId | unreachable! + let some mvarId' ← moveLetsToRHS? mvarId #[owner] + | throwError "cannot move let-declaration to the right-hand side" + Meta.Split.splitMatch mvarId' e | none => Meta.Split.splitMatch mvarId e catch ex => saved.restore trace[Elab.definition.eqns] "cannot split {e}\n{ex.toMessageData}" + if let some fvarId := fvarId? then + -- We zeta-reduce `fvarId` to move `e` toward the target. + return some [← mvarId.replaceTargetDefEq (← zetaDeltaFVars target #[fvarId])] -- Splitting may fail on a let-variable discriminant. We zeta-reduce these and retry. let fvarIds := letVarDiscrs (← getEnv) letValue? e unless fvarIds.isEmpty do @@ -624,88 +655,39 @@ def introRootLets (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do return newMVar.mvarId! /-- -Reduces the `match`es with constructor discriminants in `e`, where a discriminant may also be a -let-variable whose value is a constructor application, including one bound in `e`. --/ -def reduceCtorMatches (e : Expr) : MetaM Expr := do - let env ← getEnv - -- `usedLetOnly` drops the `let`s that only a reduced discriminant used. - Meta.transform e (usedLetOnly := true) (post := fun e => do - let some info := isMatcherAppCore? env e | return .done e - let letValue? := letValueIn (← getLCtx) - let mut args := e.getAppArgs - for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do - let discr := resolveLetVar letValue? args[i]! - if (← isConstructorApp discr) then - args := args.set! i discr - match (← reduceMatcher? (mkAppN e.getAppFn args)) with - | .reduced e => return .visit e.headBeta - | _ => return .done e) - -/-- -Reduces the `match`es with constructor discriminants in the values of the let-declarations that the -target depends on, keeping the declarations. A split creates such `match`es by substituting a -constructor for a variable in a value. - -For example, splitting `x` in -``` -x : Nat -y : Nat := match x with - | 0 => 1 - | n + 1 => n -⊢ f x = y + y -``` -produces the goal +Simplifies the `match`es with constructor discriminants in the values of the let-declarations that +the target depends on. A split creates such `match`es by substituting a constructor for a variable +in a value. The declarations are moved back into the right-hand side, where `simpMatch?` rewrites +them, as for the declaration `y` in ``` n : Nat y : Nat := match n + 1 with | 0 => 1 - | n + 1 => n + | m + 1 => m ⊢ f (n + 1) = y + y ``` -and this function replaces the value of `y` with `n`. - -If a `match` does not reduce, as for an inaccessible pattern of an indexed family, the -let-declaration and the ones that depend on it are zeta-reduced in the target instead, so that -`simpMatch?` can reduce the `match` there. +which becomes +``` +n : Nat +⊢ f (n + 1) = have y := n; y + y +``` -/ -def reduceLetValues? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do - let decls ← usedLetDecls mvarId - if decls.isEmpty then return none - let letValue? ← mvarId.letValueIn - let mut lctx ← getLCtx - let mut modified := false - -- The declarations whose values still have such a `match`, and the ones that depend on them. - let mut stuck : Array FVarId := #[] - let mut stuckSet : FVarIdSet := {} - for decl in decls do - let v ← instantiateMVars decl.value - if v.hasAnyFVar stuckSet.contains then - stuck := stuck.push decl.fvarId - stuckSet := stuckSet.insert decl.fvarId - else if (← shouldUseSimpMatch (expand v) letValue?) then - let v' ← reduceCtorMatches v - if v' != v then - lctx := lctx.modifyLocalDecl decl.fvarId (·.setValue v') - modified := true - if (← shouldUseSimpMatch (expand v') letValue?) then - stuck := stuck.push decl.fvarId - stuckSet := stuckSet.insert decl.fvarId - if !modified && stuck.isEmpty then - return none - let mut target ← mvarId.getType - -- `reduceCtorMatches` may get stuck where `simpMatch?` succeeds, as for an inaccessible pattern - -- of an indexed family, so we zeta-reduce these declarations to move the `match` to the target. - unless stuck.isEmpty do - target ← withLCtx lctx (← getLocalInstances) <| zetaDeltaFVars target stuck - let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) target .syntheticOpaque (← mvarId.getTag) - mvarId.assign mvarNew - return some mvarNew.mvarId! +def simpLetValues? (mvarId : MVarId) : MetaM (Option MVarId) := commitWhenSome? do + mvarId.withContext do + let decls ← usedLetDecls mvarId + if decls.isEmpty then return none + let letValue? ← mvarId.letValueIn + let fvarIds ← decls.filterMapM fun decl => do + let v := expand (← instantiateMVars decl.value) + return if ← shouldUseSimpMatch v letValue? then some decl.fvarId else none + if fvarIds.isEmpty then return none + let some mvarId ← moveLetsToRHS? mvarId fvarIds | return none + simpMatch? mvarId /-- Simplifies or splits a `match` of the right-hand side. Commits only if this makes progress. -/ def tryStep? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do - if let some mvarId ← reduceLetValues? mvarId then + if let some mvarId ← simpLetValues? mvarId then return some [mvarId] if let some mvarId ← simpCtorLetDiscrs? mvarId then return some [mvarId] diff --git a/tests/elab/eqns_keep_have.lean b/tests/elab/eqns_keep_have.lean index ceb7a1b75ae5..6eeff1ff33fd 100644 --- a/tests/elab/eqns_keep_have.lean +++ b/tests/elab/eqns_keep_have.lean @@ -309,6 +309,10 @@ def ctorAlias (x : Nat) : Nat := | 0 => 0 | m + 1 => m +/-- info: ctorAlias.eq_1 : ctorAlias 0 = 0 -/ +#guard_msgs in #check ctorAlias.eq_1 + + /-- info: ctorAlias.eq_2 (n : Nat) : ctorAlias n.succ = n -/ #guard_msgs in #check ctorAlias.eq_2 @@ -362,6 +366,17 @@ def nestedValueCases (x : Nat) : Nat := | 0 => c | n + 1 => c + n + +/-- +info: nestedValueCases.eq_1 : + nestedValueCases 0 = + (have b := 0 + 1; + b) + + have b := 0 + 1; + b +-/ +#guard_msgs in #check nestedValueCases.eq_1 + /-- info: nestedValueCases.eq_3 (n_1 : Nat) : nestedValueCases n_1.succ.succ = @@ -401,7 +416,7 @@ info: nestedValueChain.eq_3 (n_1 : Nat) : -/ #guard_msgs in #check nestedValueChain.eq_3 --- Literal patterns overlap, so the `have` is zeta-reduced to split the `match` in its value. +-- Literal patterns overlap: the `match` in the value is simplified with the hypotheses of the split. def valNatLit (x : Nat) : Nat := have y := match x with | 5 => 1 @@ -410,9 +425,18 @@ def valNatLit (x : Nat) : Nat := y + y /-- info: equations: -@[backward_defeq] theorem valNatLit.eq_1 : valNatLit 5 = 1 + 1 -@[backward_defeq] theorem valNatLit.eq_2 : valNatLit 7 = 3 + 3 -theorem valNatLit.eq_3 : ∀ (x : Nat), (x = 5 → False) → (x = 7 → False) → valNatLit x = 2 + 2 +@[backward_defeq] theorem valNatLit.eq_1 : valNatLit 5 = + have y := 1; + y + y +@[backward_defeq] theorem valNatLit.eq_2 : valNatLit 7 = + have y := 3; + y + y +theorem valNatLit.eq_3 : ∀ (x : Nat), + (x = 5 → False) → + (x = 7 → False) → + valNatLit x = + have y := 2; + y + y -/ #guard_msgs in #print equations valNatLit @@ -429,19 +453,23 @@ def twoVals (x z : Nat) : Nat := info: equations: @[backward_defeq] theorem twoVals.eq_1 : twoVals 0 0 = have a := 1; - a + a + have b := a; + b + b @[backward_defeq] theorem twoVals.eq_2 : ∀ (n : Nat), twoVals n.succ 0 = have a := 2; - a + a + have b := a; + b + b @[backward_defeq] theorem twoVals.eq_3 : ∀ (n : Nat), twoVals 0 n.succ = have a := 1; - a + 1 + (a + 1) + have b := a + 1; + b + b @[backward_defeq] theorem twoVals.eq_4 : ∀ (n n_1 : Nat), twoVals n_1.succ n.succ = have a := 2; - a + 1 + (a + 1) + have b := a + 1; + b + b -/ #guard_msgs in #print equations twoVals @@ -454,9 +482,19 @@ def valOverlap (x y : Nat) : Nat := r + r /-- info: equations: -@[backward_defeq] theorem valOverlap.eq_1 : ∀ (y : Nat), valOverlap 0 y = 1 + 1 -theorem valOverlap.eq_2 : ∀ (x : Nat), (x = 0 → False) → valOverlap x 0 = 2 + 2 -@[backward_defeq] theorem valOverlap.eq_3 : ∀ (n m : Nat), valOverlap n.succ m.succ = n + m + (n + m) +@[backward_defeq] theorem valOverlap.eq_1 : ∀ (y : Nat), + valOverlap 0 y = + have r := 1; + r + r +theorem valOverlap.eq_2 : ∀ (x : Nat), + (x = 0 → False) → + valOverlap x 0 = + have r := 2; + r + r +@[backward_defeq] theorem valOverlap.eq_3 : ∀ (n m : Nat), + valOverlap n.succ m.succ = + have r := n + m; + r + r -/ #guard_msgs in #print equations valOverlap @@ -468,8 +506,13 @@ def valMixedDiscr (x : Nat) : Nat := y + y /-- info: equations: -@[backward_defeq] theorem valMixedDiscr.eq_1 : valMixedDiscr 0 = 1 + 1 -@[backward_defeq] theorem valMixedDiscr.eq_2 : ∀ (n : Nat), valMixedDiscr n.succ = n + (n.succ + 1) + (n + (n.succ + 1)) +@[backward_defeq] theorem valMixedDiscr.eq_1 : valMixedDiscr 0 = + have y := 1; + y + y +@[backward_defeq] theorem valMixedDiscr.eq_2 : ∀ (n : Nat), + valMixedDiscr n.succ = + have y := n + (n.succ + 1); + y + y -/ #guard_msgs in #print equations valMixedDiscr @@ -530,7 +573,7 @@ inductive Vec (α : Type) : Nat → Type | nil : Vec α 0 | cons : α → Vec α n → Vec α (n + 1) --- Indexed discriminants in a value: the reduction of the `match` gets stuck, so the `have` is zeta-reduced. +-- Indexed discriminants in a value. def vecTwo (n : Nat) (v w : Vec Nat n) : Nat := have r := match v, w with | .nil, .nil => 0 @@ -544,9 +587,13 @@ info: equations: have r := 0; r + r @[backward_defeq] theorem vecTwo.eq_2 : ∀ (n_2 : Nat) (a_1 : Vec Nat n_2) (b : Nat) (a_2 : Vec Nat n_2), - vecTwo (n_2 + 1) (Vec.cons 0 a_1) (Vec.cons b a_2) = b + b + vecTwo (n_2 + 1) (Vec.cons 0 a_1) (Vec.cons b a_2) = + have r := b; + r + r @[backward_defeq] theorem vecTwo.eq_3 : ∀ (n_2 : Nat) (a_1 : Vec Nat n_2) (b : Nat) (a_2 : Vec Nat n_2) (n : Nat), - vecTwo (n_2 + 1) (Vec.cons n.succ a_1) (Vec.cons b a_2) = n + b + (n + b) + vecTwo (n_2 + 1) (Vec.cons n.succ a_1) (Vec.cons b a_2) = + have r := n + b; + r + r -/ #guard_msgs in #print equations vecTwo @@ -626,3 +673,25 @@ info: haveNested.eq_2 (x y : Nat) (x_3 : x = 0 → False) : -/ #guard_msgs in #check haveNested.eq_2 + +def bigHave (x : Nat) (y : Nat) : Nat := + have r := match x with + | 0 => y + y * y + y^3 + | _ => y^4 + y^5 + y + r + r + r + +/-- +info: bigHave.eq_1 (y : Nat) : + bigHave 0 y = + have r := y + y * y + y ^ 3; + r + r + r +-/ +#guard_msgs in #check bigHave.eq_1 + +/-- +info: bigHave.eq_2 (x y : Nat) (x_3 : x = 0 → False) : + bigHave x y = + have r := y ^ 4 + y ^ 5 + y; + r + r + r +-/ +#guard_msgs in #check bigHave.eq_2 From 56829eb2e9519d10700d41dc6e596525bda6bb90 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2026 22:46:59 +0000 Subject: [PATCH 04/17] fix: split other `match`es before zeta-reducing in equation lemmas When splitting a `match` fails, `splitMatch?` first tries the other `match`es, and only then zeta-reduces let-variables. This keeps the `have`s that the `match` elaborator generalizes as discriminants of an outer `match`. Co-Authored-By: Claude Opus 5.5 --- src/Lean/Elab/PreDefinition/Eqns.lean | 17 +++++++------- tests/elab/eqns_keep_have.lean | 33 +++++++++++---------------- 2 files changed, 22 insertions(+), 28 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 30a7b600c3ac..4e65bdc6c563 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -555,17 +555,18 @@ partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Opti catch ex => saved.restore trace[Elab.definition.eqns] "cannot split {e}\n{ex.toMessageData}" + -- Splitting another `match` first may make `e` splittable, as for a `match` whose + -- discriminants include let-variables that depend on a variable split by the other one. + if let some mvarIds ← go (badCases.insert e) then + return some mvarIds + -- Otherwise, we zeta-reduce, which is the last resort since it copies values. if let some fvarId := fvarId? then - -- We zeta-reduce `fvarId` to move `e` toward the target. return some [← mvarId.replaceTargetDefEq (← zetaDeltaFVars target #[fvarId])] - -- Splitting may fail on a let-variable discriminant. We zeta-reduce these and retry. let fvarIds := letVarDiscrs (← getEnv) letValue? e - unless fvarIds.isEmpty do - let target' ← mvarId.withContext <| zetaDeltaFVars target fvarIds - if let some mvarIds ← commitWhenSome? do - splitMatch? (← mvarId.replaceTargetDefEq target') declNames then - return some mvarIds - go (badCases.insert e) + if fvarIds.isEmpty then + return none + let target' ← mvarId.withContext <| zetaDeltaFVars target fvarIds + commitWhenSome? do splitMatch? (← mvarId.replaceTargetDefEq target') declNames else trace[Elab.definition.eqns] "did not find term to split\n{MessageData.ofGoal mvarId}" return none diff --git a/tests/elab/eqns_keep_have.lean b/tests/elab/eqns_keep_have.lean index 6eeff1ff33fd..382217ead397 100644 --- a/tests/elab/eqns_keep_have.lean +++ b/tests/elab/eqns_keep_have.lean @@ -353,8 +353,9 @@ info: unusedBranch.eq_1 (x a : Nat) : -/ #guard_msgs in #check unusedBranch.eq_1 --- Splitting `x` exposes a `match` in the value of `c`, which must then be split too. The `match` --- generalizes the `have`s, whose values depend on `x`, so they are zeta-reduced to split it. +-- Splitting `x` exposes a `match` in the value of `c`, which must then be split too. The outer +-- `match` generalizes the `have`s, whose values depend on `x`, so the `match x` in the value of `a` +-- is split first, and the outer `match` then reduces. def nestedValueCases (x : Nat) : Nat := have a := have b := x + 1 @@ -370,21 +371,18 @@ def nestedValueCases (x : Nat) : Nat := /-- info: nestedValueCases.eq_1 : nestedValueCases 0 = - (have b := 0 + 1; - b) + - have b := 0 + 1; - b + have a := 0 + 1; + have c := a + a; + c -/ #guard_msgs in #check nestedValueCases.eq_1 /-- info: nestedValueCases.eq_3 (n_1 : Nat) : nestedValueCases n_1.succ.succ = - ((have b := n_1.succ.succ + 1; - b + n_1) + - have b := n_1.succ.succ + 1; - b + n_1) + - n_1.succ + have a := n_1.succ.succ + 1 + n_1; + have c := a + a; + c + n_1.succ -/ #guard_msgs in #check nestedValueCases.eq_3 @@ -404,15 +402,10 @@ def nestedValueChain (x : Nat) : Nat := /-- info: nestedValueChain.eq_3 (n_1 : Nat) : nestedValueChain n_1.succ.succ = - ((have b := n_1.succ.succ + 1; - b + n_1) + - have b := n_1.succ.succ + 1; - b + n_1) + - ((have b := n_1.succ.succ + 1; - b + n_1) + - have b := n_1.succ.succ + 1; - b + n_1) + - n_1.succ + have a := n_1.succ.succ + 1 + n_1; + have c := a + a; + have d := c + c; + d + n_1.succ -/ #guard_msgs in #check nestedValueChain.eq_3 From 84ca713d8d4b9e288fbc75a5b14fd2d5942f5de9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2026 23:03:51 +0000 Subject: [PATCH 05/17] Checkpoint --- tests/elab/eqns_issues.lean | 93 +++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 tests/elab/eqns_issues.lean diff --git a/tests/elab/eqns_issues.lean b/tests/elab/eqns_issues.lean new file mode 100644 index 000000000000..5617fdce4fe4 --- /dev/null +++ b/tests/elab/eqns_issues.lean @@ -0,0 +1,93 @@ +/-! +Cases where the equation lemmas still copy values that could stay shared. The `#guard_msgs` +blocks are the expected results; they fail on the current implementation. +-/ + +-- 1. A `have` inside the value of a `have` whose `match` is split. +def innerHave (x : Nat) : Nat := + have a := + have b := x * x + x + match x with + | 0 => b + | n + 1 => b + b + n + a + a + +/-- +info: innerHave.eq_1 : + innerHave 0 = + have a := + have b := 0 * 0 + 0; + b; + a + a +-/ +#guard_msgs in #check innerHave.eq_1 + +/-- +info: innerHave.eq_2 (n : Nat) : + innerHave n.succ = + have a := + have b := n.succ * n.succ + n.succ; + b + b + n; + a + a +-/ +#guard_msgs in #check innerHave.eq_2 + +-- 2. The same, with a non-variable discriminant `x + 1`. +def mixedUnderHave (x : Nat) : Nat := + have a := + have b := x * x + match x, x + 1 with + | 0, _ => b + | n + 1, m => b + b + n + m + a + a + +/-- +info: mixedUnderHave.eq_1 : + mixedUnderHave 0 = + have a := + have b := 0 * 0; + b; + a + a +-/ +#guard_msgs in #check mixedUnderHave.eq_1 + +/-- +info: mixedUnderHave.eq_2 (n : Nat) : + mixedUnderHave n.succ = + have a := + have b := n.succ * n.succ; + b + b + n + (n.succ + 1); + a + a +-/ +#guard_msgs in #check mixedUnderHave.eq_2 + +-- 3. A `have` that is a discriminant, with a value that depends on the split variable. +def discrDep (x : Nat) : Nat := + have k := x * x + x + match x, k with + | 0, _ => 1 + | n + 1, m => n + m + m + +/-- info: discrDep.eq_1 : discrDep 0 = 1 -/ +#guard_msgs in #check discrDep.eq_1 + +/-- +info: discrDep.eq_2 (n : Nat) : + discrDep n.succ = + have k := n.succ * n.succ + n.succ; + n + k + k +-/ +#guard_msgs in #check discrDep.eq_2 + +-- 4. With `cleanup.letToHave false`, the `have` stays a `have`. +def noCleanup (x : Nat) : Nat := + have y := x + 1 + y + y + +/-- +info: noCleanup.eq_1 (x : Nat) : + noCleanup x = + have y := x + 1; + y + y +-/ +#guard_msgs in #check noCleanup.eq_1 From 2f34ed4d619ed7937bc3b9ac00f4ee304b80e18c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2026 00:37:58 +0000 Subject: [PATCH 06/17] refactor: preserve binding scopes in equation generation Keep let/have bindings in their lexical scopes while generating equations. Separate matcher case refinement from RHS normalization and construct equality proofs for scoped telescope rewrites. Isolate simplifier caches when entering local scopes. Add regression coverage for nested bindings, dependent values, computed discriminants, and normalization proofs. --- src/Lean/Elab/PreDefinition/Eqns.lean | 779 ++++++++------------ src/Lean/Meta/Match/Rewrite.lean | 4 +- src/Lean/Meta/Tactic/Split.lean | 38 +- tests/elab/1074a.lean | 7 +- tests/elab/5667.lean | 10 +- tests/elab/byteSliceIssue.lean | 2 + tests/elab/byteSliceIssue.lean.out.expected | 4 +- tests/elab/eqns_issues.lean | 256 ++++++- tests/elab/eqns_keep_have.lean | 50 +- tests/elab/eqns_telescope_proofs.lean | 94 +++ tests/elab/heapSort.lean | 6 +- tests/elab/heapSort.lean.out.expected | 20 +- tests/elab/splitList.lean.out.expected | 6 +- tests/elab/split_refine_match.lean | 69 ++ tests/elab/streamEqIssue.lean.out.expected | 12 +- tests/elab/structuralEqn6.lean | 14 +- tests/elab_bench/eqns_have_chain.lean | 69 ++ 17 files changed, 901 insertions(+), 539 deletions(-) create mode 100644 tests/elab/eqns_telescope_proofs.lean create mode 100644 tests/elab/split_refine_match.lean create mode 100644 tests/elab_bench/eqns_have_chain.lean diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 4e65bdc6c563..e8665a55a764 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -6,17 +6,18 @@ Authors: Leonardo de Moura, Joachim Breitner module prelude import Lean.Elab.PreDefinition.EqnsUtils +import Lean.Meta.HaveTelescope import Lean.Meta.Match.NamedPatterns +import Lean.Meta.Match.Rewrite import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.Split import Lean.Meta.Tactic.SplitIf import Lean.Meta.Tactic.CasesOnStuckLHS -import Lean.Meta.LetToHave /-! This module implements the generation of equational theorems, given unfolding theorems. The unfolding theorems are generated differently for different kinds of recursive definition, -but the code here is no longer cares about that. +but the code here no longer cares about that. -/ @@ -38,6 +39,10 @@ def unfoldThmType (declName : Name) : MetaM Expr := do let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body mkForallFVars xs type +/-- +Unfolds the application of `declName` on the left-hand side of an equality goal, using its +unfolding theorem when available and delta reduction otherwise. +-/ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do if let some unfoldThm ← getUnfoldEqnFor? declName (nonRec := false) then -- Recursive definition: Use unfolding lemma @@ -55,6 +60,10 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC -- Else use delta reduction deltaLHS mvarId +/-- +Proves a generated equation type for `declName`. After introducing its parameters and hypotheses, +tries reflexivity, then unfolds the definition and reduces or splits the remaining cases. +-/ partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do withTraceNode `Elab.definition.eqns (fun _ => return m!"proving:{indentExpr type}") do withNewMCtxDepth do @@ -102,6 +111,10 @@ partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do else throwError "failed to generate equational theorem for `{.ofConstName declName}`\n{MessageData.ofGoal mvarId}" +/-- +Checks whether the left-hand side of a quantified equality depends on `fvarId`. +For a non-equality conclusion, checks the entire conclusion. +-/ def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool := forallTelescope type fun _ type => do if let some (_, lhs, _) ← matchEq? type then @@ -109,9 +122,7 @@ def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool := else dependsOn type fvarId -/-- - Eliminate `namedPatterns` from equation, and trivial hypotheses. --/ +/-- Eliminates named-pattern annotations and redundant equality hypotheses from an equation type. -/ def simpEqnType (eqnType : Expr) : MetaM Expr := do forallTelescopeReducing (← instantiateMVars eqnType) fun ys type => do let proofVars := collect type @@ -152,41 +163,16 @@ where runST (go e) -/-- Zeta-reduces the `let`s in the binder prefix of `∀ xs, lhs = rhs`. -/ -def zetaReduceLets (type : Expr) : MetaM Expr := do - let mut e := type - let mut subst := #[] - let mut xs := #[] - let mut lctx : LocalContext := {} - repeat - match e with - | .forallE n d b bi => - let fvarId ← mkFreshFVarId - lctx := lctx.mkLocalDecl fvarId n (d.instantiateRev subst) bi - xs := xs.push (mkFVar fvarId) - subst := subst.push (mkFVar fvarId) - e := b - | .letE _ _ v b _ => - subst := subst.push (v.instantiateRev subst) - e := b - | _ => break - return lctx.mkForall xs (e.instantiateRev subst) - /-- -Saves the equation type for the goal `mvarId`, whose target is `lhs = rhs`, where `mkEqnTypes` -stopped splitting. The equation abstracts the local declarations that the target depends on, -including through the types and values of other declarations, and the hypotheses about them that -the split produced (see `isIrrelevant`). See `mkEqnType` for how let-declarations are handled. +Closes a terminal goal over its free variables and relevant propositional hypotheses, simplifies +the resulting equation type, and appends it to the state. RHS bindings remain inside the target. -/ partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := mvarId.withContext do let target ← mvarId.getType' let fvarState := collectFVars {} target let fvarState ← (← getLCtx).foldrM (init := fvarState) fun decl fvarState => do if fvarState.fvarSet.contains decl.fvarId then - -- We need to track `let`-declarations. `introRootLets` keeps them now. - let fvarState := collectFVars fvarState (← instantiateMVars decl.type) - let some value := decl.value? (allowNondep := true) | return fvarState - return collectFVars fvarState (← instantiateMVars value) + return collectFVars fvarState (← instantiateMVars decl.type) else return fvarState let mut fvarIdSet := fvarState.fvarSet @@ -203,77 +189,15 @@ partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := mva modified := true (fvarIdSet, fvarIds) ← pushDecl fvarIdSet fvarIds decl until !modified - let type ← mkEqnType fvarIds target + let type ← mkForallFVars (fvarIds.map mkFVar) target let type ← simpEqnType type modify (·.push type) where - /-- - Returns the equation type for the goal `target`, which is `lhs = rhs`, abstracting the local - declarations `fvarIds` that the equation depends on, in context order. The let-declarations among - `fvarIds`, which `introRootLets` introduced, become `have`s (or `let`s, if dependent) of the - right-hand side: the result is `∀ xs, lhs = let ls := vs; rhs`, where the `xs` are the other - declarations. A let-declaration that `lhs` or the type of some `x` depends on is zeta-reduced - instead. - - For example, given - ``` - n : Nat - y : Nat := n + 1 - ⊢ f n = y * 2 - ``` - and `fvarIds := #[n, y]`, the result is - ``` - ∀ n, f n = - have y := n + 1 - y * 2 - ``` - If `fvarIds` also contains `h : y ≠ 0`, then `y` is zeta-reduced, and the result is - ``` - ∀ n, n + 1 ≠ 0 → f n = (n + 1) * 2 - ``` - The alternative is a `let` among the binders, `∀ n, let y := n + 1; y ≠ 0 → f n = y * 2`, but - `rw` and `simp` expect an equation lemma to be a telescope of `∀`s ending in an equation, with - the left-hand side's arguments visible to them. Zeta-reducing is rarely needed: the hypotheses of a - split are about the discriminants, which are variables of the left-hand side, not about `have`s. - -/ - mkEqnType (fvarIds : Array FVarId) (target : Expr) : MetaM Expr := do - let isLet (fvarId : FVarId) : MetaM Bool := return (← fvarId.getDecl).isLet - if (← fvarIds.allM fun x => notM (isLet x)) then - mkForallFVars (fvarIds.map mkFVar) target - else - let some (_, lhs, rhs) := target.eq? - | zetaReduceLets (← mkForallFVars (fvarIds.map mkFVar) target) - -- `outer` is closed under dependencies: it contains the lets that `lhs`, the type of a - -- non-let, or the value of an `outer` let depends on. - -- All variables in `outer` are inlined. - -- A declaration's dependencies come before it in `fvarIds`, so one reverse pass suffices. - let mut outer : FVarIdSet := {} - let mut need := collectFVars {} (← instantiateMVars lhs) - for fvarId in fvarIds.reverse do - let decl ← fvarId.getDecl - if decl.isLet then - if need.fvarSet.contains fvarId then - outer := outer.insert fvarId - need := collectFVars need (← instantiateMVars decl.value) - else - need := collectFVars need (← instantiateMVars decl.type) - let mut xs := #[] - let mut ls := #[] - for fvarId in fvarIds do - if (← isLet fvarId) && !outer.contains fvarId then - ls := ls.push (mkFVar fvarId) - else - xs := xs.push (mkFVar fvarId) - let rhs ← mkLetFVars ls rhs (generalizeNondepLet := false) - -- `intro` turns a `have` into a dependent let-declaration, so we restore the `have`s. - let rhs ← if (← getOptions).getBool `cleanup.letToHave true then letToHave rhs else pure rhs - zetaReduceLets (← mkForallFVars xs (← mkEq lhs rhs) (generalizeNondepLet := false)) - /-- We say the type/proposition is "irrelevant" if 1- It does not contain any variable in `fvarIdSet` OR 2- It is of the form `x = t` or `t = x` where `x` is a free variable - that is not in `fvarIdSet`. This can of equality can be eliminated by substitution. -/ + that is not in `fvarIdSet`. This kind of equality can be eliminated by substitution. -/ isIrrelevant (fvarIdSet : FVarIdSet) (type : Expr) : MetaM Bool := do if Option.isNone <| type.find? fun e => e.isFVar && fvarIdSet.contains e.fvarId! then return true @@ -283,13 +207,12 @@ where else return false + /-- Adds a declaration after recursively collecting the dependencies of its type. -/ pushDecl (fvarIdSet : FVarIdSet) (fvarIds : Array FVarId) (localDecl : LocalDecl) : MetaM (FVarIdSet × Array FVarId) := do let (fvarIdSet, fvarIds) ← collectDeps fvarIdSet fvarIds (← instantiateMVars localDecl.type) - let (fvarIdSet, fvarIds) ← match localDecl.value? (allowNondep := true) with - | some value => collectDeps fvarIdSet fvarIds (← instantiateMVars value) - | none => pure (fvarIdSet, fvarIds) return (fvarIdSet.insert localDecl.fvarId, fvarIds.push localDecl.fvarId) + /-- Extends the selected declarations with the transitive type dependencies of `type`. -/ collectDeps (fvarIdSet : FVarIdSet) (fvarIds : Array FVarId) (type : Expr) : MetaM (FVarIdSet × Array FVarId) := do let s := collectFVars {} type let usedFVarIds ← sortFVarIds <| s.fvarSet.toArray @@ -300,423 +223,321 @@ where (fvarIdSet, fvarIds) ← pushDecl fvarIdSet fvarIds (← fvarId.getDecl) return (fvarIdSet, fvarIds) -/-- Zeta-reduces the `let`s and `have`s at the root of `e`, and consumes metadata. -/ -partial def expand (e : Expr) : Expr := Id.run do - let mut e := e - let mut subst := #[] - repeat - match e with - | .letE _ _ v b _ => - subst := subst.push (v.instantiateRev subst) - e := b - | .mdata _ b => e := b - | _ => break - let r := e.instantiateRev subst - -- The substitution may expose another root `let`, as in `let y := (let z := x; t); y`. - if r.isLet || r.isMData then expand r else r - - /-- -Follows a chain of let-variables to the first value that is not one. - -`introRootLets` keeps the `let`s and `have`s of the right-hand side as let-declarations, so a -`match` discriminant may be a let-variable that stands for a variable or a constructor application. -We use this function to decide whether such a discriminant is a variable, which `match` can be -split on, or a constructor application, which `match` can be reduced on. - -For example, given -``` -x : Nat -y : Option Nat := some x -z : Option Nat := y -⊢ f x = match z with - | some n => n - | none => 0 -``` -`resolveLetVar letValue? z` is `some x`, so the `match` reduces to `x`. +A matcher splitter invocation whose arguments are well-scoped in the goal's local context. +Dependencies on bindings inside the RHS are enclosed in `let`/`have` expressions in the arguments. -/ -partial def resolveLetVar (letValue? : FVarId → Option Expr) (e : Expr) : Expr := - if let .fvar fvarId := e then - match letValue? fvarId with - | some v => resolveLetVar letValue? v - | none => e - else - e +structure MatchToSplit where + declName : Name + levels : Array Level + params : Array Expr + discrs : Array Expr + deriving BEq, Hashable /-- - Quick filter for deciding whether to use `simpMatch?` at `mkEqnTypes`. - If the result is `false`, then it is not worth trying `simpMatch`. +Follows a chain of local `let`/`have` aliases until reaching an ordinary variable or a non-variable +value. Only aliases at the head are followed; subexpressions of the value remain shared. -/ -def shouldUseSimpMatch (e : Expr) (letValue? : FVarId → Option Expr := fun _ => none) : MetaM Bool := do - let env ← getEnv - let find (root : Expr) : ExceptT Unit MetaM Unit := - root.forEach fun e => do - if let some info := isMatcherAppCore? env e then - let args := e.getAppArgs - for discr in args[info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)] do - if (← Meta.isConstructorApp (resolveLetVar letValue? discr)) then - throwThe Unit () - return (← (find e).run) matches .error _ +partial def resolveLetVar (e : Expr) : MetaM Expr := do + match e.consumeMData with + | .fvar fvarId => + if let some value := (← fvarId.getDecl).value? (allowNondep := true) then + resolveLetVar value + else + return e + | _ => return e /-- -Finds a `match` to split in `e`, the first one in a pre-order traversal. Returns `(m, none)` if the -`match` `m` occurs in `e`, and `(m, some x)` if it occurs in the value of the let-variable `x`. - -- `declNames`: the functions being defined, empty for a non-recursive definition. For a recursive - definition, unless `deepRecursiveSplit` is set, only a `match` with an alternative that has a - recursive call is split. -- `exceptionSet`: the `match`es to skip, because splitting them already failed. -- `letValue?`: the value of a let-variable, used to decide whether a discriminant that is a - let-variable stands for a variable (see `resolveLetVar`). A `match` is only split if one of its - discriminants is a variable. -- `letMatch?`: the `match` to split in the value of a let-variable, if any. The search treats an - occurrence of a let-variable `x` as an occurrence of its value: if `letMatch? x` is `some m`, the - search stops at `x` and returns `(m, some x)`. This finds the same `match`, in the same order, as - a search in `e` with its let-variables zeta-reduced. - - `letMatch?` memoizes this function on the let-values: `mkLetMatches` calls it on the value of - each let-declaration, in context order, passing the results for the earlier ones. `splitMatch?` - then calls it on the target with all results. This way each value is searched once, instead of - at each occurrence of its let-variable. +Finds the first eligible matcher in `rhs` whose splitter invocation is not in `exceptions`. +At least one discriminant must resolve to a variable in the goal's local context. Enclosing RHS +bindings are closed over the splitter arguments; captures of enclosing lambda or alternative +parameters make a matcher ineligible. + +Binding values are searched before their bodies. For recursive definitions, unless deep splitting +is enabled, a candidate must have an alternative with a recursive call depending on its binders. -/ -def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e : Expr) - (declNames : Array Name) (exceptionSet : ExprSet) (letValue? : FVarId → Option Expr := fun _ => none) - (letMatch? : FVarId → Option Expr := fun _ => none) : Option (Expr × Option FVarId) := - let r? := e.findExt? fun e => Id.run do - if let .fvar fvarId := e then - return if (letMatch? fvarId).isSome then .found else .done - if e.hasLooseBVars || exceptionSet.contains e then - return Expr.FindStep.visit - else if let some info := isMatcherAppCore? env e then - let args := e.getAppArgs - -- If none of the discriminants is a free variable, then it is not worth splitting the match - let mut hasFVarDiscr := false - for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do - let discr := args[i]! - if (resolveLetVar letValue? discr).isFVar then - hasFVarDiscr := true - break - unless hasFVarDiscr do - return Expr.FindStep.visit - -- For non-recursive functions (`declNames` empty), we split here - if declNames.isEmpty then - return Expr.FindStep.found - -- For recursive functions, the “new” behavior is to likewise split - if deepRecursiveSplit then - return Expr.FindStep.found - -- Else, the “old” behavior is split only when at least one alternative contains a `declNames` - -- application with loose bound variables. - for i in info.getFirstAltPos...(info.getFirstAltPos + info.numAlts) do - let alt := args[i]! - if Option.isSome <| alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars then - return Expr.FindStep.found - return Expr.FindStep.visit - else - let Expr.const declName .. := e.getAppFn | return Expr.FindStep.visit - if declName == ``WellFounded.fix || isBRecOnRecursor env declName then - -- We should not go inside unfolded nested recursive applications - return Expr.FindStep.done - else - return Expr.FindStep.visit - match r? with - | some (.fvar fvarId) => (letMatch? fvarId).map (·, some fvarId) - | some e => some (e, none) - | none => none +partial def findMatchToSplit? (rhs : Expr) (declNames : Array Name) + (exceptions : Std.HashSet MatchToSplit) : MetaM (Option MatchToSplit) := do + let outer ← getLCtx + let deep := backward.eqns.deepRecursiveSplit.get (← getOptions) + visit outer deep #[] rhs +where + visit (outer : LocalContext) (deep : Bool) (lets : Array Expr) (e : Expr) : + MetaM (Option MatchToSplit) := do + checkSystem "findMatchToSplit" + if let some app ← matchMatcherApp? e then + let eligible := declNames.isEmpty || deep || app.alts.any fun alt => + (alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars).isSome + if eligible then + let hasVar ← app.discrs.anyM fun discr => do + let discr ← resolveLetVar discr + return discr.isFVar && outer.contains discr.fvarId! + if hasVar then + let closed ← mkLetFVars lets e (generalizeNondepLet := false) + -- Captures of enclosing lambdas and match alternatives prevent a split. + if !closed.hasAnyFVar (fun x => !outer.contains x) then + let params ← app.params.mapM fun e => mkLetFVars lets e (generalizeNondepLet := false) + let discrs ← app.discrs.mapM fun e => do + let resolved ← resolveLetVar e + mkLetFVars lets resolved (generalizeNondepLet := false) + unless (params ++ discrs).any (fun e => e.hasAnyFVar fun x => !outer.contains x) do + let candidate := { declName := app.matcherName, levels := app.matcherLevels, params, discrs } + unless exceptions.contains candidate do return some candidate + if let .const name _ := e.getAppFn then + if name == ``WellFounded.fix || isBRecOnRecursor (← getEnv) name then + return none + match e with + | .letE .. => + letTelescope e fun xs body => do + let mut lets := lets + for x in xs do + if let some candidate ← visit outer deep lets ((← x.fvarId!.getDecl).value (allowNondep := true)) then + return some candidate + lets := lets.push x + visit outer deep lets body + | .lam n t b bi | .forallE n t b bi => + withLocalDecl n bi t fun x => visit outer deep lets (b.instantiate1 x) + | .app .. => + if !e.getAppFn.isConst then + if let some candidate ← visit outer deep lets e.getAppFn then return some candidate + for arg in e.getAppArgs do + if let some candidate ← visit outer deep lets arg then return some candidate + return none + | .mdata _ b | .proj _ _ b => visit outer deep lets b + | _ => return none /-- -Returns the value of `fvarId` if it is a let-variable in `lctx`, and `none` otherwise. Nondependent -let-declarations (`have`s) are included. Partially applied to `lctx`, it is the `letValue?` -argument of the pure functions `findMatchToSplit?` and `resolveLetVar`, which cannot access the -local context. +Result of simplifying a telescope suffix. All fields use loose bound variables for the preceding +bindings. `proof?`, when present, proves equality from the original suffix to `expr`; otherwise +the change is definitional. `type` is the type of the suffix in that prefix context. -/ -def letValueIn (lctx : LocalContext) (fvarId : FVarId) : Option Expr := - (lctx.find? fvarId).bind (·.value? (allowNondep := true)) - -/-- `letValueIn` for the local context of `mvarId`. -/ -def _root_.Lean.MVarId.letValueIn (mvarId : MVarId) : MetaM (FVarId → Option Expr) := - return Eqns.letValueIn (← mvarId.getDecl).lctx - -/-- The discriminants of the `match` application `e` that are let-variables according to `letValue?`. -/ -def letVarDiscrs (env : Environment) (letValue? : FVarId → Option Expr) (e : Expr) : Array FVarId := Id.run do - let some info := isMatcherAppCore? env e | return #[] - let mut fvarIds := #[] - for discr in e.getAppArgs[info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)] do - if let .fvar fvarId := discr then - if (letValue? fvarId).isSome then - fvarIds := fvarIds.push fvarId - return fvarIds - -/-- The let-declarations that the target depends on, in context order. -/ -def usedLetDecls (mvarId : MVarId) : MetaM (Array LocalDecl) := mvarId.withContext do - let lctx ← getLCtx - unless lctx.any (·.isLet) do return #[] - let used := collectFVars {} (← instantiateMVars (← mvarId.getType)) - -- A declaration precedes the ones that depend on it, so one reverse pass suffices. - let (_, decls) ← lctx.foldrM (init := (used, #[])) fun decl (used, decls) => do - let some v := decl.value? (allowNondep := true) | return (used, decls) - if used.fvarSet.contains decl.fvarId then - return (collectFVars used (← instantiateMVars v), decls.push decl) - else - return (used, decls) - return decls.reverse +structure EqnTelescopeResult where + expr : Expr + type : Expr + proof? : Option Expr := none /-- -Returns the map `letMatch?` for `findMatchToSplit?`: for each let-declaration `x` in `decls` whose -value has a `match` to split, maps `x` to the first such `match`, as found by `findMatchToSplit?` -on the value. The other arguments are passed to `findMatchToSplit?`. - -`decls` must be in context order, since the search in the value of `x` uses the results for the -let-declarations before `x`: if the value of `x` mentions `y`, and the value of `y` has a `match` -to split, then `x` is mapped to that `match`. - -Each `x` is also mapped to the let-declaration whose value has the `match`, which `splitMatch?` -moves back into the right-hand side to split it. For example, given -``` -x : Nat -a : Nat := match x with - | 0 => 1 - | _ + 1 => 2 -c : Nat := a + a -``` -both `a` and `c` are mapped to the `match` in the value of `a`, and to `a`. +Simplifies the suffix `e` beginning at binding `i` of the telescope described by `info`. +The preceding bindings are represented by free variables in `xs` and the cached expressions in +`info`, but by loose bound variables in `e` and the result. Abstraction is batched so that closing +each binder does not repeatedly traverse the entire remaining body and proof. + +Unused values are skipped. Fixed values admit only `dsimp`; other values admit propositional +rewrites. Each updated value is entered as a dependent local definition so that matcher reduction +can use its value while simplifying the remainder. The simplifier cache is isolated for that +scope, and the rebuilt expression retains the original `let`/`have` flags. + +A value rewrite is lifted with `congrArg (fun x => originalBody)`. The body proof is closed with +`let x := updatedValue`, since it may rely on that value; the two proofs compose by transitivity. +For a nonfixed binding the result type cannot depend on `x`, so its bound-variable slot is removed. +For a fixed binding the result type is closed with the binding itself. -/ -def mkLetMatches (deep : Bool) (env : Environment) (declNames : Array Name) (exceptionSet : ExprSet) - (letValue? : FVarId → Option Expr) (decls : Array LocalDecl) : - MetaM (FVarIdMap (Expr × FVarId)) := do - let mut letMatches : FVarIdMap (Expr × FVarId) := {} - for decl in decls do - -- The `match` may be below `let`s at the root of the value. - let v := expand (← instantiateMVars decl.value) - let letMatch? := fun fvarId => (letMatches.get? fvarId).map (·.1) - if let some (e, y?) := findMatchToSplit? deep env v declNames exceptionSet letValue? letMatch? then - let owner := match y? with - | some y => (letMatches.get? y).get!.2 - | none => decl.fvarId - letMatches := letMatches.insert decl.fvarId (e, owner) - return letMatches +partial def simpEqnTelescope (info : HaveTelescopeInfo) (fixed used : Array Bool) + (e : Expr) (i : Nat) (xs : Array Expr) : Simp.SimpM EqnTelescopeResult := do + if h : i < info.haveInfo.size then + let hi := info.haveInfo[i] + let .letE n t v b nondep := e | unreachable! + let x := hi.decl.toExpr + let val := hi.decl.value (allowNondep := true) + let rv ← if !used[i]! then pure { expr := val : Simp.Result } + else if fixed[i]! then pure { expr := ← Simp.dsimp val : Simp.Result } + else Simp.simp val + let v' := if rv.expr == val then v else rv.expr.abstract xs + let hv? := rv.proof?.map (·.abstract xs) + let decl := (hi.decl.setValue rv.expr).setNondep false + let rb ← withExistingLocalDecls [decl] <| Simp.withNewLemmas #[x] do + simpEqnTelescope info fixed used b (i + 1) (xs.push x) + let type := if fixed[i]! then mkLet n t v' rb.type false + else rb.type.lowerLooseBVars 1 1 + let expr := mkLet n t v' rb.expr nondep + let hb? := rb.proof?.map fun h => mkLet n t v' h false + let hv? := hv?.map fun h => mkApp6 (mkConst ``congrArg [hi.level, info.level]) + t type v v' (mkLambda n .default t b) h + let proof? := match hv?, hb? with + | none, hb? => hb? + | hv?, none => hv? + | some hv, some hb => some <| mkEqTransCore info.level type e + (mkLet n t v' b nondep) expr hv hb + return { expr, type, proof? } + else + let rb ← Simp.simp info.body + return { + expr := rb.expr.abstract xs + type := info.bodyType.abstract xs + proof? := rb.proof?.map (·.abstract xs) + } /-- -Moves the let-declarations `fvarIds`, and the let-declarations that depend on them, from the local -context back into the right-hand side: the target `lhs = rhs` becomes `lhs = let xs := vs; rhs`. -There, `Split.splitMatch` and `simpMatch?` rewrite the values `vs`, using the hypotheses of a split. -A moved value `v` becomes `expand v`, so that a `match` below the `let`s at the root of `v` has no -loose bound variables. Returns `none` if `lhs` or a declaration that is not a let-declaration -depends on them. +Opens a leading telescope of mixed `let`/`have` bindings once and records its declarations, +instantiated body, and dependencies between bindings. + +`computeFixedUsed false` then computes two dependency closures: `used` starts from the body; +`fixed` starts from its result type and every dependent `let`. A dependent let's body may rely on +its value to typecheck even when the result type does not mention it, so that value and its +dependencies must be restricted to definitional simplification. -/ -def moveLetsToRHS? (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM (Option MVarId) := - mvarId.withContext do - let target ← mvarId.getType' - let some (_, lhs, rhs) := target.eq? | return none - let mut lctx ← getLCtx - let mut moved : FVarIdSet := {} - let mut xs := #[] - for decl in (← getLCtx) do - let mut dep := fvarIds.contains decl.fvarId - unless dep do - dep := (← instantiateMVars decl.type).hasAnyFVar moved.contains - if let some v := decl.value? (allowNondep := true) then - dep := dep || (← instantiateMVars v).hasAnyFVar moved.contains - unless dep do continue - let some v := decl.value? (allowNondep := true) | return none - moved := moved.insert decl.fvarId - xs := xs.push (mkFVar decl.fvarId) - lctx := lctx.modifyLocalDecl decl.fvarId (·.setValue (expand (← instantiateMVars v))) - if xs.isEmpty || (← instantiateMVars lhs).hasAnyFVar moved.contains then return none - let rhs ← withLCtx lctx (← getLocalInstances) do - mkLetFVars xs rhs (generalizeNondepLet := false) - let target ← mkEq lhs rhs - let lctxNew := xs.foldr (init := lctx) fun x lctx => lctx.erase x.fvarId! - let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) target .syntheticOpaque - (← mvarId.getTag) - mvarId.assign mvarNew - return some mvarNew.mvarId! - -partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do - let target ← mvarId.getType' - let letValue? ← mvarId.letValueIn - let decls ← usedLetDecls mvarId - let deep := backward.eqns.deepRecursiveSplit.get (← getOptions) - let env ← getEnv - let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do - let letMatches ← mkLetMatches deep env declNames badCases letValue? decls - if let some (e, fvarId?) := findMatchToSplit? deep env target declNames badCases letValue? - (fun fvarId => (letMatches.get? fvarId).map (·.1)) then - -- `splitMatch` may assign `mvarId` before failing. - let saved ← saveState - try - match fvarId? with - | some fvarId => - -- `e` is in the value of `owner`, which we move back into the right-hand side. - let some (_, owner) := letMatches.get? fvarId | unreachable! - let some mvarId' ← moveLetsToRHS? mvarId #[owner] - | throwError "cannot move let-declaration to the right-hand side" - Meta.Split.splitMatch mvarId' e - | none => Meta.Split.splitMatch mvarId e - catch ex => - saved.restore - trace[Elab.definition.eqns] "cannot split {e}\n{ex.toMessageData}" - -- Splitting another `match` first may make `e` splittable, as for a `match` whose - -- discriminants include let-variables that depend on a variable split by the other one. - if let some mvarIds ← go (badCases.insert e) then - return some mvarIds - -- Otherwise, we zeta-reduce, which is the last resort since it copies values. - if let some fvarId := fvarId? then - return some [← mvarId.replaceTargetDefEq (← zetaDeltaFVars target #[fvarId])] - let fvarIds := letVarDiscrs (← getEnv) letValue? e - if fvarIds.isEmpty then - return none - let target' ← mvarId.withContext <| zetaDeltaFVars target fvarIds - commitWhenSome? do splitMatch? (← mvarId.replaceTargetDefEq target') declNames - else - trace[Elab.definition.eqns] "did not find term to split\n{MessageData.ofGoal mvarId}" - return none - go {} +def getEqnTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo := do + letTelescope e fun xs body => do + let mut indices : Std.HashMap FVarId Nat := {} + for i in *...xs.size do + indices := indices.insert xs[i]!.fvarId! i + let getDeps (e : Expr) : Std.HashSet Nat := + (collectFVars {} e).fvarIds.foldl (init := {}) fun deps id => + match indices[id]? with + | none => deps + | some i => deps.insert i + let bodyType ← inferType body + let mut info : HaveTelescopeInfo := { + body, bodyType + level := ← getLevel bodyType + bodyDeps := getDeps body + bodyTypeDeps := getDeps bodyType + } + for i in *...xs.size do + let decl ← xs[i]!.fvarId!.getDecl + let hi : HaveInfo := { + decl + level := ← getLevel decl.type + typeBackDeps := getDeps decl.type + valueBackDeps := getDeps (decl.value (allowNondep := true)) + } + info := { info with haveInfo := info.haveInfo.push hi } + unless decl.isNondep do + info := { info with bodyTypeDeps := info.bodyTypeDeps.insert i } + return info /-- -Returns `true` if `simpMatch?` reduces the `match` application `e` itself. This is the step that -`Split.simpMatch` applies to each `match`, but applied only to `e`, without simplifying its -subterms. +The `simp` callback for equation normalization. It handles complete binding telescopes before the +default traversal, using `simpEqnTelescope` to preserve their nesting and sharing. Unused bindings +are removed afterward. A changed telescope is revisited: removing dependent uses can make a +previously fixed value eligible for propositional rewriting. A stable telescope returns `.done`. + +For a matcher, first try definitional reduction, then its congruence equations using local +hypotheses to discharge branch conditions. Other expressions use the default traversal. +Since matcher rewriting can use hypotheses introduced under binders, callers with +`contextual := false` must set `wellBehavedDischarge := false` to isolate cached results by scope. -/ -def reducesMatch (e : Expr) : MetaM Bool := do - if (← reduceRecMatcher? e).isSome then return true - let some matcherName := e.getAppFn.constName? | return false - let methods : Simp.Methods := { discharge? := (← SplitIf.mkDischarge?) } - let (step, _) ← Simp.SimpM.run (← Split.getSimpMatchContext) (methods := methods) - (k := Simp.simpMatchCore matcherName e) - return !(step matches .continue) +partial def simpEqn : Simp.Simproc := fun e => do + if e.isLet then + let info ← getEqnTelescopeInfo e + let (fixed, used) ← info.computeFixedUsed false + let r ← simpEqnTelescope info fixed used e 0 #[] + let r := { expr := ← zetaUnused r.expr, proof? := r.proof? : Simp.Result } + return if r.expr == e then .done r else .visit r + if let some app ← matchMatcherApp? e then + if let some e' ← reduceRecMatcher? e then + return .visit { expr := e' } + for i in *...app.numAlts do + let r ← rwMatcher i e + if r.expr != e then return .visit r + return .continue /-- -Replaces each `match` discriminant that is a let-variable whose value is a constructor application -with that value, so that `simpMatch?` can reduce the `match`. Other occurrences of the -let-variable are kept. The discriminants of a `match` are only replaced if the `match` then -reduces, so that a value is not copied into a `match` that stays, as `big` below: -``` -x w : Nat -big : Option Nat := some (x * x) -y : Option Nat := some x -⊢ f x w = (match y with | some n => n | none => 0) + (match g w, big with ...) -``` -Here `y` is replaced, and `big` is not, since `g w` is not a constructor application. +The definitional counterpart of `simpEqn`, used for fixed binding values and dependent arguments +that `simp` cannot rewrite propositionally. It opens a whole binding telescope, skips unused +values, and definitionally simplifies the other values and body with preceding values available +as local definitions. Rebuilding preserves binding flags and removes unused bindings. + +Matchers are reduced only definitionally; no congruence-equation proofs are used. Changed results +are revisited, and the returned expression is definitionally equal to the input. -/ -def inlineCtorLetDiscrs? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do - unless (← getLCtx).any (·.isLet) do return none - let target ← mvarId.getType' - let letValue? ← mvarId.letValueIn - let env ← getEnv - let post (e : Expr) : MetaM TransformStep := do - let some info := isMatcherAppCore? env e | return .done e - let mut args := e.getAppArgs - let mut modified := false - for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do - let discr := args[i]! - unless discr.isFVar && (letValue? discr.fvarId!).isSome do continue - let v := resolveLetVar letValue? discr - if (← isConstructorApp v) then - args := args.set! i v - modified := true - unless modified do return .done e - let e' := mkAppN e.getAppFn args - if (← reducesMatch e') then - return .done e' +partial def dsimpEqn : Simp.DSimproc := fun e => do + if e.isLet then + let info ← getEqnTelescopeInfo e + let (_, used) ← info.computeFixedUsed false + let r ← Simp.withFreshCache <| visit info used e 0 #[] + let r ← zetaUnused r + return if r == e then .done r else .visit r + if ← isMatcherApp e then + if let some e' ← reduceRecMatcher? e then return .visit e' + return .continue +where + visit (info : HaveTelescopeInfo) (used : Array Bool) (e : Expr) (i : Nat) + (xs : Array Expr) : Simp.SimpM Expr := do + if h : i < info.haveInfo.size then + let decl := info.haveInfo[i].decl + let .letE n t v b nondep := e | unreachable! + let value := decl.value (allowNondep := true) + let value' ← if used[i]! then Simp.dsimp value else pure value + let v' := if value' == value then v else value'.abstract xs + let decl := (decl.setValue value').setNondep false + let b ← withExistingLocalDecls [decl] <| visit info used b (i+1) (xs.push decl.toExpr) + return mkLet n t v' b nondep else - return .done e - -- `Meta.transform`, since `reducesMatch` needs a term without loose bound variables. - let target' ← Meta.transform target (post := post) - if target' == target then return none - return some (← mvarId.replaceTargetDefEq target') - -/-- Applies `inlineCtorLetDiscrs?` only if `simpMatch?` then reduces the `match`. -/ -def simpCtorLetDiscrs? (mvarId : MVarId) : MetaM (Option MVarId) := commitWhenSome? do - let some mvarId ← inlineCtorLetDiscrs? mvarId | return none - simpMatch? mvarId + return (← Simp.dsimp info.body).abstract xs /-- -Introduces the `let`s and `have`s at the root of the right-hand side as let-declarations, so that a -`match` below them can be split while the equations keep them instead of copying their values into -each use. Also consumes metadata. +Normalizes the RHS of an equality goal using `simpEqn` and `dsimpEqn`, preserving shared bindings. +The neutral configuration disables general reductions, including zeta expansion, while `simp` +provides traversal and congruence. Propositional RHS rewrites are lifted to the whole target; +definitional rewrites directly replace the target. +Returns the original goal when unchanged, which lets `splitMatch?` detect normalization progress. -/ -def introRootLets (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do +def normalizeEqn (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do let target ← mvarId.getType' let some (_, lhs, rhs) := target.eq? | return mvarId - if !rhs.isLet && !rhs.isMData then return mvarId - let mut lctx ← getLCtx - let mut fvars := #[] - let mut e := rhs - repeat - match e with - | .mdata _ b => e := b - | .letE n t v b _ => - let fvarId ← mkFreshFVarId - lctx := lctx.mkLetDecl fvarId n (t.instantiateRev fvars) (v.instantiateRev fvars) - fvars := fvars.push (mkFVar fvarId) - e := b - | _ => break - let newMVar ← mkFreshExprMVarAt lctx (← getLocalInstances) (← mkEq lhs (e.instantiateRev fvars)) .syntheticOpaque (← mvarId.getTag) - mvarId.assign (← withLCtx lctx {} (mkLetFVars fvars newMVar)) - return newMVar.mvarId! + let ctx ← Simp.mkContext (config := { Simp.neutralConfig with dsimp := true, etaStruct := .none }) + let methods : Simp.Methods := { + pre := simpEqn + dpre := dsimpEqn + discharge? := ← SplitIf.mkDischarge? + -- Matcher rewrites can use hypotheses introduced while descending under binders. + wellBehavedDischarge := false + } + let (r, _) ← Simp.main rhs ctx (methods := methods) + if r.expr == rhs then return mvarId + let target' ← mkEq lhs r.expr + if let some proof := r.proof? then + let eq := target.appFn! + return ← mvarId.replaceTargetEq target' (← mkCongrArg eq proof) + else + mvarId.replaceTargetDefEq target' /-- -Simplifies the `match`es with constructor discriminants in the values of the let-declarations that -the target depends on. A split creates such `match`es by substituting a constructor for a variable -in a value. The declarations are moved back into the right-hand side, where `simpMatch?` rewrites -them, as for the declaration `y` in -``` -n : Nat -y : Nat := match n + 1 with - | 0 => 1 - | m + 1 => m -⊢ f (n + 1) = y + y -``` -which becomes -``` -n : Nat -⊢ f (n + 1) = have y := n; y + y -``` +Tries eligible RHS matchers until a splitter produces branches whose RHSs all change under +normalization. Each attempt saves the metavariable state; failure restores it and excludes that +splitter invocation from further attempts. Returned branches are already normalized. -/ -def simpLetValues? (mvarId : MVarId) : MetaM (Option MVarId) := commitWhenSome? do - mvarId.withContext do - let decls ← usedLetDecls mvarId - if decls.isEmpty then return none - let letValue? ← mvarId.letValueIn - let fvarIds ← decls.filterMapM fun decl => do - let v := expand (← instantiateMVars decl.value) - return if ← shouldUseSimpMatch v letValue? then some decl.fvarId else none - if fvarIds.isEmpty then return none - let some mvarId ← moveLetsToRHS? mvarId fvarIds | return none - simpMatch? mvarId - -/-- Simplifies or splits a `match` of the right-hand side. Commits only if this makes progress. -/ -def tryStep? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := - commitWhenSome? do - if let some mvarId ← simpLetValues? mvarId then - return some [mvarId] - if let some mvarId ← simpCtorLetDiscrs? mvarId then - return some [mvarId] - if (← shouldUseSimpMatch (← mvarId.getType')) then - if let some mvarId ← simpMatch? mvarId then - return some [mvarId] - splitMatch? mvarId declNames +partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : + MetaM (Option (List MVarId)) := mvarId.withContext do + let target ← mvarId.getType' + let some (_, _, rhs) := target.eq? | return none + let rec go (exceptions : Std.HashSet MatchToSplit) : MetaM (Option (List MVarId)) := do + let some candidate ← findMatchToSplit? rhs declNames exceptions | return none + let saved ← saveState + try + let branches ← Split.refineMatch mvarId candidate.declName candidate.levels candidate.params candidate.discrs + let branches ← branches.mapM fun branch => do + let normalized ← normalizeEqn branch + if normalized == branch then + throwError "case split did not reduce the right-hand side" + return normalized + return some branches + catch ex => + saved.restore + trace[Elab.definition.eqns] "cannot split {.ofConstName candidate.declName}\n{ex.toMessageData}" + go (exceptions.insert candidate) + go {} +/-- +Calculates equation statements by normalizing the initial goal, recursively splitting eligible +matches, and saving terminal goals. Each recursive call receives an already-normalized RHS. +The resulting statements are proved separately by `mkEqnProof`. +-/ partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do - let (_, eqnTypes) ← go mvarId |>.run #[] + let (_, eqnTypes) ← go (← normalizeEqn mvarId) |>.run #[] return eqnTypes where go (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := do trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}" - -- `saveEqn` only puts back the let-declarations that the equation uses, so the unused root - -- `let`s and `have`s are dropped. - let mvarId ← introRootLets mvarId - if let some mvarIds ← tryStep? mvarId declNames then + if let some mvarIds ← splitMatch? mvarId declNames then mvarIds.forM go else saveEqn mvarId /-- - Some of the hypotheses added by `mkEqnTypes` may not be used by the actual proof (i.e., `value` argument). - This method eliminates them. - - Alternative solution: improve `saveEqn` and make sure it never includes unnecessary hypotheses. - These hypotheses are leftovers from tactics such as `splitMatch?` used in `mkEqnTypes`. +Removes parameters unused by both the equation's conclusion and its proof, retaining the +transitive type dependencies of the remaining parameters. -/ def removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr) := do go declType declValue #[] {} @@ -752,6 +573,7 @@ structure EqnTypes where types : Array Expr deriving TypeName +/-- Computes equation statements under the definition's saved options and a fresh metavariable depth. -/ def realizeEqnTypes (key : EqnTypesKey) : MetaM EqnTypes := withEqnOptions key.declName <| withOptions (tactic.hygienic.set · false) do let target ← unfoldThmType key.declName @@ -762,6 +584,10 @@ def realizeEqnTypes (key : EqnTypesKey) : MetaM EqnTypes := mkEqnTypes key.declNames goal.mvarId! return { types } +/-- +Proves and registers one equation, removes unused parameters, and infers its definitional-equality +attribute. +-/ def realizeEqn (declName name : Name) (type : Expr) : MetaM Unit := withEqnOptions declName <| withOptions (tactic.hygienic.set · false) do let info ← getConstInfoDefn declName @@ -797,6 +623,11 @@ def mkEqns (declName : Name) (declNames : Array Name) : MetaM (Array Name) := do realizeConst declName name (realizeEqn declName name type) return thmNames +/-- +Equation-theorem provider for definitions. Recursive definitions use split equations; +nonrecursive definitions use either split equations or one unfolding equation, according to +`backward.eqns.nonrecursive`. +-/ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do if (← isRecursiveDefinition declName) then let some (.defnInfo info) := (← getEnv).find? declName | diff --git a/src/Lean/Meta/Match/Rewrite.lean b/src/Lean/Meta/Match/Rewrite.lean index 66b56cff539f..f67678c66800 100644 --- a/src/Lean/Meta/Match/Rewrite.lean +++ b/src/Lean/Meta/Match/Rewrite.lean @@ -128,7 +128,9 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do else if hType.isEq then h.assumption <|> h.refl <|> throwError m!"Failed to resolve `{h}`" else if hType.isHEq then - h.assumption <|> h.hrefl <|> throwError m!"Failed to resolve `{h}`" + -- Splitting may provide an `Eq` hypothesis where the matcher equation requires `HEq`. + h.assumption <|> h.hrefl <|> (do (← h.heqOfEq).assumption) <|> + throwError m!"Failed to resolve `{h}`" let unassignedHyps ← hyps.filterM fun h => return !(← h.isAssigned) unless unassignedHyps.isEmpty do throwError m!"Not all hypotheses of `{.ofConstName eqnThm}` could be discharged: {unassignedHyps}" diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 926a29ced11c..bb212162211f 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -249,7 +249,10 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs : | none => mvarId := mvarId' return mvarId -def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := do +private def applyMatchSplitterCore (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) + (params : Array Expr) (discrs : Array Expr) + (generalize : MVarId → Expr → Array Expr → MetaM (Array FVarId × Array FVarId × MVarId)) : + MetaM (List MVarId) := do let some info ← getMatcherInfo? matcherDeclName | throwInternalMisuseError m!"Internal error in `split` tactic: `{matcherDeclName}` is not an auxiliary declaration used to encode `match`-expressions" let matchEqns ← Match.getEquationsFor matcherDeclName -- splitterPre does not have the correct universe elimination level, but this is fine, we only use it to compute the `motiveType`, @@ -257,9 +260,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le let splitterPre := mkAppN (mkConst matchEqns.splitterName us.toList) params let motiveType := (← whnfForall (← inferType splitterPre)).bindingDomain! trace[split.debug] "applyMatchSplitter\n{mvarId}" - let (discrs, mvarId) ← generalizeMatchPropDiscrs mvarId discrs - trace[split.debug] "after generalizeMatchPropDiscrs\n{mvarId}" - let (discrFVarIds, discrEqs, mvarId) ← generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs + let (discrFVarIds, discrEqs, mvarId) ← generalize mvarId motiveType discrs trace[split.debug] "after generalizeMatchDiscrs\n{mvarId}" let mvarId ← generalizeTargetsEq mvarId motiveType (discrFVarIds.map mkFVar) mvarId.withContext do trace[split.debug] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}" @@ -303,6 +304,35 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le return (i+1, mvarId::mvarIds) return mvarIds.reverse +def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := + applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs => do + let (discrs, mvarId) ← generalizeMatchPropDiscrs mvarId discrs + trace[split.debug] "after generalizeMatchPropDiscrs\n{mvarId}" + generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs + +/-- +Refines a goal into the cases of a matcher applied to `params` and `discrs`, without replacing +matcher occurrences in the target. The arguments must be well-typed in the goal's context, but +the matcher application need not occur in the target. + +Computed discriminants are linked to fresh variables by equalities. After splitting, these +equalities specialize the goal where possible; unresolved conditions remain as hypotheses. +The target is not simplified. +-/ +def refineMatch (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) + (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := mvarId.withContext do + applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs => + mvarId.withContext do + if ← discrs.allM fun discr => do + unless discr.isFVar do return false + return !(← discr.fvarId!.getDecl).isLet + then + return (discrs.map (·.fvarId!), #[], mvarId) + let mvarId ← generalizeTargetsEq mvarId motiveType discrs + let (discrFVarIds, mvarId) ← mvarId.introN discrs.size + let (discrEqs, mvarId) ← mvarId.introN discrs.size + return (discrFVarIds, discrEqs, mvarId) + def mkDiscrGenErrorMsg (e : Expr) : MessageData := m!"`split` tactic failed to generalize discriminant(s) at{indentExpr e}\nresulting expression was not type correct\npossible solution: generalize discriminant(s) manually before using `split`" diff --git a/tests/elab/1074a.lean b/tests/elab/1074a.lean index 229bd10201a9..336b7a79a7ef 100644 --- a/tests/elab/1074a.lean +++ b/tests/elab/1074a.lean @@ -1,3 +1,5 @@ +/-! Equation generation for recursive elimination of proofs. -/ + inductive Term : Type | id2: Term -> Term -> Term @@ -19,10 +21,7 @@ def Brx.interp_nil (H: Brx a): H.interp = H.interp } /-- -info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) : - H_2.interp = - match ⋯ with - | ⋯ => Hz.interp +info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) : H_2.interp = ⋯.interp -/ #guard_msgs in #check Brx.interp.eq_1 diff --git a/tests/elab/5667.lean b/tests/elab/5667.lean index 78cbc1663cbf..71807490f311 100644 --- a/tests/elab/5667.lean +++ b/tests/elab/5667.lean @@ -1,3 +1,5 @@ +/-! Equation generation for structural and mutual recursion with multiple discriminants (#5667). -/ + inductive Expr where | const (i : BitVec 32) | op (op : Unit) (e1 : Expr) @@ -25,10 +27,10 @@ info: optimize.eq_def (x✝ : Expr) : /-- info: equations: @[backward_defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i -theorem optimize.eq_2 : ∀ (e1 : Expr) (bop : Unit) (i : BitVec 32), - optimize e1 = Expr.const i → optimize (Expr.op bop e1) = Expr.op bop (Expr.const 0) -theorem optimize.eq_3 : ∀ (e1 : Expr) (bop : Unit), - (∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop e1) = Expr.const 0 +theorem optimize.eq_2 : ∀ (e1 : Expr) (bop_1 : Unit) (i : BitVec 32), + optimize e1 = Expr.const i → optimize (Expr.op bop_1 e1) = Expr.op bop_1 (Expr.const 0) +theorem optimize.eq_3 : ∀ (e1 : Expr) (bop_1 : Unit), + (∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop_1 e1) = Expr.const 0 -/ #guard_msgs in #print equations optimize diff --git a/tests/elab/byteSliceIssue.lean b/tests/elab/byteSliceIssue.lean index 4d2388365857..974f2899b926 100644 --- a/tests/elab/byteSliceIssue.lean +++ b/tests/elab/byteSliceIssue.lean @@ -1,3 +1,5 @@ +/-! Equation generation for a well-founded monadic byte-slice loop. -/ + def Nat.Up (ub a i : Nat) := i < a ∧ i < ub theorem Nat.Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩ diff --git a/tests/elab/byteSliceIssue.lean.out.expected b/tests/elab/byteSliceIssue.lean.out.expected index 5566ffd9435e..b05a0aae73fd 100644 --- a/tests/elab/byteSliceIssue.lean.out.expected +++ b/tests/elab/byteSliceIssue.lean.out.expected @@ -5,7 +5,5 @@ let __do_lift ← f (arr.get! i) b match __do_lift with | ForInStep.done b => pure b - | ForInStep.yield b => - have this := ⋯; - forIn.loop f arr off _end (i + 1) b + | ForInStep.yield b => forIn.loop f arr off _end (i + 1) b else pure b diff --git a/tests/elab/eqns_issues.lean b/tests/elab/eqns_issues.lean index 5617fdce4fe4..b13afe9a5297 100644 --- a/tests/elab/eqns_issues.lean +++ b/tests/elab/eqns_issues.lean @@ -1,7 +1,14 @@ +module + +import Lean + /-! -Cases where the equation lemmas still copy values that could stay shared. The `#guard_msgs` -blocks are the expected results; they fail on the current implementation. +Regression tests for equation lemmas preserving shared values, nested binding scopes, and binding +kinds while splitting matches (#16122). -/ +@[expose] public section + +set_option linter.unusedVariables false -- 1. A `have` inside the value of a `have` whose `match` is split. def innerHave (x : Nat) : Nat := @@ -80,6 +87,7 @@ info: discrDep.eq_2 (n : Nat) : #guard_msgs in #check discrDep.eq_2 -- 4. With `cleanup.letToHave false`, the `have` stays a `have`. +set_option cleanup.letToHave false in def noCleanup (x : Nat) : Nat := have y := x + 1 y + y @@ -91,3 +99,247 @@ info: noCleanup.eq_1 (x : Nat) : y + y -/ #guard_msgs in #check noCleanup.eq_1 + +-- A dependent binding and a nondependent `let` retain their binding kinds too. +set_option cleanup.letToHave false in +def noCleanupLet (x : Nat) : Nat := + let y := x + 1 + y + y + +/-- +info: noCleanupLet.eq_1 (x : Nat) : + noCleanupLet x = + let y := x + 1; + y + y +-/ +#guard_msgs in #check noCleanupLet.eq_1 + +set_option cleanup.letToHave false in +def noCleanupDependent (x : Nat) : Fin 5 := + let n := 4 + match x with + | 0 => (⟨n, by decide⟩ : Fin (n + 1)) + | _ + 1 => 0 + +/-- +info: noCleanupDependent.eq_1 : + noCleanupDependent 0 = + let n := 4; + ⟨n, noCleanupDependent._proof_1⟩ +-/ +#guard_msgs in #check noCleanupDependent.eq_1 + +-- The computed discriminant remains shared even when it also occurs in a branch hypothesis. +def computedPremise (f : Nat → Nat) (x : Nat) : Nat := + have k := f x + match x, k with + | 0, _ => 1 + | _, 0 => 2 + | n + 1, m + 1 => n + k + k + m + +/-- +info: equations: +@[backward_defeq] theorem computedPremise.eq_1 : ∀ (f : Nat → Nat), computedPremise f 0 = 1 +theorem computedPremise.eq_2 : ∀ (f : Nat → Nat) (x_1 : Nat), (x_1 = 0 → False) → f x_1 = 0 → computedPremise f x_1 = 2 +theorem computedPremise.eq_3 : ∀ (f : Nat → Nat) (n m : Nat), + f n.succ = m.succ → + computedPremise f n.succ = + have k := f n.succ; + n + k + k + m +-/ +#guard_msgs in #print equations computedPremise + +-- Each inner `y` belongs to its own binding value, including the value without a match. +def nestedScopes (x : Nat) : Nat := + have a := + have y := x + 1 + match x with + | 0 => y + y + | n + 1 => y + y + n + have b := + have y := x * x + a + y + y + a + b + b + +/-- +info: nestedScopes.eq_2 (n : Nat) : + nestedScopes n.succ = + have a := + have y := n.succ + 1; + y + y + n; + have b := + have y := n.succ * n.succ; + a + y + y; + a + b + b +-/ +#guard_msgs in #check nestedScopes.eq_2 + +-- A match in a dead binding must not produce extra equations. +def unusedValue (x : Nat) : Nat := + have y := match x with + | 0 => 1 + | _ + 1 => 2 + 7 + +/-- +info: equations: +@[backward_defeq] theorem unusedValue.eq_1 : ∀ (x : Nat), unusedValue x = 7 +-/ +#guard_msgs in #print equations unusedValue + +-- Matches capturing a lambda parameter stay inside the lambda; independent matches can split. +def lambdaCapture (x : Nat) (ys : List Nat) : List Nat := + ys.map fun y => match x with + | 0 => y + | n + 1 => n + y + +def lambdaIndependent (x : Nat) (ys : List Nat) : List Nat := + ys.map fun _ => match x with + | 0 => 7 + | n + 1 => n + +open Lean Meta in +run_meta do + for (decl, count) in #[(``lambdaCapture, 1), (``lambdaIndependent, 2)] do + let some eqns ← getEqnsFor? decl | throwError "missing equations for {decl}" + unless eqns.size == count do + throwError "expected {count} equations for {decl}, got {eqns.size}" + +-- A value fixed by the result type still reduces matches through local constructor aliases. +set_option cleanup.letToHave false in +def fixedValue (x : Nat) : Fin (x + 1) := + let n := + have a := some x + have b := a + match b with + | none => 0 + | some k => k + (⟨0, Nat.zero_lt_succ n⟩ : Fin (n + 1)) + +open Lean Meta in +run_meta do + let some eqns ← getEqnsFor? ``fixedValue | throwError "missing equations" + unless eqns.size == 1 do throwError "expected one equation, got {eqns.size}" + forallTelescope (← getConstInfo eqns[0]!).type fun xs body => do + let some (_, _, .letE _ _ value _ false) := body.eq? + | throwError "dependent binding was lost" + unless value == xs[0]! do throwError "constructor aliases in the fixed value did not reduce" + +example (x : Nat) : (fixedValue x).val = 0 := by + rw [fixedValue.eq_1] + +-- Once a branch drops dependent uses, its remaining shared value can simplify propositionally. +set_option cleanup.letToHave false in +def branchDeadValueBarrier (x : Nat) : Nat := + have a := match x with | 5 => 1 | _ => 2 + let n := a + 1 + have v : Fin n := ⟨a, Nat.lt_succ_self a⟩ + match x with + | 5 => v.val + | _ => a + a + +open Lean Meta in +run_meta do + let some eqns ← getEqnsFor? ``branchDeadValueBarrier | throwError "missing equations" + unless eqns.size == 2 do throwError "expected two equations, got {eqns.size}" + for eqn in eqns do + discard <| getConstInfo eqn + forallTelescope (← getConstInfo eqns[1]!).type fun _ body => do + let some (_, _, .letE _ _ value _ true) := body.eq? + | throwError "shared value was lost" + unless ← isDefEq value (mkNatLit 2) do throwError "branch value did not simplify" + +-- Expanding this value before finding the match would duplicate the chain exponentially. +def nestedChain (x : Nat) : Nat := + have a := + have v0 := x * x + x + have v1 := v0 + v0 + have v2 := v1 + v1 + have v3 := v2 + v2 + have v4 := v3 + v3 + have v5 := v4 + v4 + have v6 := v5 + v5 + have v7 := v6 + v6 + have v8 := v7 + v7 + have v9 := v8 + v8 + have v10 := v9 + v9 + have v11 := v10 + v10 + have v12 := v11 + v11 + have v13 := v12 + v12 + have v14 := v13 + v13 + have v15 := v14 + v14 + have v16 := v15 + v15 + have v17 := v16 + v16 + have v18 := v17 + v17 + have v19 := v18 + v18 + have v20 := v19 + v19 + have v21 := v20 + v20 + have v22 := v21 + v21 + have v23 := v22 + v22 + have v24 := v23 + v23 + match x with + | 0 => v24 + | n + 1 => v24 + v24 + n + a + a + +open Lean Meta in +run_meta do + let some eqns ← getEqnsFor? ``nestedChain | throwError "missing equations" + unless eqns.size == 2 do throwError "expected two equations, got {eqns.size}" + for eqn in eqns do + let type := (← getConstInfo eqn).type + forallTelescope type fun _ body => do + let some (_, _, rhs) := body.eq? | throwError "expected an equation" + let .letE `a _ value _ true := rhs | throwError "outer have was lost" + let mut value := value + let mut count : Nat := 0 + while let .letE _ _ _ body true := value do + count := count + 1 + value := body + unless count == 25 do throwError "expected 25 nested haves, got {count}" + unless (← rhs.numObjs) < 1000 do throwError "equation exceeded the size bound" + +open Lean Meta in +run_meta do + for (decl, nondep) in #[(``noCleanup, true), (``noCleanupLet, false), + (``noCleanupDependent, false)] do + let some eqns ← getEqnsFor? decl | throwError "missing equations for {decl}" + forallTelescope (← getConstInfo eqns[0]!).type fun _ body => do + let some (_, _, .letE _ _ _ _ actual) := body.eq? + | throwError "binding was lost in {decl}" + unless actual == nondep do throwError "binding kind changed in {decl}" + +/-- +info: nestedChain.eq_2 (n : Nat) : + nestedChain n.succ = + have a := + have v0 := n.succ * n.succ + n.succ; + have v1 := v0 + v0; + have v2 := v1 + v1; + have v3 := v2 + v2; + have v4 := v3 + v3; + have v5 := v4 + v4; + have v6 := v5 + v5; + have v7 := v6 + v6; + have v8 := v7 + v7; + have v9 := v8 + v8; + have v10 := v9 + v9; + have v11 := v10 + v10; + have v12 := v11 + v11; + have v13 := v12 + v12; + have v14 := v13 + v13; + have v15 := v14 + v14; + have v16 := v15 + v15; + have v17 := v16 + v16; + have v18 := v17 + v17; + have v19 := v18 + v18; + have v20 := v19 + v19; + have v21 := v20 + v20; + have v22 := v21 + v21; + have v23 := v22 + v22; + have v24 := v23 + v23; + v24 + v24 + n; + a + a +-/ +#guard_msgs in +#check nestedChain.eq_2 diff --git a/tests/elab/eqns_keep_have.lean b/tests/elab/eqns_keep_have.lean index 382217ead397..8cc24f3cfc63 100644 --- a/tests/elab/eqns_keep_have.lean +++ b/tests/elab/eqns_keep_have.lean @@ -1,7 +1,11 @@ +module + /-! Tests that equation lemmas keep the `have`s at the root of the right-hand side, also above a split `match`, so that `vcgen +jp [f]` sees the join points of `f` (#16122). -/ +@[expose] public section + set_option linter.unusedVariables false def f (x : Nat) : Nat := @@ -178,7 +182,12 @@ def discr2 (x : Nat) : Nat := | 0, _ => 1 | n + 1, m => n + m -/-- info: discr2.eq_2 (n : Nat) : discr2 n.succ = n + (n.succ + 2) -/ +/-- +info: discr2.eq_2 (n : Nat) : + discr2 n.succ = + have k := n.succ + 2; + n + k +-/ #guard_msgs in #check discr2.eq_2 -- The `match` in the value of the `have` is split, and the `have` is kept. @@ -353,9 +362,7 @@ info: unusedBranch.eq_1 (x a : Nat) : -/ #guard_msgs in #check unusedBranch.eq_1 --- Splitting `x` exposes a `match` in the value of `c`, which must then be split too. The outer --- `match` generalizes the `have`s, whose values depend on `x`, so the `match x` in the value of `a` --- is split first, and the outer `match` then reduces. +-- Nested matches in a binding value are split while its sharing and scope are preserved. def nestedValueCases (x : Nat) : Nat := have a := have b := x + 1 @@ -371,7 +378,9 @@ def nestedValueCases (x : Nat) : Nat := /-- info: nestedValueCases.eq_1 : nestedValueCases 0 = - have a := 0 + 1; + have a := + have b := 0 + 1; + b; have c := a + a; c -/ @@ -380,13 +389,15 @@ info: nestedValueCases.eq_1 : /-- info: nestedValueCases.eq_3 (n_1 : Nat) : nestedValueCases n_1.succ.succ = - have a := n_1.succ.succ + 1 + n_1; + have a := + have b := n_1.succ.succ + 1; + b + n_1; have c := a + a; c + n_1.succ -/ #guard_msgs in #check nestedValueCases.eq_3 --- The target reaches the `match` in the value of `c` only through `d`. +-- Shared dependencies reach the nested match without expanding intermediate values. def nestedValueChain (x : Nat) : Nat := have a := have b := x + 1 @@ -402,7 +413,9 @@ def nestedValueChain (x : Nat) : Nat := /-- info: nestedValueChain.eq_3 (n_1 : Nat) : nestedValueChain n_1.succ.succ = - have a := n_1.succ.succ + 1 + n_1; + have a := + have b := n_1.succ.succ + 1; + b + n_1; have c := a + a; have d := c + c; d + n_1.succ @@ -449,17 +462,17 @@ info: equations: have b := a; b + b @[backward_defeq] theorem twoVals.eq_2 : ∀ (n : Nat), - twoVals n.succ 0 = - have a := 2; - have b := a; - b + b -@[backward_defeq] theorem twoVals.eq_3 : ∀ (n : Nat), twoVals 0 n.succ = have a := 1; have b := a + 1; b + b +@[backward_defeq] theorem twoVals.eq_3 : ∀ (n : Nat), + twoVals n.succ 0 = + have a := 2; + have b := a; + b + b @[backward_defeq] theorem twoVals.eq_4 : ∀ (n n_1 : Nat), - twoVals n_1.succ n.succ = + twoVals n.succ n_1.succ = have a := 2; have b := a + 1; b + b @@ -519,8 +532,13 @@ def valAndTarget (x : Nat) : Nat := | n + 1 => y + n /-- info: equations: -@[backward_defeq] theorem valAndTarget.eq_1 : valAndTarget 0 = 1 + 1 -@[backward_defeq] theorem valAndTarget.eq_2 : ∀ (n : Nat), valAndTarget n.succ = 2 + n +@[backward_defeq] theorem valAndTarget.eq_1 : valAndTarget 0 = + have y := 1; + y + y +@[backward_defeq] theorem valAndTarget.eq_2 : ∀ (n : Nat), + valAndTarget n.succ = + have y := 2; + y + n -/ #guard_msgs in #print equations valAndTarget diff --git a/tests/elab/eqns_telescope_proofs.lean b/tests/elab/eqns_telescope_proofs.lean new file mode 100644 index 000000000000..575d5390dcd8 --- /dev/null +++ b/tests/elab/eqns_telescope_proofs.lean @@ -0,0 +1,94 @@ +module +import Lean +public meta import Lean.Meta.Tactic.Refl +import all Lean.Elab.PreDefinition.Eqns + +/-! +Checks the kernel proofs produced by equation normalization for simultaneous binding-value and +body rewrites, mixed let/have telescopes, transitive type dependencies, dependent results, and +matcher rewriting under local assumptions. +-/ + +open Lean Meta Elab + +def valueAndBody (x y : Nat) : Nat := + have a := match x with | 5 => 1 | _ => 2 + have b := a + 1 + have c := match y with | 5 => b | _ => b + b + match x with | 5 => c | _ => c + a + +set_option cleanup.letToHave false in +def mixedDependent (x y : Nat) : Nat := + have a := match x with | 5 => 1 | _ => 2 + let t := Fin (a + 1) + have z : t := ⟨a, Nat.lt_succ_self a⟩ + have b := match y with | 5 => z.val | _ => z.val + z.val + match y with | 5 => b | _ => b + a + +set_option cleanup.letToHave false in +def dependentResult (x y : Nat) : Fin (x + 2) := + let n := x + 1 + have _a := match y with | 5 => 0 | _ => 1 + have b : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩ + match y with | 5 => ⟨0, Nat.zero_lt_succ n⟩ | _ => b + +meta def checkNormalizationProof (body : Expr) : MetaM Expr := do + let lhs ← mkFreshExprMVar (← inferType body) + let goal ← mkFreshExprSyntheticOpaqueMVar (← mkEq lhs body) + let normalized ← Lean.Elab.Eqns.normalizeEqn goal.mvarId! + let some (_, _, rhs) := (← normalized.getType').eq? | throwError "expected an equation" + if ← isDefEq body rhs then throwError "expected a nondefinitional rewrite" + normalized.refl + let proof ← instantiateMVars goal + checkWithKernel proof + unless ← isDefEq (← inferType proof) (← mkEq rhs body) do + throwError "incorrect telescope proof type" + return rhs + +run_meta do + for name in #[``valueAndBody, ``mixedDependent, ``dependentResult] do + let info ← getConstInfoDefn name + lambdaTelescope info.value fun xs body => do + withLocalDeclD `hx (mkNot (← mkEq xs[0]! (mkNatLit 5))) fun _ => do + withLocalDeclD `hy (mkNot (← mkEq xs[1]! (mkNatLit 5))) fun _ => do + discard <| checkNormalizationProof body + +def literalMatcher (x : Nat) : Nat := match x with | 5 => 1 | _ => 2 + +-- Reusing a matcher across a lambda boundary must respect the hypothesis's scope in either order. +run_meta do + withLocalDeclD `x (mkConst ``Nat) fun x => do + let .lam _ _ body _ := (← getConstInfoDefn ``literalMatcher).value + | throwError "unexpected matcher template" + let matcher := body.instantiate1 x + let fn := mkLambda `h .default (mkNot (← mkEq x (mkNatLit 5))) matcher + for reverse in [false, true] do + let pair ← mkAppM ``Prod.mk (if reverse then #[matcher, fn] else #[fn, matcher]) + let rhs ← checkNormalizationProof pair + let_expr Prod.mk _ _ fst snd := rhs | throwError "expected a pair" + let (fn', matcher') := if reverse then (snd, fst) else (fst, snd) + let .lam _ _ body' _ := fn' | throwError "expected a lambda" + unless ← isDefEq body' (mkNatLit 2) do + throwError "matcher did not simplify under the local hypothesis" + unless matcher' == matcher do + throwError "matcher changed outside the hypothesis's scope" + +def zeroMatcher (x : Nat) : Nat := match x with | 0 => 1 | _ => 2 + +-- A proof binding can enable rewriting a matcher whose earlier occurrence was unchanged. +run_meta do + lambdaTelescope (← getConstInfoDefn ``zeroMatcher).value fun xs matcher => do + let x := xs[0]! + let nat := mkConst ``Nat + withLocalDeclD `hx (← mkEq (mkNatAdd x x) (mkNatLit 0)) fun hx => do + let proof ← mkAppM ``Nat.eq_zero_of_add_eq_zero_left #[hx] + let body ← withLetDecl `a nat matcher (nondep := true) fun a => do + withLetDecl `h (← mkEq x (mkNatLit 0)) proof (nondep := true) fun h => do + withLetDecl `b nat matcher (nondep := true) fun b => do + mkLetFVars #[a, h, b] (mkNatAdd a b) (usedLetOnly := false) (generalizeNondepLet := false) + let rhs ← checkNormalizationProof body + let .letE _ _ valueA (.letE _ _ valueB _ true) true := rhs + | throwError "expected both shared bindings" + unless valueA == matcher do throwError "earlier matcher changed before the proof binding" + unless ← isDefEq valueB (mkNatLit 1) do + throwError "later matcher did not simplify under the proof binding" diff --git a/tests/elab/heapSort.lean b/tests/elab/heapSort.lean index 92b04f3f7326..e47fd51c3328 100644 --- a/tests/elab/heapSort.lean +++ b/tests/elab/heapSort.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +/-! Tests heap operations, heap sorting, and their generated equation theorems. -/ + /-- A max-heap data structure. -/ structure BinaryHeap (α) (lt : α → α → Bool) where arr : Array α @@ -184,9 +186,7 @@ info: Array.heapSort.loop.eq_1 fun a b => let gt := fun y x => decide (x < y); match e : a.max with | none => out - | some x => - have this := ⋯; - Array.heapSort.loop (fun a b => decide (a < b)) a.popMax (out.push x) + | some x => Array.heapSort.loop (fun a b => decide (a < b)) a.popMax (out.push x) -/ #guard_msgs in #check Array.heapSort.loop.eq_1 (fun (a b : Nat) => a < b) diff --git a/tests/elab/heapSort.lean.out.expected b/tests/elab/heapSort.lean.out.expected index 5aeaa1953627..29c2b2306a4f 100644 --- a/tests/elab/heapSort.lean.out.expected +++ b/tests/elab/heapSort.lean.out.expected @@ -1,11 +1,11 @@ -heapSort.lean:15:4-15:15: warning: declaration uses `sorry` -heapSort.lean:15:4-15:15: warning: declaration uses `sorry` -heapSort.lean:13:0-36:24: warning: declaration uses `sorry` -heapSort.lean:13:0-36:24: warning: declaration uses `sorry` -heapSort.lean:43:4-43:10: warning: declaration uses `sorry` -heapSort.lean:58:4-58:13: warning: declaration uses `sorry` -heapSort.lean:58:4-58:13: warning: declaration uses `sorry` -heapSort.lean:56:0-69:24: warning: declaration uses `sorry` -heapSort.lean:56:0-69:24: warning: declaration uses `sorry` -heapSort.lean:102:4-102:13: warning: declaration uses `sorry` +heapSort.lean:17:4-17:15: warning: declaration uses `sorry` +heapSort.lean:17:4-17:15: warning: declaration uses `sorry` +heapSort.lean:15:0-38:24: warning: declaration uses `sorry` +heapSort.lean:15:0-38:24: warning: declaration uses `sorry` +heapSort.lean:45:4-45:10: warning: declaration uses `sorry` +heapSort.lean:60:4-60:13: warning: declaration uses `sorry` +heapSort.lean:60:4-60:13: warning: declaration uses `sorry` +heapSort.lean:58:0-71:24: warning: declaration uses `sorry` +heapSort.lean:58:0-71:24: warning: declaration uses `sorry` +heapSort.lean:104:4-104:13: warning: declaration uses `sorry` heapSort.lean:194:11-194:15: warning: declaration uses `sorry` diff --git a/tests/elab/splitList.lean.out.expected b/tests/elab/splitList.lean.out.expected index b3be2e52d89b..a196d0620e50 100644 --- a/tests/elab/splitList.lean.out.expected +++ b/tests/elab/splitList.lean.out.expected @@ -3,11 +3,7 @@ @len.eq_3 : ∀ {α : Type u_1} (a b : α) (as : List α), len (a :: b :: as) = match h : a :: b :: as, h₂ : splitList (a :: b :: as), ⋯ with - | .(fst ++ snd), ListSplit.split fst snd, h₁ => - have this := ⋯; - have dec₁ := ⋯; - have dec₂ := ⋯; - len fst + len snd + | .(fst ++ snd), ListSplit.split fst snd, h₁ => len fst + len snd @len.eq_def : ∀ {α : Type u_1} (x : List α), len x = match x with diff --git a/tests/elab/split_refine_match.lean b/tests/elab/split_refine_match.lean new file mode 100644 index 000000000000..d88dad9f1c35 --- /dev/null +++ b/tests/elab/split_refine_match.lean @@ -0,0 +1,69 @@ +module +import Lean +public meta import Lean.Meta.Tactic.Split + +/-! +Tests matcher-based case refinement of a target containing no matcher application, including +overlapping patterns, computed discriminants, and discriminants closed over shared bindings. +-/ + +open Lean Meta Elab + +private def matcherTemplate (x y : Nat) : Nat := + match x, y with + | 0, _ => 1 + | _, 0 => 2 + | n + 1, m + 1 => n + m + +private meta def hasHypothesis (type : Expr) : MetaM Bool := do + for decl in ← getLCtx do + if ← isDefEq decl.type type then return true + return false + +private meta def checkRefinement (app : MatcherApp) (x p : Expr) + (discr : Expr → MetaM Expr) (shared : Bool) : MetaM Unit := do + let goal ← mkFreshExprSyntheticOpaqueMVar (mkApp p x) + let branches ← Split.refineMatch goal.mvarId! app.matcherName app.matcherLevels app.params + #[x, ← discr x] + unless branches.length == 3 do throwError "expected three branches" + for i in *...3 do + let branch := branches[i]! + branch.withContext do + let target ← branch.getType' + unless target.isApp && target.appFn! == p do + throwError "refinement changed the target predicate" + let arg := target.appArg! + match i with + | 0 => + unless ← isDefEq arg (mkNatLit 0) do throwError "first branch did not specialize x to zero" + | 1 => + unless arg.isFVar do throwError "overlapping branch specialized x" + unless ← hasHypothesis (mkNot (← mkEq arg (mkNatLit 0))) do + throwError "missing overlap hypothesis" + unless ← hasHypothesis (← mkEq (← discr arg) (mkNatLit 0)) do + throwError "missing computed-discriminant hypothesis" + | _ => + unless arg.isAppOfArity ``Nat.succ 1 && arg.appArg!.isFVar do + throwError "last branch did not specialize x to a successor" + let expected ← discr arg + let mut found := false + for decl in ← getLCtx do + if let some (_, lhs, rhs) := decl.type.eq? then + if rhs.isAppOfArity ``Nat.succ 1 && rhs.appArg!.isFVar then + if ← isDefEq lhs expected then + if shared && !lhs.isLet then throwError "discriminant sharing was lost" + found := true + unless found do throwError "missing successor discriminant hypothesis" + +run_meta do + let info ← getConstInfoDefn ``matcherTemplate + lambdaTelescope info.value fun xs rhs => do + let some app ← matchMatcherApp? rhs | throwError "expected matcher" + let nat := mkConst ``Nat + withLocalDeclD `f (← mkArrow nat nat) fun f => do + withLocalDeclD `p (← mkArrow nat (mkSort 0)) fun p => do + checkRefinement app xs[0]! p (fun x => pure (mkApp f x)) false + checkRefinement app xs[0]! p (fun x => + withLetDecl `a nat (mkApp f x) (nondep := true) fun a => + withLetDecl `b nat (mkNatAdd a a) (nondep := true) fun b => + mkLetFVars #[a, b] (mkNatAdd b b) (generalizeNondepLet := false)) true diff --git a/tests/elab/streamEqIssue.lean.out.expected b/tests/elab/streamEqIssue.lean.out.expected index 6113afb57bee..53641cf5b562 100644 --- a/tests/elab/streamEqIssue.lean.out.expected +++ b/tests/elab/streamEqIssue.lean.out.expected @@ -1,10 +1,10 @@ @Std.Stream.hasLength.eq_1 : ∀ {stream : Type u_1} {value : Type u_2} [inst : Std.Stream stream value] (s : stream), Std.Stream.next? s = none → Std.Stream.hasLength 0 s = true @Std.Stream.hasLength.eq_2 : ∀ {stream : Type u_1} {value : Type u_2} [inst : Std.Stream stream value] (s : stream) - (n_2 : Nat) (s' : stream) (fst : value), - Std.Stream.next? s = some (fst, s') → Std.Stream.hasLength n_2.succ s = Std.Stream.hasLength n_2 s' + (n_3 : Nat) (s' : stream) (fst : value), + Std.Stream.next? s = some (fst, s') → Std.Stream.hasLength n_3.succ s = Std.Stream.hasLength n_3 s' @Std.Stream.hasLength.eq_3 : ∀ {stream : Type u_1} {value : Type u_2} [inst : Std.Stream stream value] (s : stream) - (n : Nat), - (n = 0 → Std.Stream.next? s = none → False) → - (∀ (n_1 : Nat) (fst : value) (s' : stream), n = n_1.succ → Std.Stream.next? s = some (fst, s') → False) → - Std.Stream.hasLength n s = false + (n_1 : Nat), + (n_1 = 0 → Std.Stream.next? s = none → False) → + (∀ (n : Nat) (fst : value) (s' : stream), n_1 = n.succ → Std.Stream.next? s = some (fst, s') → False) → + Std.Stream.hasLength n_1 s = false diff --git a/tests/elab/structuralEqn6.lean b/tests/elab/structuralEqn6.lean index 0336c5142e03..4786bab4f10a 100644 --- a/tests/elab/structuralEqn6.lean +++ b/tests/elab/structuralEqn6.lean @@ -1,3 +1,5 @@ +/-! Tests structural and well-founded equation theorems with proof discriminants. -/ + def trailingZeros (i : Int) : Nat := if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0 where @@ -10,9 +12,8 @@ where /-- info: equations: -@[backward_defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0) - (hk_2 : i.natAbs ≤ k_2 + 1), - trailingZeros.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc +@[backward_defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_3 : Nat) (hk_3 : i.natAbs ≤ k_3 + 1), + trailingZeros.aux k_3.succ i hi hk_3 acc = if h : i % 2 = 0 then trailingZeros.aux k_3 (i / 2) ⋯ ⋯ (acc + 1) else acc -/ #guard_msgs(pass trace, all) in #print equations trailingZeros.aux @@ -34,10 +35,9 @@ where /-- info: equations: -theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0) - (hk_2 : i.natAbs ≤ k_2 + 1), - trailingZeros'.aux k_2.succ i hi hk_2 acc = - if h : i % 2 = 0 then trailingZeros'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc +theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_3 : Nat) (hk_3 : i.natAbs ≤ k_3 + 1), + trailingZeros'.aux k_3.succ i hi hk_3 acc = + if h : i % 2 = 0 then trailingZeros'.aux k_3 (i / 2) ⋯ ⋯ (acc + 1) else acc -/ #guard_msgs(pass trace, all) in #print equations trailingZeros'.aux diff --git a/tests/elab_bench/eqns_have_chain.lean b/tests/elab_bench/eqns_have_chain.lean new file mode 100644 index 000000000000..f233059ed574 --- /dev/null +++ b/tests/elab_bench/eqns_have_chain.lean @@ -0,0 +1,69 @@ +module + +import Lean + +/-! +Benchmark equation generation for a match below a long chain of shared values (#16122). +Every value uses the preceding value twice, so zeta expansion would be exponential. The resulting +equations must retain the chain inside its original binding and have size linear in its length. +-/ + +open Lean Meta + +set_option maxHeartbeats 400000 +set_option maxRecDepth 100000 + +-- Opaque applications keep reduction costs independent of the chain's expanded size. +private opaque combine (a b : Nat) : Nat := a + b + +private def chainTail (x a : Nat) : Nat := + match x with + | 0 => a + | n + 1 => combine (combine a a) n + +private def makeChainDefinition (n : Nat) : MetaM Name := do + let name ← mkFreshUserName `eqnsHaveChain + let nat := mkConst ``Nat + let arrow ← mkArrow nat nat + let type ← mkArrow arrow arrow + let value ← withLocalDeclD `f arrow fun f => + withLocalDeclD `x nat fun x => do + let .lam _ _ (.lam _ _ template _) _ := (← getConstInfoDefn ``chainTail).value + | throwError "unexpected chain template" + let mut body := template.instantiateRev #[x, mkBVar 0] + for _ in [:n] do + body := mkLet `a nat (mkApp2 (mkConst ``combine) (mkBVar 0) (mkBVar 0)) body true + body := mkLet `a nat (mkApp f x) body true + body := mkLet `result nat body (mkApp2 (mkConst ``combine) (mkBVar 0) (mkBVar 0)) true + mkLambdaFVars #[f, x] body + let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) value + 1) + addDecl <| .defnDecl { name, levelParams := [], type, value, hints, safety := .safe } + enableRealizationsForConst name + return name + +run_meta do + let bench := (← IO.getEnv "TEST_BENCH") == some "1" + for n in (if bench then [200, 400, 800] else [25]) do + let name ← makeChainDefinition n + let start ← IO.monoNanosNow + let some eqns ← getEqnsFor? name | throwError "missing equations" + let infos ← eqns.mapM getConstInfo + unless ((← getEnv).toKernelEnv.find? name).isSome do + throwError "missing definition after checking equations" + let stop ← IO.monoNanosNow + if bench then + IO.println s!"measurement: eqns_have_chain_{n} {(stop - start).toFloat / 1e9} s" + unless eqns.size == 2 do throwError "expected two equations, got {eqns.size}" + for info in infos do + forallTelescope info.type fun _ body => do + let some (_, _, .letE _ _ inner _ true) := body.eq? + | throwError "outer binding was lost" + let mut value := inner + let mut count : Nat := 0 + while let .letE _ _ _ body true := value do + count := count + 1 + value := body + unless count == n + 1 do + throwError "expected {n + 1} nested bindings, got {count}" + unless (← body.numObjs) ≤ 32 * n + 256 do + throwError "equation exceeded the size bound for {n} bindings" From abd904c16611d525501dcf81d40059a1da718bc0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2026 03:43:22 +0000 Subject: [PATCH 07/17] fix: preserve have invariants during equation normalization This PR fixes generated equations whose have bindings become invalid after reducing dependent matches. Track the definitions unfolded while typechecking normalized telescopes, then substitute the corresponding have values throughout their scopes. Apply the pass after simp and dsimp, and add regressions for dependent types, named-match proof arguments, and fixed binding values. --- src/Lean/Elab/PreDefinition/Eqns.lean | 49 ++++++++++++++++++++++++--- tests/elab/eqns_have_invariant.lean | 46 +++++++++++++++++++++++++ 2 files changed, 91 insertions(+), 4 deletions(-) create mode 100644 tests/elab/eqns_have_invariant.lean diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index e8665a55a764..d773dff299fb 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -316,6 +316,43 @@ structure EqnTelescopeResult where type : Expr proof? : Option Expr := none +/-- +Unfolds `have`s whose values are needed to typecheck the normalized telescope. +The dependency check excludes the normalization proof: that proof may use a binding's value +even when the resulting body is well typed with the binding abstract. +-/ +def zetaDependentHaves (e : Expr) : MetaM Expr := do + if !e.isLet then return e + /- Values must be available during checking so that we can record which ones it unfolds. + The original binding flags in `e` determine which declarations are retained afterward. -/ + letTelescope e (preserveNondepLet := false) fun xs body => do + let deps ← withTrackingZetaDelta <| withInferTypeConfig do + for x in xs do + let decl ← x.fvarId!.getDecl + check decl.type + let value := decl.value (allowNondep := true) + /- `inferType` alone would miss ill-typed arguments inside the value. + The separate comparison also checks that its type still agrees with the declaration. -/ + check value + if !(← isDefEq decl.type (← inferType value)) then + throwLetTypeMismatchMessage decl.fvarId + check body + getZetaDeltaFVarIds + return rebuild xs deps e 0 +where + rebuild (xs : Array Expr) (deps : FVarIdSet) (e : Expr) (i : Nat) : Expr := + match e with + | .letE n t v b nondep => + let b := rebuild xs deps b (i + 1) + if nondep && deps.contains xs[i]!.fvarId! then + /- Substitute throughout the scope, including types and implicit arguments. + For `have a := 0; have q : {n // n = a} := ⟨0, rfl⟩; q.val`, + changing only `q`'s type would leave the predicate argument of `q.val` unchanged. -/ + b.instantiate1 v + else + mkLet n t v b nondep + | _ => e + /-- Simplifies the suffix `e` beginning at binding `i` of the telescope described by `info`. The preceding bindings are represented by free variables in `xs` and the cached expressions in @@ -409,7 +446,8 @@ def getEqnTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo := do /-- The `simp` callback for equation normalization. It handles complete binding telescopes before the default traversal, using `simpEqnTelescope` to preserve their nesting and sharing. Unused bindings -are removed afterward. A changed telescope is revisited: removing dependent uses can make a +are removed afterward, and `zetaDependentHaves` unfolds bindings needed to typecheck the result. +A changed telescope is revisited: removing dependent uses can make a previously fixed value eligible for propositional rewriting. A stable telescope returns `.done`. For a matcher, first try definitional reduction, then its congruence equations using local @@ -423,7 +461,8 @@ partial def simpEqn : Simp.Simproc := fun e => do let (fixed, used) ← info.computeFixedUsed false let r ← simpEqnTelescope info fixed used e 0 #[] let r := { expr := ← zetaUnused r.expr, proof? := r.proof? : Simp.Result } - return if r.expr == e then .done r else .visit r + if r.expr == e then return .done r + return .visit { r with expr := ← zetaUnused (← zetaDependentHaves r.expr) } if let some app ← matchMatcherApp? e then if let some e' ← reduceRecMatcher? e then return .visit { expr := e' } @@ -436,7 +475,8 @@ partial def simpEqn : Simp.Simproc := fun e => do The definitional counterpart of `simpEqn`, used for fixed binding values and dependent arguments that `simp` cannot rewrite propositionally. It opens a whole binding telescope, skips unused values, and definitionally simplifies the other values and body with preceding values available -as local definitions. Rebuilding preserves binding flags and removes unused bindings. +as local definitions. `zetaDependentHaves` unfolds bindings needed to typecheck the result; +remaining bindings keep their original flags, and unused bindings are removed. Matchers are reduced only definitionally; no congruence-equation proofs are used. Changed results are revisited, and the returned expression is definitionally equal to the input. @@ -447,7 +487,8 @@ partial def dsimpEqn : Simp.DSimproc := fun e => do let (_, used) ← info.computeFixedUsed false let r ← Simp.withFreshCache <| visit info used e 0 #[] let r ← zetaUnused r - return if r == e then .done r else .visit r + if r == e then return .done r + return .visit (← zetaUnused (← zetaDependentHaves r)) if ← isMatcherApp e then if let some e' ← reduceRecMatcher? e then return .visit e' return .continue diff --git a/tests/elab/eqns_have_invariant.lean b/tests/elab/eqns_have_invariant.lean new file mode 100644 index 000000000000..4c03f5afeb93 --- /dev/null +++ b/tests/elab/eqns_have_invariant.lean @@ -0,0 +1,46 @@ +module + +/-! Simplifying generated equations must preserve the `have` abstraction invariant (#16122). -/ + +def dependentMatcher : Nat := + have a := 0 + have q : { n : Nat // n = a } := + match a with + | 0 => ⟨0, rfl⟩ + | n+1 => ⟨n+1, rfl⟩ + q.val + +example (n : Nat) : dependentMatcher = 0 := by + simp -zeta only [dependentMatcher.eq_1, ← Nat.sub_self n] + simp -zeta only [Nat.sub_self] + rfl + +opaque usesProof (n : Nat) (h : n = 0) : Nat + +-- The dependency occurs inside a proof argument, while the result type remains `Nat`. +def namedMatcher : Nat := + have a := 0 + match h : a with + | 0 => usesProof a h + | _+1 => 0 + +example (n : Nat) : namedMatcher = usesProof 0 rfl := by + simp -zeta only [namedMatcher.eq_1, ← Nat.sub_self n] <;> + simp -zeta only [Nat.sub_self] <;> rfl + +-- The dependent `let` makes equation normalization use `dsimp` for `n`'s value. +set_option cleanup.letToHave false in +def fixedHave : Nat := + have n := + have a := 0 + have q : {n : Nat // n = a} := match a with + | 0 => ⟨0, rfl⟩ + | n+1 => ⟨n+1, rfl⟩ + q.val + let v : Fin (n+1) := ⟨0, Nat.zero_lt_succ n⟩ + n + v.val + +example (m : Nat) : fixedHave = 0 := by + simp -zeta only [fixedHave.eq_1, ← Nat.sub_self m] + simp -zeta only [Nat.sub_self] + rfl From 06c7186fcca8bfab4dc12e6b99baf1f72066862b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2026 04:11:08 +0000 Subject: [PATCH 08/17] chore: checkpoint equation normalization (wip) --- src/Lean/Elab/PreDefinition/Eqns.lean | 42 ++++++++++++++++++++++----- 1 file changed, 35 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index d773dff299fb..96624841755b 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -373,19 +373,31 @@ partial def simpEqnTelescope (info : HaveTelescopeInfo) (fixed used : Array Bool (e : Expr) (i : Nat) (xs : Array Expr) : Simp.SimpM EqnTelescopeResult := do if h : i < info.haveInfo.size then let hi := info.haveInfo[i] + /- + **Note**: `hi.decl` has no loose de-Bruijn indices, but `t`, `v`, and `b` might have. + We extract them from `e` to avoid unnecessary `abstract` steps. + -/ let .letE n t v b nondep := e | unreachable! let x := hi.decl.toExpr let val := hi.decl.value (allowNondep := true) - let rv ← if !used[i]! then pure { expr := val : Simp.Result } - else if fixed[i]! then pure { expr := ← Simp.dsimp val : Simp.Result } + let rv ← if !used[i]! then pure { expr := val } + else if fixed[i]! then pure { expr := (← Simp.dsimp val) } else Simp.simp val let v' := if rv.expr == val then v else rv.expr.abstract xs let hv? := rv.proof?.map (·.abstract xs) + /- + Given `have a := 0; ... match a with | 0 => ... | _ => ...`, + we want to make sure `a` is transparent when reducing the `match`. + -/ let decl := (hi.decl.setValue rv.expr).setNondep false let rb ← withExistingLocalDecls [decl] <| Simp.withNewLemmas #[x] do simpEqnTelescope info fixed used b (i + 1) (xs.push x) - let type := if fixed[i]! then mkLet n t v' rb.type false - else rb.type.lowerLooseBVars 1 1 + let type := if fixed[i]! then + /- A fixed binding may occur in the result type, so close the type with the binding. -/ + mkLet n t v' rb.type false + else + /- The type does not depend on this binding; remove its unused bound-variable slot. -/ + rb.type.lowerLooseBVars 1 1 let expr := mkLet n t v' rb.expr nondep let hb? := rb.proof?.map fun h => mkLet n t v' h false let hv? := hv?.map fun h => mkApp6 (mkConst ``congrArg [hi.level, info.level]) @@ -397,9 +409,10 @@ partial def simpEqnTelescope (info : HaveTelescopeInfo) (fixed used : Array Bool (mkLet n t v' b nondep) expr hv hb return { expr, type, proof? } else + /- Simplify the body. -/ let rb ← Simp.simp info.body return { - expr := rb.expr.abstract xs + expr := if rb.expr == info.body then e else rb.expr.abstract xs type := info.bodyType.abstract xs proof? := rb.proof?.map (·.abstract xs) } @@ -462,7 +475,10 @@ partial def simpEqn : Simp.Simproc := fun e => do let r ← simpEqnTelescope info fixed used e 0 #[] let r := { expr := ← zetaUnused r.expr, proof? := r.proof? : Simp.Result } if r.expr == e then return .done r - return .visit { r with expr := ← zetaUnused (← zetaDependentHaves r.expr) } + let mut r' ← zetaDependentHaves r.expr + if r' != r.expr then + r' ← zetaUnused r' + return .visit { r with expr := r' } if let some app ← matchMatcherApp? e then if let some e' ← reduceRecMatcher? e then return .visit { expr := e' } @@ -488,7 +504,10 @@ partial def dsimpEqn : Simp.DSimproc := fun e => do let r ← Simp.withFreshCache <| visit info used e 0 #[] let r ← zetaUnused r if r == e then return .done r - return .visit (← zetaUnused (← zetaDependentHaves r)) + let r' ← zetaDependentHaves r + if r == r' then return .visit r' + /- If some `have`-decls were inlined, some of the remaining declarations may be unused now. -/ + return .visit (← zetaUnused r') if ← isMatcherApp e then if let some e' ← reduceRecMatcher? e then return .visit e' return .continue @@ -497,10 +516,19 @@ where (xs : Array Expr) : Simp.SimpM Expr := do if h : i < info.haveInfo.size then let decl := info.haveInfo[i].decl + /- + **Note**: `decl` has no loose de-Bruijn indices, but `t`, `v`, and `b` might have. + We extract them from `e` to avoid unnecessary `abstract` steps. + -/ let .letE n t v b nondep := e | unreachable! + /- Recall that the original `decl` may be a `have`, and without `allowNondep := true`, `value` will fail. -/ let value := decl.value (allowNondep := true) let value' ← if used[i]! then Simp.dsimp value else pure value let v' := if value' == value then v else value'.abstract xs + /- + Given `have a := 0; ... match a with | 0 => ... | _ => ...`, + we want to make sure `a` is transparent when reducing the `match`. + -/ let decl := (decl.setValue value').setNondep false let b ← withExistingLocalDecls [decl] <| visit info used b (i+1) (xs.push decl.toExpr) return mkLet n t v' b nondep From d3dee0b2efc39ad67684e1370fb2722f202b1568 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2026 04:40:25 +0000 Subject: [PATCH 09/17] refactor: reuse letToHave in equation normalization Rebuild changed binding bodies with let and run letToHave before revisiting the result. Preserve sharing for dependent bindings, and cover conversion of existing lets and nested shared values in the tests and benchmarks. --- src/Lean/Elab/PreDefinition/Eqns.lean | 68 ++++++--------------------- tests/elab/eqns_issues.lean | 27 +++++++++-- tests/elab_bench/eqns_have_chain.lean | 41 ++++++++++++++++ 3 files changed, 78 insertions(+), 58 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 96624841755b..8db25720fa56 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -7,6 +7,7 @@ module prelude import Lean.Elab.PreDefinition.EqnsUtils import Lean.Meta.HaveTelescope +import Lean.Meta.LetToHave import Lean.Meta.Match.NamedPatterns import Lean.Meta.Match.Rewrite import Lean.Meta.Tactic.Simp.Main @@ -316,43 +317,6 @@ structure EqnTelescopeResult where type : Expr proof? : Option Expr := none -/-- -Unfolds `have`s whose values are needed to typecheck the normalized telescope. -The dependency check excludes the normalization proof: that proof may use a binding's value -even when the resulting body is well typed with the binding abstract. --/ -def zetaDependentHaves (e : Expr) : MetaM Expr := do - if !e.isLet then return e - /- Values must be available during checking so that we can record which ones it unfolds. - The original binding flags in `e` determine which declarations are retained afterward. -/ - letTelescope e (preserveNondepLet := false) fun xs body => do - let deps ← withTrackingZetaDelta <| withInferTypeConfig do - for x in xs do - let decl ← x.fvarId!.getDecl - check decl.type - let value := decl.value (allowNondep := true) - /- `inferType` alone would miss ill-typed arguments inside the value. - The separate comparison also checks that its type still agrees with the declaration. -/ - check value - if !(← isDefEq decl.type (← inferType value)) then - throwLetTypeMismatchMessage decl.fvarId - check body - getZetaDeltaFVarIds - return rebuild xs deps e 0 -where - rebuild (xs : Array Expr) (deps : FVarIdSet) (e : Expr) (i : Nat) : Expr := - match e with - | .letE n t v b nondep => - let b := rebuild xs deps b (i + 1) - if nondep && deps.contains xs[i]!.fvarId! then - /- Substitute throughout the scope, including types and implicit arguments. - For `have a := 0; have q : {n // n = a} := ⟨0, rfl⟩; q.val`, - changing only `q`'s type would leave the predicate argument of `q.val` unchanged. -/ - b.instantiate1 v - else - mkLet n t v b nondep - | _ => e - /-- Simplifies the suffix `e` beginning at binding `i` of the telescope described by `info`. The preceding bindings are represented by free variables in `xs` and the cached expressions in @@ -362,7 +326,8 @@ each binder does not repeatedly traverse the entire remaining body and proof. Unused values are skipped. Fixed values admit only `dsimp`; other values admit propositional rewrites. Each updated value is entered as a dependent local definition so that matcher reduction can use its value while simplifying the remainder. The simplifier cache is isolated for that -scope, and the rebuilt expression retains the original `let`/`have` flags. +scope. A changed body is rebuilt with `let`; `simpEqn` then uses `letToHave` to recover `have` +bindings where their bodies remain well typed with the variable abstract. A value rewrite is lifted with `congrArg (fun x => originalBody)`. The body proof is closed with `let x := updatedValue`, since it may rely on that value; the two proofs compose by transitivity. @@ -398,7 +363,9 @@ partial def simpEqnTelescope (info : HaveTelescopeInfo) (fixed used : Array Bool else /- The type does not depend on this binding; remove its unused bound-variable slot. -/ rb.type.lowerLooseBVars 1 1 - let expr := mkLet n t v' rb.expr nondep + /- A changed body may need the value of `x` to typecheck. Use `let` until `letToHave` + checks whether the body can still be abstracted over `x`. -/ + let expr := mkLet n t v' rb.expr (nondep && rb.expr == b) let hb? := rb.proof?.map fun h => mkLet n t v' h false let hv? := hv?.map fun h => mkApp6 (mkConst ``congrArg [hi.level, info.level]) t type v v' (mkLambda n .default t b) h @@ -459,8 +426,8 @@ def getEqnTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo := do /-- The `simp` callback for equation normalization. It handles complete binding telescopes before the default traversal, using `simpEqnTelescope` to preserve their nesting and sharing. Unused bindings -are removed afterward, and `zetaDependentHaves` unfolds bindings needed to typecheck the result. -A changed telescope is revisited: removing dependent uses can make a +are removed afterward, and `letToHave` determines which bindings can be nondependent. +A changed telescope is revisited: removing dependent uses or restoring a `have` can make a previously fixed value eligible for propositional rewriting. A stable telescope returns `.done`. For a matcher, first try definitional reduction, then its congruence equations using local @@ -475,10 +442,7 @@ partial def simpEqn : Simp.Simproc := fun e => do let r ← simpEqnTelescope info fixed used e 0 #[] let r := { expr := ← zetaUnused r.expr, proof? := r.proof? : Simp.Result } if r.expr == e then return .done r - let mut r' ← zetaDependentHaves r.expr - if r' != r.expr then - r' ← zetaUnused r' - return .visit { r with expr := r' } + return .visit { r with expr := (← letToHave r.expr) } if let some app ← matchMatcherApp? e then if let some e' ← reduceRecMatcher? e then return .visit { expr := e' } @@ -491,8 +455,8 @@ partial def simpEqn : Simp.Simproc := fun e => do The definitional counterpart of `simpEqn`, used for fixed binding values and dependent arguments that `simp` cannot rewrite propositionally. It opens a whole binding telescope, skips unused values, and definitionally simplifies the other values and body with preceding values available -as local definitions. `zetaDependentHaves` unfolds bindings needed to typecheck the result; -remaining bindings keep their original flags, and unused bindings are removed. +as local definitions. Changed bodies are rebuilt with `let`, and `letToHave` recovers `have` +bindings where possible. Unused bindings are removed. Matchers are reduced only definitionally; no congruence-equation proofs are used. Changed results are revisited, and the returned expression is definitionally equal to the input. @@ -504,10 +468,7 @@ partial def dsimpEqn : Simp.DSimproc := fun e => do let r ← Simp.withFreshCache <| visit info used e 0 #[] let r ← zetaUnused r if r == e then return .done r - let r' ← zetaDependentHaves r - if r == r' then return .visit r' - /- If some `have`-decls were inlined, some of the remaining declarations may be unused now. -/ - return .visit (← zetaUnused r') + return .visit (← letToHave r) if ← isMatcherApp e then if let some e' ← reduceRecMatcher? e then return .visit e' return .continue @@ -530,8 +491,9 @@ where we want to make sure `a` is transparent when reducing the `match`. -/ let decl := (decl.setValue value').setNondep false - let b ← withExistingLocalDecls [decl] <| visit info used b (i+1) (xs.push decl.toExpr) - return mkLet n t v' b nondep + let b' ← withExistingLocalDecls [decl] <| visit info used b (i+1) (xs.push decl.toExpr) + /- As in `simpEqnTelescope`, a changed body must be checked before retaining `have`. -/ + return mkLet n t v' b' (nondep && b' == b) else return (← Simp.dsimp info.body).abstract xs diff --git a/tests/elab/eqns_issues.lean b/tests/elab/eqns_issues.lean index b13afe9a5297..33ed20d629dc 100644 --- a/tests/elab/eqns_issues.lean +++ b/tests/elab/eqns_issues.lean @@ -3,8 +3,8 @@ module import Lean /-! -Regression tests for equation lemmas preserving shared values, nested binding scopes, and binding -kinds while splitting matches (#16122). +Regression tests for equation lemmas preserving shared values and valid nested binding scopes +while splitting matches (#16122). -/ @[expose] public section @@ -100,7 +100,7 @@ info: noCleanup.eq_1 (x : Nat) : -/ #guard_msgs in #check noCleanup.eq_1 --- A dependent binding and a nondependent `let` retain their binding kinds too. +-- An unchanged telescope does not need another `letToHave` pass. set_option cleanup.letToHave false in def noCleanupLet (x : Nat) : Nat := let y := x + 1 @@ -114,6 +114,23 @@ info: noCleanupLet.eq_1 (x : Nat) : -/ #guard_msgs in #check noCleanupLet.eq_1 +-- When normalization changes the body, an original nondependent `let` becomes a `have`. +set_option cleanup.letToHave false in +def noCleanupLetMatch (x : Nat) : Nat := + let y := x + 1 + match x with + | 0 => y + y + | n + 1 => y + y + n + +/-- +info: noCleanupLetMatch.eq_1 : + noCleanupLetMatch 0 = + have y := 0 + 1; + y + y +-/ +#guard_msgs in #check noCleanupLetMatch.eq_1 + +-- A binding whose body needs its value remains a `let`. set_option cleanup.letToHave false in def noCleanupDependent (x : Nat) : Fin 5 := let n := 4 @@ -221,8 +238,8 @@ run_meta do let some eqns ← getEqnsFor? ``fixedValue | throwError "missing equations" unless eqns.size == 1 do throwError "expected one equation, got {eqns.size}" forallTelescope (← getConstInfo eqns[0]!).type fun xs body => do - let some (_, _, .letE _ _ value _ false) := body.eq? - | throwError "dependent binding was lost" + let some (_, _, .letE _ _ value _ true) := body.eq? + | throwError "expected a nondependent binding" unless value == xs[0]! do throwError "constructor aliases in the fixed value did not reduce" example (x : Nat) : (fixedValue x).val = 0 := by diff --git a/tests/elab_bench/eqns_have_chain.lean b/tests/elab_bench/eqns_have_chain.lean index f233059ed574..7e7fec347ede 100644 --- a/tests/elab_bench/eqns_have_chain.lean +++ b/tests/elab_bench/eqns_have_chain.lean @@ -6,6 +6,8 @@ import Lean Benchmark equation generation for a match below a long chain of shared values (#16122). Every value uses the preceding value twice, so zeta expansion would be exponential. The resulting equations must retain the chain inside its original binding and have size linear in its length. +Also cover nested binding values: checking each complete value at every enclosing scope would +repeatedly traverse the same inner telescope. -/ open Lean Meta @@ -41,6 +43,22 @@ private def makeChainDefinition (n : Nat) : MetaM Name := do enableRealizationsForConst name return name +private def makeNestedDefinition (n : Nat) : MetaM Name := do + let name ← mkFreshUserName `eqnsNestedHave + let nat := mkConst ``Nat + let type ← mkArrow nat nat + let value ← withLocalDeclD `x nat fun x => do + let .lam _ _ (.lam _ _ template _) _ := (← getConstInfoDefn ``chainTail).value + | throwError "unexpected chain template" + let mut body := template.instantiateRev #[x, mkNatLit 0] + for _ in [:n] do + body := mkHave `a nat body (mkApp2 (mkConst ``combine) (mkBVar 0) (mkBVar 0)) + mkLambdaFVars #[x] body + let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) value + 1) + addDecl <| .defnDecl { name, levelParams := [], type, value, hints, safety := .safe } + enableRealizationsForConst name + return name + run_meta do let bench := (← IO.getEnv "TEST_BENCH") == some "1" for n in (if bench then [200, 400, 800] else [25]) do @@ -67,3 +85,26 @@ run_meta do throwError "expected {n + 1} nested bindings, got {count}" unless (← body.numObjs) ≤ 32 * n + 256 do throwError "equation exceeded the size bound for {n} bindings" + +run_meta do + let bench := (← IO.getEnv "TEST_BENCH") == some "1" + for n in (if bench then [200, 400, 800] else [25]) do + let name ← makeNestedDefinition n + let start ← IO.monoNanosNow + let some eqns ← getEqnsFor? name | throwError "missing equations" + let infos ← eqns.mapM getConstInfo + let stop ← IO.monoNanosNow + if bench then + IO.println s!"measurement: eqns_nested_have_{n} {(stop - start).toFloat / 1e9} s" + if eqns.size != 2 then throwError "expected two equations, got {eqns.size}" + for info in infos do + forallTelescope info.type fun _ body => do + let some (_, _, rhs) := body.eq? | throwError "expected an equation" + let mut value := rhs + let mut count := 0 + while let .letE _ _ inner _ true := value do + count := count + 1 + value := inner + if count != n then throwError "expected {n} nested bindings, got {count}" + if (← rhs.numObjs) > 32 * n + 256 then + throwError "equation exceeded the size bound for {n} bindings" From 876b91e06309ec20ced7845b5799a5dc5420aaad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2026 06:31:26 +0000 Subject: [PATCH 10/17] fix: discard impossible branches when generating equations This PR avoids duplicate equation theorems by eliminating contradictory branches after matcher refinement. Use the existing contradiction checker in Split.refineMatch to close branches whose discriminant equalities or overlap exclusions become contradictory after substitution. Add regressions for dependent bindings, constant discriminants, and quantified overlap exclusions, and update the expected trace names after removing an impossible equation. --- src/Lean/Meta/Tactic/Split.lean | 12 +++- tests/elab/eqns_have_invariant.lean | 69 +++++++++++++++++++ tests/elab/grind_ematch_gen_pattern.lean | 8 +-- ...grind_ematch_gen_pattern.lean.out.expected | 2 +- 4 files changed, 83 insertions(+), 8 deletions(-) diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index bb212162211f..85c076b5cdda 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -10,6 +10,7 @@ public import Lean.Meta.Match.MatcherApp.Basic public import Lean.Meta.Tactic.Apply public import Lean.Meta.Tactic.Generalize public import Lean.Meta.Tactic.Simp.Types +import Lean.Meta.Tactic.Contradiction import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.SplitIf @@ -316,12 +317,12 @@ matcher occurrences in the target. The arguments must be well-typed in the goal' the matcher application need not occur in the target. Computed discriminants are linked to fresh variables by equalities. After splitting, these -equalities specialize the goal where possible; unresolved conditions remain as hypotheses. -The target is not simplified. +equalities specialize the goal where possible. Contradictory branches are closed; unresolved +conditions remain as hypotheses. The target is not simplified. -/ def refineMatch (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := mvarId.withContext do - applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs => + let mvarIds ← applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs => mvarId.withContext do if ← discrs.allM fun discr => do unless discr.isFVar do return false @@ -332,6 +333,11 @@ def refineMatch (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) let (discrFVarIds, mvarId) ← mvarId.introN discrs.size let (discrEqs, mvarId) ← mvarId.introN discrs.size return (discrFVarIds, discrEqs, mvarId) + /- Substitution can expose contradictions in the generalized discriminant equalities + (e.g. `0 = n.succ`) or overlap exclusions (e.g. `0 = 0 → False`). These hypotheses + are already in the local context, so `Cases.unifyEqs?` does not process them. -/ + mvarIds.filterM fun mvarId => do + return !(← mvarId.contradictionCore { useDecide := false, emptyType := false, genDiseq := true }) def mkDiscrGenErrorMsg (e : Expr) : MessageData := m!"`split` tactic failed to generalize discriminant(s) at{indentExpr e}\nresulting expression was not type correct\npossible solution: generalize discriminant(s) manually before using `split`" diff --git a/tests/elab/eqns_have_invariant.lean b/tests/elab/eqns_have_invariant.lean index 4c03f5afeb93..6984488ec4ef 100644 --- a/tests/elab/eqns_have_invariant.lean +++ b/tests/elab/eqns_have_invariant.lean @@ -44,3 +44,72 @@ example (m : Nat) : fixedHave = 0 := by simp -zeta only [fixedHave.eq_1, ← Nat.sub_self m] simp -zeta only [Nat.sub_self] rfl + +/- The second and fourth alternatives are impossible because `a = 0`. Equation generation +must eliminate them, including the contradiction in the second alternative's overlap condition. -/ +def depMatch (x : Nat) : Nat := + have a := 0 + have q : { n : Nat // n ≤ x + a } := + match x, a with + | 0, 0 => ⟨0, by simp⟩ + | 0, a => ⟨0, by simp⟩ + | x+1, 0 => ⟨x, by simp⟩ + | x+1, a+1 => ⟨x+a, by lia⟩ + q.val + +/-- +info: depMatch.eq_1 : + depMatch 0 = + let a := 0; + have q := ⟨0, depMatch._proof_1⟩; + q.val +-/ +#guard_msgs in #check depMatch.eq_1 + +/-- +info: depMatch.eq_2 (x_3 : Nat) : + depMatch x_3.succ = + let a := 0; + have q := ⟨x_3, ⋯⟩; + q.val +-/ +#guard_msgs in #check depMatch.eq_2 + +example : depMatch 0 = 0 := depMatch.eq_1 +example (n : Nat) : depMatch (n+1) = n := depMatch.eq_2 n + +/-- error: Unknown identifier `depMatch.eq_3` -/ +#guard_msgs in #check depMatch.eq_3 + +-- Constant discriminants must eliminate impossible alternatives without any local bindings. +def constantDiscr (x : Nat) : Nat := + match x, (0 : Nat) with + | 0, 0 => 0 + | 0, _ => 0 + | n+1, 0 => n + | n+1, k+1 => n+k + +example : constantDiscr 0 = 0 := constantDiscr.eq_1 +example (n : Nat) : constantDiscr (n+1) = n := constantDiscr.eq_2 n + +/-- error: Unknown identifier `constantDiscr.eq_3` -/ +#guard_msgs in #check constantDiscr.eq_3 + +-- The impossible overlap condition quantifies over the payload of `some`. +def constructorDiscr (x : Nat) : Nat := + match x, (some 0 : Option Nat) with + | 0, some n => n + | 0, _ => 0 + | n+1, _ => n + +example : constructorDiscr 0 = 0 := constructorDiscr.eq_1 +example (n : Nat) : constructorDiscr (n+1) = n := constructorDiscr.eq_2 n + +/-- info: constructorDiscr.eq_1 : constructorDiscr 0 = 0 -/ +#guard_msgs in #check constructorDiscr.eq_1 + +/-- info: constructorDiscr.eq_2 (n : Nat) : constructorDiscr n.succ = n -/ +#guard_msgs in #check constructorDiscr.eq_2 + +/-- error: Unknown identifier `constructorDiscr.eq_3` -/ +#guard_msgs in #check constructorDiscr.eq_3 diff --git a/tests/elab/grind_ematch_gen_pattern.lean b/tests/elab/grind_ematch_gen_pattern.lean index 3b70fb8d7499..1ed5d9393111 100644 --- a/tests/elab/grind_ematch_gen_pattern.lean +++ b/tests/elab/grind_ematch_gen_pattern.lean @@ -40,7 +40,7 @@ example (a : Nat) (h : b = some a) : (b.pbind fun a h => some <| 2*a) = some (a /-- trace: [grind.ematch.instance] pbind_some': (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯) -[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a +[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a -/ #guard_msgs (trace) in example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by @@ -54,7 +54,7 @@ trace: [grind.ematch.instance] pbind_some': ∀ (h : b = some a), (b.pbind fun a (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯) [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + f b ⋯)), (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯ + f b ⋯) -[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a +[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 2 * f b ⋯)), (b.pbind fun a h => some (a + f b ⋯)) = some (a + 2 * f b ⋯ + f b ⋯) [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 3 * f b ⋯)), @@ -112,7 +112,7 @@ reset_grind_attrs% /-- trace: [grind.ematch.instance] pbind_some'': (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯) -[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a +[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a -/ #guard_msgs (trace) in example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by @@ -127,7 +127,7 @@ reset_grind_attrs% /-- trace: [grind.ematch.instance] pbind_some''': some (a + f b ⋯) = b.pbind fun a h => some (a + f b ⋯) -[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a +[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a -/ #guard_msgs (trace) in example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by diff --git a/tests/elab/grind_ematch_gen_pattern.lean.out.expected b/tests/elab/grind_ematch_gen_pattern.lean.out.expected index d6f8d7ee4d8c..41fc72d982f9 100644 --- a/tests/elab/grind_ematch_gen_pattern.lean.out.expected +++ b/tests/elab/grind_ematch_gen_pattern.lean.out.expected @@ -3,7 +3,7 @@ (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯) [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + f b ⋯)), (b.pbind fun a h => some (a + f b ⋯)) = some (a + f b ⋯ + f b ⋯) -[grind.ematch.instance] f.eq_2: f (some a) ⋯ = a +[grind.ematch.instance] f.eq_1: f (some a) ⋯ = a [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 2 * f b ⋯)), (b.pbind fun a h => some (a + f b ⋯)) = some (a + 2 * f b ⋯ + f b ⋯) [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 3 * f b ⋯)), From 354bae1055b6bf899fd1efc8077b70486022f68b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Nov 2026 06:39:57 +0000 Subject: [PATCH 11/17] test: remove equation have-chain benchmark --- tests/elab_bench/eqns_have_chain.lean | 110 -------------------------- 1 file changed, 110 deletions(-) delete mode 100644 tests/elab_bench/eqns_have_chain.lean diff --git a/tests/elab_bench/eqns_have_chain.lean b/tests/elab_bench/eqns_have_chain.lean deleted file mode 100644 index 7e7fec347ede..000000000000 --- a/tests/elab_bench/eqns_have_chain.lean +++ /dev/null @@ -1,110 +0,0 @@ -module - -import Lean - -/-! -Benchmark equation generation for a match below a long chain of shared values (#16122). -Every value uses the preceding value twice, so zeta expansion would be exponential. The resulting -equations must retain the chain inside its original binding and have size linear in its length. -Also cover nested binding values: checking each complete value at every enclosing scope would -repeatedly traverse the same inner telescope. --/ - -open Lean Meta - -set_option maxHeartbeats 400000 -set_option maxRecDepth 100000 - --- Opaque applications keep reduction costs independent of the chain's expanded size. -private opaque combine (a b : Nat) : Nat := a + b - -private def chainTail (x a : Nat) : Nat := - match x with - | 0 => a - | n + 1 => combine (combine a a) n - -private def makeChainDefinition (n : Nat) : MetaM Name := do - let name ← mkFreshUserName `eqnsHaveChain - let nat := mkConst ``Nat - let arrow ← mkArrow nat nat - let type ← mkArrow arrow arrow - let value ← withLocalDeclD `f arrow fun f => - withLocalDeclD `x nat fun x => do - let .lam _ _ (.lam _ _ template _) _ := (← getConstInfoDefn ``chainTail).value - | throwError "unexpected chain template" - let mut body := template.instantiateRev #[x, mkBVar 0] - for _ in [:n] do - body := mkLet `a nat (mkApp2 (mkConst ``combine) (mkBVar 0) (mkBVar 0)) body true - body := mkLet `a nat (mkApp f x) body true - body := mkLet `result nat body (mkApp2 (mkConst ``combine) (mkBVar 0) (mkBVar 0)) true - mkLambdaFVars #[f, x] body - let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) value + 1) - addDecl <| .defnDecl { name, levelParams := [], type, value, hints, safety := .safe } - enableRealizationsForConst name - return name - -private def makeNestedDefinition (n : Nat) : MetaM Name := do - let name ← mkFreshUserName `eqnsNestedHave - let nat := mkConst ``Nat - let type ← mkArrow nat nat - let value ← withLocalDeclD `x nat fun x => do - let .lam _ _ (.lam _ _ template _) _ := (← getConstInfoDefn ``chainTail).value - | throwError "unexpected chain template" - let mut body := template.instantiateRev #[x, mkNatLit 0] - for _ in [:n] do - body := mkHave `a nat body (mkApp2 (mkConst ``combine) (mkBVar 0) (mkBVar 0)) - mkLambdaFVars #[x] body - let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) value + 1) - addDecl <| .defnDecl { name, levelParams := [], type, value, hints, safety := .safe } - enableRealizationsForConst name - return name - -run_meta do - let bench := (← IO.getEnv "TEST_BENCH") == some "1" - for n in (if bench then [200, 400, 800] else [25]) do - let name ← makeChainDefinition n - let start ← IO.monoNanosNow - let some eqns ← getEqnsFor? name | throwError "missing equations" - let infos ← eqns.mapM getConstInfo - unless ((← getEnv).toKernelEnv.find? name).isSome do - throwError "missing definition after checking equations" - let stop ← IO.monoNanosNow - if bench then - IO.println s!"measurement: eqns_have_chain_{n} {(stop - start).toFloat / 1e9} s" - unless eqns.size == 2 do throwError "expected two equations, got {eqns.size}" - for info in infos do - forallTelescope info.type fun _ body => do - let some (_, _, .letE _ _ inner _ true) := body.eq? - | throwError "outer binding was lost" - let mut value := inner - let mut count : Nat := 0 - while let .letE _ _ _ body true := value do - count := count + 1 - value := body - unless count == n + 1 do - throwError "expected {n + 1} nested bindings, got {count}" - unless (← body.numObjs) ≤ 32 * n + 256 do - throwError "equation exceeded the size bound for {n} bindings" - -run_meta do - let bench := (← IO.getEnv "TEST_BENCH") == some "1" - for n in (if bench then [200, 400, 800] else [25]) do - let name ← makeNestedDefinition n - let start ← IO.monoNanosNow - let some eqns ← getEqnsFor? name | throwError "missing equations" - let infos ← eqns.mapM getConstInfo - let stop ← IO.monoNanosNow - if bench then - IO.println s!"measurement: eqns_nested_have_{n} {(stop - start).toFloat / 1e9} s" - if eqns.size != 2 then throwError "expected two equations, got {eqns.size}" - for info in infos do - forallTelescope info.type fun _ body => do - let some (_, _, rhs) := body.eq? | throwError "expected an equation" - let mut value := rhs - let mut count := 0 - while let .letE _ _ inner _ true := value do - count := count + 1 - value := inner - if count != n then throwError "expected {n} nested bindings, got {count}" - if (← rhs.numObjs) > 32 * n + 256 then - throwError "equation exceeded the size bound for {n} bindings" From a01a81020f9ea5b5e4c5970470fb94d978aca9b2 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 4 Nov 2026 18:12:16 +0000 Subject: [PATCH 12/17] chore: drop two docstrings in Eqns.lean --- src/Lean/Elab/PreDefinition/Eqns.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 8db25720fa56..6bafdc4fa1f2 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -604,7 +604,6 @@ structure EqnTypes where types : Array Expr deriving TypeName -/-- Computes equation statements under the definition's saved options and a fresh metavariable depth. -/ def realizeEqnTypes (key : EqnTypesKey) : MetaM EqnTypes := withEqnOptions key.declName <| withOptions (tactic.hygienic.set · false) do let target ← unfoldThmType key.declName @@ -615,10 +614,6 @@ def realizeEqnTypes (key : EqnTypesKey) : MetaM EqnTypes := mkEqnTypes key.declNames goal.mvarId! return { types } -/-- -Proves and registers one equation, removes unused parameters, and infers its definitional-equality -attribute. --/ def realizeEqn (declName name : Name) (type : Expr) : MetaM Unit := withEqnOptions declName <| withOptions (tactic.hygienic.set · false) do let info ← getConstInfoDefn declName From a2245966c1f5306a40a5cc98b1d73600d3fd0843 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 4 Nov 2026 19:41:00 +0000 Subject: [PATCH 13/17] fix: rewrite over-applied matchers in `rwMatcher` `rwMatcher` instantiated the matcher congruence equation with all arguments of the matcher application. If the matcher is applied to more arguments than its arity, the extra arguments land on the pattern variables of the equation, and the overlap hypotheses cannot be discharged. Equation generation then keeps the `match` unsplit, for example in the `@[to_dual]` translation `WithInitial.comp` of Mathlib's `WithTerminal.comp`. `rwMatcher` now rewrites the matcher application and reapplies the extra arguments. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA --- src/Lean/Meta/Match/Rewrite.lean | 9 +++++- tests/elab/eqns_over_applied_match.lean | 43 +++++++++++++++++++++++++ 2 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 tests/elab/eqns_over_applied_match.lean diff --git a/src/Lean/Meta/Match/Rewrite.lean b/src/Lean/Meta/Match/Rewrite.lean index f67678c66800..15057ee9ea8e 100644 --- a/src/Lean/Meta/Match/Rewrite.lean +++ b/src/Lean/Meta/Match/Rewrite.lean @@ -65,6 +65,8 @@ In the `onAlt` handler of a `MatcherApp.transform`, you can use this function on substituted matcher application with the alternative `altIdx`. If it fails, it returns a rewrite with `proof? := none` and the unchanged expression. +If the matcher is applied to more arguments than its arity, the rewrite applies to the matcher +application and carries the extra arguments along. "Properly substituted" here means that the discriminants have been substituted according to the alternative; otherwise, the rewrite might fail because some hypothesis of the congruence @@ -72,7 +74,7 @@ equation theorem cannot be discharged by assumption or reflixivity. See `Lean.Meta.Tactic.FunInd.buildInductionBody` and `Lean.Elab.Tactic.Do.VCGen.Split` for examples of how to coerce `MatherApp.transform` into doing the substitution on the motive for you. -/ -def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do +partial def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then let mut e := e while true do @@ -90,6 +92,11 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do trace[Meta.Match.debug] "Not a matcher application:{indentExpr e}" return { expr := e } let matcherDeclName := e.getAppFn.constName! + let some info ← getMatcherInfo? matcherDeclName | return { expr := e } + let args := e.getAppArgs + if info.arity < args.size then + let r ← rwMatcher altIdx (mkAppN e.getAppFn (args.extract 0 info.arity)) + return ← r.addExtraArgs (args.extract info.arity) let eqns ← Match.genMatchCongrEqns matcherDeclName unless altIdx < eqns.size do trace[Meta.Match.debug] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}" diff --git a/tests/elab/eqns_over_applied_match.lean b/tests/elab/eqns_over_applied_match.lean new file mode 100644 index 000000000000..5569f7f15c39 --- /dev/null +++ b/tests/elab/eqns_over_applied_match.lean @@ -0,0 +1,43 @@ +/-! +Equation lemmas split a `match` that is applied to more arguments than its arity, also when an +alternative needs an overlap hypothesis. +-/ + +def over (a b : Bool) (n : Nat) : Nat := + (match a, b with + | true, true => fun n => n + | _, _ => fun _ => 0) n + +/-- +info: over.eq_1 (n : Nat) : over true true n = n +-/ +#guard_msgs in +#check over.eq_1 + +/-- +info: over.eq_2 (a b : Bool) (n : Nat) (x_2 : a = true → b = true → False) : over a b n = (fun x => 0) n +-/ +#guard_msgs in +#check over.eq_2 + +inductive WT where + | of : Nat → WT + | star : WT + +@[reducible] def WT.Hom : WT → WT → Type + | of _, of _ => Nat + | star, of _ => PEmpty + | _, star => PUnit + +/-- The over-applied `match` that `@[to_dual]` produces for a composition of morphisms. -/ +def WT.comp {X Y Z : WT} (f : Hom X Y) (g : Hom Y Z) : Hom X Z := + (match (motive := (x y z : WT) → Hom x y → Hom y z → Hom x z) X, Y, Z with + | of _, of _, of _ => fun f g => (f + g : Nat) + | of _, _, star => fun _ _ => PUnit.unit + | star, of _, _ => fun f _ => PEmpty.elim f + | _, star, of _ => fun _ g => PEmpty.elim g + | star, star, star => fun _ _ => PUnit.unit) f g + +/-- info: WT.comp.eq_5 (f g : WT.star.Hom WT.star) : WT.comp f g = PUnit.unit -/ +#guard_msgs in +#check WT.comp.eq_5 From fb93fa87cd9b47bd70f0b4dc771d045b1812adfb Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 4 Nov 2026 21:43:06 +0000 Subject: [PATCH 14/17] fix: prove equations with matcher congruence equations `mkEqnTypes` computes an equation statement by rewriting a matcher with its congruence equation, also when the discriminants of that alternative are not constructor applications. `mkEqnProof` then cannot reduce the matcher on the left-hand side if the compiled matcher cases on such a discriminant, for example `AugmentedSimplexCategory.tensorHom` in Mathlib. `mkEqnProof` now tries the same rewrite on the left-hand side before it fails. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA --- src/Lean/Elab/PreDefinition/Eqns.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 6bafdc4fa1f2..01744df7f2a6 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -61,6 +61,25 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC -- Else use delta reduction deltaLHS mvarId +/-- +Rewrites a matcher application on the left-hand side of an equality goal with the congruence +equation of the first alternative that applies. Equation statements are computed with the same +rewrite, so it proves equations whose discriminants are not constructor applications. +-/ +def rwMatcherLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do + let target ← mvarId.getType' + let some (_, lhs, rhs) := target.eq? | return none + let some app ← matchMatcherApp? lhs | return none + for i in *...app.numAlts do + let r ← rwMatcher i lhs + if r.expr != lhs then + let targetNew ← mkEq r.expr rhs + let some proof := r.proof? | return some (← mvarId.replaceTargetDefEq targetNew) + let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew + mvarId.assign (← mkEqTrans proof mvarNew) + return some mvarNew.mvarId! + return none + /-- Proves a generated equation type for `declName`. After introducing its parameters and hypotheses, tries reflexivity, then unfolds the definition and reduces or splits the remaining cases. @@ -109,6 +128,8 @@ partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do mvarIds.forM go else if let some mvarIds ← splitTarget? mvarId (useNewSemantics := true) then mvarIds.forM go + else if let some mvarId ← rwMatcherLHS? mvarId then + go mvarId else throwError "failed to generate equational theorem for `{.ofConstName declName}`\n{MessageData.ofGoal mvarId}" From 2bf9dec1d08234b3266c26b59ffc99973154ea30 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 4 Nov 2026 22:24:00 +0000 Subject: [PATCH 15/17] test: update kernel unfolding count in ack.lean Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA --- tests/elab/ack.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/elab/ack.lean b/tests/elab/ack.lean index 63bbd96477e8..2640908b487c 100644 --- a/tests/elab/ack.lean +++ b/tests/elab/ack.lean @@ -16,8 +16,8 @@ trace: [simp] Diagnostics use `set_option diagnostics.threshold ` to control threshold for reporting counters --- trace: [diag] Diagnostics - [kernel] unfolded declarations (max: 86, num: 1): - [kernel] OfNat.ofNat ↦ 86 + [kernel] unfolded declarations (max: 91, num: 1): + [kernel] OfNat.ofNat ↦ 91 use `set_option diagnostics.threshold ` to control threshold for reporting counters -/ #guard_msgs in From 25dc542ee2e7e1fb1cc97ce91254844660ccdb3f Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 4 Nov 2026 23:57:42 +0000 Subject: [PATCH 16/17] fix: add no `congr_simp` theorems while normalizing equations `normalizeEqn` used `simp` with global congruence theorems, so computing the equation statements realized `congr_simp` theorems such as `SplitEpi.mk.congr_simp` in Mathlib. These theorems are now kept with the equation lemmas, and a module that imports them sees no proof. Mathlib's `to_dual` unfolds `congr_simp` theorems in proofs and then fails. `normalizeEqn` now builds congruence proofs in place. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA --- src/Lean/Elab/PreDefinition/Eqns.lean | 6 ++++-- tests/elab/eqns_no_congr_simp.lean | 27 +++++++++++++++++++++++++++ 2 files changed, 31 insertions(+), 2 deletions(-) create mode 100644 tests/elab/eqns_no_congr_simp.lean diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index efbaa650e6bd..7778647dc43d 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -521,14 +521,16 @@ where /-- Normalizes the RHS of an equality goal using `simpEqn` and `dsimpEqn`, preserving shared bindings. The neutral configuration disables general reductions, including zeta expansion, while `simp` -provides traversal and congruence. Propositional RHS rewrites are lifted to the whole target; +provides traversal and congruence. Congruence proofs are built in place, so normalization adds no +`congr_simp` theorems to the environment. Propositional RHS rewrites are lifted to the whole target; definitional rewrites directly replace the target. Returns the original goal when unchanged, which lets `splitMatch?` detect normalization progress. -/ def normalizeEqn (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do let target ← mvarId.getType' let some (_, lhs, rhs) := target.eq? | return mvarId - let ctx ← Simp.mkContext (config := { Simp.neutralConfig with dsimp := true, etaStruct := .none }) + let ctx ← Simp.mkContext + (config := { Simp.neutralConfig with dsimp := true, etaStruct := .none, congrConsts := false }) let methods : Simp.Methods := { pre := simpEqn dpre := dsimpEqn diff --git a/tests/elab/eqns_no_congr_simp.lean b/tests/elab/eqns_no_congr_simp.lean new file mode 100644 index 000000000000..bc1d784606cf --- /dev/null +++ b/tests/elab/eqns_no_congr_simp.lean @@ -0,0 +1,27 @@ +import Lean +open Lean Meta + +/-! +Generating equation lemmas adds no `congr_simp` theorems to the environment. A module that +imports such a theorem cannot unfold it, which breaks tools that unfold `congr_simp` theorems +in proofs, such as Mathlib's `to_dual`. +-/ + +structure S where + n : Nat + h : 0 < n + 1 + +def g (b : Bool) (m : Nat) : S := + match b with + | true => ⟨m + 0, Nat.succ_pos _⟩ + | false => ⟨0, Nat.succ_pos _⟩ + +/-- +info: [g.eq_1, g.eq_2] +--- +info: false +-/ +#guard_msgs in +run_meta do + logInfo m!"{(← getEqnsFor? ``g).getD #[]}" + logInfo m!"{(← getEnv).contains `S.mk.congr_simp}" From 93b8f4d474e8911e8ec6bbb9a98f8ac4cbe86c80 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 5 Nov 2026 00:56:15 +0000 Subject: [PATCH 17/17] fix: compute equation statements with private declarations visible MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The body of a definition with an exposed body can mention private auxiliary proofs, such as the shared `_proof_` declarations of a module, while its equation lemmas are public. `mkEqnTypes` normalizes the right-hand side with `simp`, which looks up these proofs and fails with "Unknown constant" when it runs in exporting mode, for example in Mathlib's `SSet.Truncated.liftOfStrictSegal.f₂`. `mkEqnTypes` now runs with private declarations visible. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA --- src/Lean/Elab/PreDefinition/Eqns.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 7778647dc43d..fb08fa575869 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -577,10 +577,13 @@ partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : Calculates equation statements by normalizing the initial goal, recursively splitting eligible matches, and saving terminal goals. Each recursive call receives an already-normalized RHS. The resulting statements are proved separately by `mkEqnProof`. +The body of a definition can mention private auxiliary proofs even if the equations are public, +so the statements are computed with private declarations visible. -/ -partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do - let (_, eqnTypes) ← go (← normalizeEqn mvarId) |>.run #[] - return eqnTypes +partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := + withoutExporting do + let (_, eqnTypes) ← go (← normalizeEqn mvarId) |>.run #[] + return eqnTypes where go (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := do trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"