clear_denominator

Stream: maths

[Patrick Massot]

Let's start a new thread about this

[Patrick Massot]

It's a dream about a tactic called clear_denominator

[Patrick Massot]

Assume the current goal is either an equality or an inequality

[Patrick Massot]

It has a bunch of +, -, *, /, maybe • (scalar multiplication)

[Patrick Massot]

we want to get rid of all divisions

[Patrick Massot]

the tactic walks through the goal and builds a list of all denominators (right-hand argument of a /)

[Patrick Massot]

It creates sub-goals x ≠ 0 for all denominators x, and immediately tries to discharge them by assumption or applying ne_of_gt or ne_of_lt to all assumptions

[Patrick Massot]

then it multiplies both sides of the goal by the product of all denominators, using the relevant lemmas (assuming the subgoals)

[Patrick Massot]

and then simplifies the goal to get rid of divisions by using x/x = 1

[Patrick Massot]

Of course nested divisions would be problematic

[Patrick Massot]

The Cauchy-Schwarz thread is an example where you could use this

[Assia Mahboubi]

The inequality case is more difficult because of sign conditions, isn't it? But even in the equality case, the size of the formula to be proved can become quite large. Coq has a field tactic, built on top of ring, that does about the same thing as what you describe I think.

[Patrick Massot]

Indeed signs matter in inequalities

[Patrick Massot]

And we clearly need this field tactic (but Mario always want us to suffer instead of using automation)

[Assia Mahboubi]

The field problem is more difficult than the ring one. It probably has to start as a partial procedure, like the one you describe, because a complete one is much more delicate from an algorithmic point of view (you need stuff like subresultants or even may be probabilistic methods otherwise the complexity and growth of the polynomials are dreadful).