max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: use .inj in proof of .injEq (#12164)

Browse source 
This PR uses the `.inj` theorem in the proof of one direction of the
`.injEq` theorem.
This commit is contained in:
Joachim Breitner 2026-01-26 15:50:32 +01:00 • committed by GitHub
parent b44c7e161c
commit a6a3df8af0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Meta/Injective.lean
View file

@ -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