From a6a3df8af0d42d98a1c0ea26a3ff613ee6ca1d14 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 26 Jan 2026 15:50:32 +0100 Subject: [PATCH] perf: use `.inj` in proof of `.injEq` (#12164) This PR uses the `.inj` theorem in the proof of one direction of the `.injEq` theorem. --- src/Lean/Meta/Injective.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean index fb3af291ab..6b6cc7b1c8 100644 --- a/src/Lean/Meta/Injective.lean +++ b/src/Lean/Meta/Injective.lean @@ -139,13 +139,14 @@ private partial def andProjections (e : Expr) : MetaM (Array Expr) := do return acc.push e go e (← inferType e) #[] -private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := do +private def mkInjectiveEqTheoremValue (ctorVal : ConstructorVal) (targetType : Expr) : MetaM Expr := do forallTelescopeReducing targetType fun xs type => do let mvar ← mkFreshExprSyntheticOpaqueMVar type let [mvarId₁, mvarId₂] ← mvar.mvarId!.apply (mkConst ``Eq.propIntro) - | throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorName}`" - let (h, mvarId₁) ← mvarId₁.intro1 - solveEqOfCtorEq ctorName mvarId₁ h + | throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorVal.name}`" + let injPrf := mkConst (mkInjectiveTheoremNameFor ctorVal.name) (ctorVal.levelParams.map mkLevelParam) + let injPrf := mkAppN injPrf xs + mvarId₁.assign injPrf let mut mvarId₂ := mvarId₂ while true do let t ← mvarId₂.getType @@ -158,7 +159,7 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me | _ => pure () let (h, mvarId₂') ← mvarId₂.intro1 (_, mvarId₂) ← substEq mvarId₂' h - try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorName) + try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorVal.name) mkLambdaFVars xs mvar private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do @@ -167,7 +168,7 @@ private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do let some type ← mkInjectiveEqTheoremType? ctorVal | return () trace[Meta.injective] "type: {type}" - let value ← mkInjectiveEqTheoremValue ctorVal.name type + let value ← mkInjectiveEqTheoremValue ctorVal type addDecl <| Declaration.thmDecl { name levelParams := ctorVal.levelParams