Lean4
/-- `splitApply mvs static` takes two lists of `MVarId`s. The first list, `mvs`,
corresponds to goals that are potentially within the scope of `compute_degree`:
namely, goals of the form
`natDegree f ≤ d`, `degree f ≤ d`, `natDegree f = d`, `degree f = d`, `coeff f d = r`.
`splitApply` determines which of these goals are actually within the scope, it applies the relevant
lemma and returns two lists: the left-over goals of all the applications, followed by the
concatenation of the previous `static` list, followed by the newly discovered goals outside of the
scope of `compute_degree`. -/
def splitApply (mvs static : List MVarId) : MetaM ((List MVarId) × (List MVarId)) := do
let (can_progress, curr_static) :=
←
mvs.partitionM fun mv => do
return dispatchLemma (twoHeadsArgs (← mv.getType'')) != ``id
let progress :=
←
can_progress.mapM fun mv => do
let lem := dispatchLemma <| twoHeadsArgs (← mv.getType'')
mv.applyConst <| lem
return (progress.flatten, static ++ curr_static)
