Zulip Chat Archive

Stream: maths

Topic: clear_denominator


view this post on Zulip Patrick Massot (May 30 2018 at 11:54):

Let's start a new thread about this

view this post on Zulip Patrick Massot (May 30 2018 at 11:55):

It's a dream about a tactic called clear_denominator

view this post on Zulip Patrick Massot (May 30 2018 at 11:55):

Assume the current goal is either an equality or an inequality

view this post on Zulip Patrick Massot (May 30 2018 at 11:57):

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

view this post on Zulip Patrick Massot (May 30 2018 at 11:57):

we want to get rid of all divisions

view this post on Zulip 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 /)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 30 2018 at 12:00):

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

view this post on Zulip Patrick Massot (May 30 2018 at 12:01):

Of course nested divisions would be problematic

view this post on Zulip Patrick Massot (May 30 2018 at 12:01):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 30 2018 at 12:25):

Indeed signs matter in inequalities

view this post on Zulip 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)

view this post on Zulip 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