Lean4
/-- Like `Lean.MVarId.congr?` but instead of using only the congruence lemma associated to the LHS,
it tries the RHS too, in the order specified by `config.preferLHS`.
It uses `Lean.Meta.mkCongrSimp?` to generate a congruence lemma, like in the `congr` tactic.
Applies the congruence generated congruence lemmas according to `config`.
-/
def congrSimp? (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
mvarId.withContext
(do
mvarId.checkNotAssigned `congrSimp?
let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? |
return none
let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs)
if let some mvars← forSide mvarId fst then
return mvars
else if let some mvars← forSide mvarId snd then
return mvars
else
return none)
where
forSide (mvarId : MVarId) (side : Expr) : MetaM (Option (List MVarId)) :=
commitWhenSome?
(do
let side := side.cleanupAnnotations
if not side.isApp then
return none
let numArgs := config.maxArgsFor side.getAppNumArgs
if not config.partialApp && numArgs < side.getAppNumArgs then
return none
let mut f := side
for _ in [:numArgs]do
f := f.appFn!'
let some congrThm ← mkCongrSimpNArgs f numArgs |
return none
observing? <| applyCongrThm? config mvarId congrThm.type congrThm.proof)
/-- Like `mkCongrSimp?` but takes in a specific arity. -/
mkCongrSimpNArgs (f : Expr) (nArgs : Nat) : MetaM (Option CongrTheorem) := do
let f := (← Lean.instantiateMVars f).cleanupAnnotations
let info ← getFunInfoNArgs f nArgs
mkCongrSimpCore? f info (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := false)
