## Stream: maths

### Topic: clear_denominator

#### Patrick Massot (May 30 2018 at 11:55):

It's a dream about a tactic called clear_denominator

#### Patrick Massot (May 30 2018 at 11:55):

Assume the current goal is either an equality or an inequality

#### Patrick Massot (May 30 2018 at 11:57):

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

#### Patrick Massot (May 30 2018 at 11:57):

we want to get rid of all divisions

#### Patrick Massot (May 30 2018 at 11:57):

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

#### Patrick Massot (May 30 2018 at 11:59):

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 (May 30 2018 at 12:00):

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

#### Patrick Massot (May 30 2018 at 12:00):

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

#### Patrick Massot (May 30 2018 at 12:01):

Of course nested divisions would be problematic

#### Patrick Massot (May 30 2018 at 12:01):

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

#### Assia Mahboubi (May 30 2018 at 12:06):

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 (May 30 2018 at 12:25):

Indeed signs matter in inequalities

#### Patrick Massot (May 30 2018 at 12:25):

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

#### Assia Mahboubi (May 30 2018 at 13:14):

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).

Last updated: May 10 2021 at 07:15 UTC