Noisy `unusedSimpArgs` linter with `field` simproc

The field simproc has an internal simp call to discharge nonzeroness goals. It shares a simp-context with the ambient simp (the simp which called the simproc), but it doesn't share tracking of the simp-lemmas used.

This means:

• The query simp? [field, ...] may not work: if it fails, the simp trace needs to be manually inspected to find the simp-lemmas being called by the discharger;
• In a proof with a simp [field, ...] call, the unusedSimpArgs linter may be noisy, because it can incorrectly report simp-lemmas as not being used (when in fact they're used in the discharger).

The discarding of the "simp-lemma memory" occurs when the discharger's internal simp call (which is naturally in SimpM) gets packaged as a MetaM program, the discharger type for the core field(_simp) methods (reduceExpr and reduceEq).

In principle this could be fixed by having reduceExpr and reduceEq take dischargers which live in SimpM (rather than MetaM). However, I personally think the long-term plan for the field(_simp) discharger should be get rid of the simp call inside that discharger. Given that, it doesn't make sense to refactor the field_simp code to be SimpM-friendly in the short term.

(The reason we currently include a simp call in the discharger is that it gives a cheap approximation to positivity's nonzeroness-proving in fields without a partial order.)

TL;DR This issue records the behaviour, but we do not want to fix it directly. Hopefully a future refactor will render it moot.

Start by reading the core field(_simp) discharger methods, reduceExpr and reduceEq, and trace how their MetaM dischargers interact with SimpM tracking. Compare the simp? query and unusedSimpArgs behavior described here; no standalone fix is defined, since the issue expects a future discharger refactor to make the behavior moot.