Lean4
/-- `miscomputedDegree? deg false_goals` takes as input
* an `Expr`ession `deg`, representing the degree of a polynomial
(i.e. an `Expr`ession of inferred type either `ℕ` or `WithBot ℕ`);
* a list of `MVarId`s `false_goals`.
Although inconsequential for this function, the list of goals `false_goals` reduces to `False`
if `norm_num`med.
`miscomputedDegree?` extracts error information from goals of the form
* `a ≠ b`, assuming it comes from `⊢ coeff_of_given_degree ≠ 0`
--- reducing to `False` means that the coefficient that was supposed to vanish, does not;
* `a ≤ b`, assuming it comes from `⊢ degree_of_subterm ≤ degree_of_polynomial`
--- reducing to `False` means that there is a term of degree that is apparently too large;
* `a = b`, assuming it comes from `⊢ computed_degree ≤ given_degree`
--- reducing to `False` means that there is a term of degree that is apparently too large.
The cases `a ≠ b` and `a = b` are not a perfect match with the top coefficient:
reducing to `False` is not exactly correlated with a coefficient being non-zero.
It does mean that `compute_degree` reduced the initial goal to an unprovable state
(unless there was already a contradiction in the initial hypotheses!), but it is indicative that
there may be some problem.
-/
def miscomputedDegree? (deg : Expr) : List Expr → List MessageData
| tgt :: tgts =>
let rest := miscomputedDegree? deg tgts
if tgt.ne?.isSome then (m! "* the coefficient of degree {deg} may be zero") :: rest
else
if let some ((Expr.const ``Nat []), lhs, _) := tgt.le? then
(m! "* there is at least one term of naïve degree {lhs}") :: rest
else if let some (_, lhs, _) := tgt.eq? then (m! "* there may be a term of naïve degree {lhs}") :: rest else rest
| [] => []
