A potential path towards a faster field_simp

Stream: mathlib4

[Yaël Dillies]

I would like to point out that #8102 is a PR which adds a tactic that could become an internal of a future reimplementation of field_simp: unify_denoms sums fractions together and collects the denominators into one.

[Yaël Dillies]

The current implementation of unify_denoms is based on rewriting, and thus suffers from a variety of issues avoided by smarter tactics, like ring. I therefore suggested reusing the ring internals to collect the denominators.

[Yaël Dillies]

Unfortunately, the PR author doesn't have the time to implement such a suggestion. But I do think it would be a very good first metaprogramming project for a beginner. Hence I have marked the PR please-adopt and good-first-issue.

[Paul Lezeau]

I’d be happy to take that up (once I’m back from holidays:))

[Kim Morrison]

The most useful thing from my point of view would be for someone to write a good test suite for the field_simps they wish existed, so we can do a clean efficient reimplementation.

[Kim Morrison]

I haven't looked at the state of the test suite for positivity, but the same may apply there.