Lean4
/-- Try applying user-provided congruence lemmas. If any are applicable,
returns a list of new goals.
Tries a congruence lemma associated to the LHS and then, if that failed, the RHS.
-/
def userCongr? (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
mvarId.withContext
(do
mvarId.checkNotAssigned `userCongr?
let some (lhs, rhs) := (← withReducible mvarId.getType').eqOrIff? |
return none
let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs)
if let some mvars← forSide fst then
return mvars
else if let some mvars← forSide snd then
return mvars
else
return none)
where forSide (side : Expr) : MetaM (Option (List MVarId)) := do
let side := side.cleanupAnnotations
if not side.isApp then
return none
let some name := side.getAppFn.constName? |
return none
let congrTheorems := (← getSimpCongrTheorems).get name
for congrTheorem in congrTheorems do
let res ←
observing? do
let cinfo ← getConstInfo congrTheorem.theoremName
let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
let proof := mkConst congrTheorem.theoremName us
let ptype ← instantiateTypeLevelParams cinfo.toConstantVal us
applyCongrThm? config mvarId ptype proof
if let some mvars := res then
return mvars
return none
