[Merged by Bors] - feat(tactic/cancel_denoms): try to remove numeral denominators

[robertylewis]

---

This is another linarith preprocessing step that I've factored out.

variables {α : Type} [linear_ordered_field α] (a b c d : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c :=
begin
  cancel_denoms at h,
  exact h
end

example (h : a > 0) : a / 5 > 0 :=
begin
  cancel_denoms,
  exact h
end

This tactic is not particularly refined. I think it's only mildly useful as a standalone thing, and linarith doesn't care much about its output being clean. But it can occasionally be convenient. Improving the standalone version would be a good project for someone learning metaprogramming -- maybe not as a first tactic, but as a second or third.

[jcommelin]

How is this related to field_simp? I guess there is a certain overlap. Should field_simp call this tactic?

[robertylewis]

field_simp doesn't solve either example in my first post, and cancel_denoms will certainly fail most/all of the field_simp tests. My instinct is that they serve different purposes and should be kept separate. If people turn out to use them both together in practice, we could reconsider.

[bryangingechen]

Is the difference between this and field_simp that field_simp can only cancel denominators on equalities? Someone looking for field_simp might find cancel_denoms instead (or vice versa), so maybe they should be mentioned in each other's doc strings / tactic docs.

[robertylewis]

I've pushed an addition to the docs to try to clarify the relation with field_simp.

[bryangingechen]

bors r+

[bryangingechen]

bors r-

[bors]

Canceled.

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Build mathlib
• Run tests and docs