Lean4
/-- `twoHeadsArgs e` takes an `Expr`ession `e` as input and recurses into `e` to make sure
that `e` looks like `lhs ≤ rhs`, `lhs < rhs` or `lhs = rhs` and that `lhs` is one of
`natDegree f, degree f, coeff f d`.
It returns
* the function being applied on the LHS (`natDegree`, `degree`, or `coeff`),
or else `.anonymous` if it's none of these;
* the name of the relation (`Eq`, `LE.le` or `LT.lt`), or else `.anonymous` if it's none of these;
* either
* `.inl zero`, `.inl one`, or `.inl many` if the polynomial in a numeral;
* or `.inr` of the head symbol of `f`;
* or `.inl .anonymous` if inapplicable;
* if it exists, whether the `rhs` is a metavariable;
* if the LHS is `coeff f d`, whether `d` is a metavariable.
This is all the data needed to figure out whether `compute_degree` can make progress on `e`
and, if so, which lemma it should apply.
Sample outputs:
* `natDegree (f + g) ≤ d => (natDegree, LE.le, HAdd.hAdd, d.isMVar, none)` (similarly for `=`);
* `degree (f * g) = d => (degree, Eq, HMul.hMul, d.isMVar, none)` (similarly for `≤`);
* `coeff (1 : ℕ[X]) c = x => (coeff, Eq, one, x.isMVar, c.isMVar)` (no `≤` option!).
-/
def twoHeadsArgs (e : Expr) : Name × Name × (Name ⊕ Name) × List Bool :=
Id.run
(do
let (eq_or_le, lhs, rhs) ←
match e.getAppFnArgs with
| (na@``Eq, #[_, lhs, rhs]) =>
pure (na, lhs, rhs)
| (na@``LE.le, #[_, _, lhs, rhs]) =>
pure (na, lhs, rhs)
| (na@``LT.lt, #[_, _, lhs, rhs]) =>
pure (na, lhs, rhs)
| _ =>
return (.anonymous, .anonymous, .inl .anonymous, [])
let (ndeg_or_deg_or_coeff, pol, and?) ←
match lhs.getAppFnArgs with
| (na@``Polynomial.natDegree, #[_, _, pol]) =>
(na, pol, [rhs.isMVar])
| (na@``Polynomial.degree, #[_, _, pol]) =>
(na, pol, [rhs.isMVar])
| (na@``Polynomial.coeff, #[_, _, pol, c]) =>
(na, pol, [rhs.isMVar, c.isMVar])
| _ =>
return (.anonymous, eq_or_le, .inl .anonymous, [])
let head :=
match pol.numeral? with
-- can I avoid the tri-splitting `n = 0`, `n = 1`, and generic `n`?
| some 0 => .inl `zero
| some 1 => .inl `one
| some _ => .inl `many
| none =>
match pol.getAppFnArgs with
| (``DFunLike.coe, #[_, _, _, _, polFun, _]) =>
let na := polFun.getAppFn.constName
if na ∈ [``Polynomial.monomial, ``Polynomial.C] then .inr na else .inl .anonymous
| (na, _) => .inr na
(ndeg_or_deg_or_coeff, eq_or_le, head, and?))
