Lean4
/-- `try_rfl mvs` takes as input a list of `MVarId`s, scans them partitioning them into two
lists: the goals containing some metavariables and the goals not containing any metavariable.
If a goal containing a metavariable has the form `?_ = x`, `x = ?_`, where `?_` is a metavariable
and `x` is an expression that does not involve metavariables, then it closes this goal using `rfl`,
effectively assigning the metavariable to `x`.
If a goal does not contain metavariables, it tries `rfl` on it.
It returns the list of `MVarId`s, beginning with the ones that initially involved (`Expr`)
metavariables followed by the rest.
-/
def try_rfl (mvs : List MVarId) : MetaM (List MVarId) := do
let (yesMV, noMV) := ← mvs.partitionM fun mv => return hasExprMVar (← instantiateMVars (← mv.getDecl).type)
let tried_rfl := ← noMV.mapM fun g => g.applyConst ``rfl <|> return [g]
let assignable :=
←
yesMV.mapM fun g => do
let tgt := ← instantiateMVars (← g.getDecl).type
match tgt.eq? with
| some (_, lhs, rhs) =>
if (isMVar rhs && (!hasExprMVar lhs)) || (isMVar lhs && (!hasExprMVar rhs)) then
g.applyConst ``rfl
else
pure [g]
| none =>
return [g]
return (assignable.flatten ++ tried_rfl.flatten)
