Lean4
/-- Synthesize arguments `xs` either with typeclass synthesis, with `fun_prop` or with
discharger. -/
def synthesizeArgs (thmId : Origin) (xs : Array Expr) (funProp : Expr → FunPropM (Option Result)) : FunPropM Bool := do
let mut postponed : Array Expr := #[]
for x in xs do
let type ← inferType x
if (← instantiateMVars x).isMVar then
-- try type class
if (← isClass? type).isSome then
if (← synthesizeInstance thmId x type) then
continue
else if (← isFunProp type.getForallBody) then
-- try function property
if let some ⟨proof⟩← funProp type then
if (← isDefEq x proof) then
continue
else
do
trace[Meta.Tactic.fun_prop]"{(← ppOrigin thmId)}, failed to assign proof{indentExpr type}"
return false
else
-- try user provided discharger
let ctx : Context ← read
if (← isProp type) then
if let some proof← ctx.disch type then
if (← isDefEq x proof) then
continue
else
do
trace[Meta.Tactic.fun_prop]"{(← ppOrigin thmId)}, failed to assign proof{indentExpr type}"
return false
else
logError
s!"Failed to prove necessary assumption `{(← ppExpr type)}` \
when applying theorem `{← ppOrigin' thmId}`."
if ¬(← isProp type) then
postponed := postponed.push x
continue
else
trace[Meta.Tactic.fun_prop]"{(← ppOrigin thmId)}, failed to discharge hypotheses{indentExpr type}"
return false
for x in postponed do
if (← instantiateMVars x).isMVar then
logError
s!"Failed to infer `({(← ppExpr x)} : {(← ppExpr (← inferType x))})` \
when applying theorem `{← ppOrigin' thmId}`."
trace[Meta.Tactic.fun_prop]"{(← ppOrigin thmId)}, failed to infer `({(← ppExpr x)} : {← ppExpr (← inferType x)})`"
return false
return true
