Lean4
/-- This is like `Lean.MVarId.hcongr?` but (1) looks at both sides when generating the congruence lemma
and (2) inserts additional hypotheses from equalities from previous arguments.
It uses `Lean.Meta.mkRichHCongr` to generate the congruence lemmas.
If the goal is an `Eq`, it uses `eq_of_heq` first.
As a backup strategy, it uses the LHS/RHS method like in `Lean.MVarId.congrSimp?`
(where `Congr!.Config.preferLHS` determines which side to try first). This uses a particular side
of the target, generates the congruence lemma, then tries applying it. This can make progress
with higher transparency settings. To help the unifier, in this mode it assumes both sides have the
exact same function.
-/
partial def smartHCongr? (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
mvarId.withContext do
mvarId.checkNotAssigned `congr!
commitWhenSome?
(do
let mvarId ← mvarId.eqOfHEq
let some (_, lhs, _, rhs) := (← withReducible mvarId.getType').heq? |
return none
if let some mvars← loop mvarId 0 lhs rhs [] [] then
return mvars
trace[congr!]"Default smartHCongr? failed, trying LHS/RHS method"
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
loop (mvarId : MVarId) (numArgs : Nat) (lhs rhs : Expr) (lhsArgs rhsArgs : List Expr) :
MetaM (Option (List MVarId)) :=
match lhs.cleanupAnnotations, rhs.cleanupAnnotations with
| .app f a, .app f' b => do
if not (config.numArgsOk (numArgs + 1)) then
return none
let lhsArgs' := a :: lhsArgs
let rhsArgs' := b :: rhsArgs
if let some mvars← loop mvarId (numArgs + 1) f f' lhsArgs' rhsArgs' then
return mvars
if not config.partialApp && f.isApp && f'.isApp then
-- It's a partial application on both sides though.
return none
unless ← withNewMCtxDepth <| isDefEq (← inferType f) (← inferType f') do
return none
let funDefEq ← withReducible <| withNewMCtxDepth <| isDefEq f f'
if config.sameFun && not funDefEq then
return none
let info ← getFunInfoNArgs f (numArgs + 1)
let mut fixed : Array Bool := #[]
for larg in lhsArgs', rarg in rhsArgs', pinfo in info.paramInfo do
if !config.typeEqs && (!pinfo.isExplicit || pinfo.hasFwdDeps) then
-- When `typeEqs = false` then for non-explicit arguments or
-- arguments with forward dependencies, we want type arguments
-- to be plausibly equal.
if ← isType larg then
-- ^ since `f` and `f'` have defeq types, this implies `isType rarg`.
unless ← Congr!.plausiblyEqualTypes larg rarg do
fixed := fixed.push true
continue
fixed := fixed.push (← withReducible <| withNewMCtxDepth <| isDefEq larg rarg)
let cthm ←
mkRichHCongr (forceHEq := true) (← inferType f) info (fixedFun := funDefEq) (fixedParams := fixed)
-- Now see if the congruence theorem actually applies in this situation by applying it!
let (congrThm', congrProof') :=
if funDefEq then (cthm.type.bindingBody!.instantiate1 f, cthm.proof.beta #[f])
else (cthm.type.bindingBody!.bindingBody!.instantiateRev #[f, f'], cthm.proof.beta #[f, f'])
observing? <| applyCongrThm? config mvarId congrThm' congrProof'
| _, _ => return none
forSide (mvarId : MVarId) (side : Expr) : MetaM (Option (List MVarId)) := 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 info ← getFunInfoNArgs f numArgs
let mut fixed : Array Bool := #[]
if !config.typeEqs then
-- We need some strategy for fixed parameters to keep `forSide` from applying
-- in cases where `Congr!.possiblyEqualTypes` suggested not to in the previous pass.
for pinfo in info.paramInfo, arg in side.getAppArgs do
if pinfo.isProp || !(← isType arg) then
fixed := fixed.push false
else if pinfo.isExplicit && !pinfo.hasFwdDeps then
-- It's fine generating equalities for explicit type arguments without forward
-- dependencies. Only allowing these is a little strict, because an argument
-- might be something like `Fin n`. We might consider being able to generate
-- congruence lemmas that only allow equalities where they can plausibly go,
-- but that would take looking at a whole application tree.
fixed := fixed.push false
else
fixed := fixed.push true
let cthm ← mkRichHCongr (forceHEq := true) (← inferType f) info (fixedFun := true) (fixedParams := fixed)
let congrThm' := cthm.type.bindingBody!.instantiate1 f
let congrProof' := cthm.proof.beta #[f]
observing? <| applyCongrThm? config mvarId congrThm' congrProof'
