From c17c4598bc615555d231b6d8af4fdf505fd68f99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 7 May 2026 11:31:48 +0100 Subject: [PATCH] chore: refactor the usages of `Meta.mkCongrArg` with `SymM` primitives in `cbv` (#13665) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR replaces `Meta.mkCongrArg` call sites in `handleProj` and `simplifyAppFn` are replaced with direct `congrArg` constructions that reuse types already in the `Sym` pointer cache. A few stray unqualified `inferType` / `getLevel` / `isDefEq` calls in the same file are also routed through the cached `Sym` equivalents. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) --- src/Lean/Meta/Tactic/Cbv/Main.lean | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index 8d332cb215..e032ed16ab 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -259,10 +259,13 @@ def handleProj : Simproc := fun e => do | .step e' proof _ _ => let type ← Sym.inferType e' let congrArgFun := Lean.mkLambda `x .default type <| .proj typeName idx <| .bvar 0 - let congrArgFunType ← inferType congrArgFun + let congrArgFunType ← Sym.inferType congrArgFun -- If the type of a projection function is non-dependent, we can safely prove `e.i = e'.i` from `e = e'` - if (congrArgFunType.isArrow) then - let newProof ← mkCongrArg congrArgFun proof + if congrArgFunType.isArrow then + let .forallE _ α β _ := congrArgFunType | unreachable! + let u ← Sym.getLevel α + let v ← Sym.getLevel β + let newProof := mkApp6 (mkConst ``congrArg [u, v]) α β struct e' congrArgFun proof return .step (← Lean.Expr.updateProjS! e e') newProof else -- If the type of the projection function is dependent, we first try to reduce the projection @@ -273,7 +276,7 @@ def handleProj : Simproc := fun e => do return .step reduced (← Sym.mkEqRefl reduced) | .none => -- If we failed to reduce it, we turn to a last resort; we try use heterogeneous congruence lemma that we then try to turn into an equality. - unless (← isDefEq struct e') do + unless (← Sym.isDefEqI struct e') do -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do. -- TODO: Check if there is a need to report this to a user, or shall we fail silently. return .rfl (done := true) @@ -301,7 +304,10 @@ def simplifyAppFn : Simproc := fun e => do let newType ← Sym.inferType e' let congrArgFun := Lean.mkLambda `x .default newType (mkAppN (.bvar 0) e.getAppArgs) let newValue ← mkAppNS e' e.getAppArgs - let newProof ← mkCongrArg congrArgFun proof + let resultType ← Sym.inferType e + let u ← Sym.getLevel newType + let v ← Sym.getLevel resultType + let newProof := mkApp6 (mkConst ``congrArg [u, v]) newType resultType fn e' congrArgFun proof trace[Debug.Meta.Tactic.cbv.reduce] "simplifyAppFn:{indentExpr e}\n==>{indentExpr newValue}" return .step newValue newProof @@ -405,11 +411,11 @@ public def cbvGoal (mvarId : MVarId) (simplifyTarget : Bool := true) (fvarIdsToS | .rfl _ _ => pure () | .step type' proof _ _ => if type'.isFalse then - let u ← getLevel type + let u ← Sym.getLevel type mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkApp4 (mkConst ``Eq.mp [u]) type type' proof (mkFVar fvarId))) return none else - let u ← getLevel type + let u ← Sym.getLevel type toAssert := toAssert.push { userName := localDecl.userName, type := type', value := mkApp4 (mkConst ``Eq.mp [u]) type type' proof (mkFVar fvarId) } -- Process target if simplifyTarget then