Is there a field_simp variant that generates hypotheses?

Stream: Is there code for X?

[Terence Tao]

In order for field_simp to simplify a hypothesis a/c = b/c to a=b, it requires an existing hypothesis that c \neq 0. Is there a version of field_simp that will go ahead and make these simplifications anyway, and add any missing hypothesis of the form c \neq 0 as an additional goal?

[Sebastien Gouezel]

No, we don't have that. A crude version to fake this is

  have : c ≠ 0; swap

This adds a new goal that c is nonzero, and then puts it at the end of the goals list. Of course, if your idea was to avoid writing c in the first place, it's not a good solution, and in any case once you're stating have : c ≠ 0, you might as well prove it right away.

[Heather Macbeth]

It could be nice to have intermediate behaviours, too. I wonder if one could design a convenient syntax to specify which out of the not-verified-nonzero denominators should be multiplied through (with a goal of their nonzeroness generated), and which should be kept as denominators.

[Adam Topaz]

We should probably also just have a field_simp! that forcibly clears all denominators introducing goals as needed.

[Heather Macbeth]

One option could be a totally opaque syntax (field_simp 2 3 7 indicating which denominators to multiply out, for a well-defined numbering of the denominators which the user isn't expected to be able to predict) together with a widget like @Patrick Massot 's congr widget to generate this tactic call, selecting the desired denominators by clicking on them.

[Adam Topaz]

the docstring for field_simp says that there is a cancel_denoms tactic, but I've never used it. Has it been ported?

[Adam Topaz]

oh sorry that's for numerical denominators

[Eric Wieser]

Heather Macbeth said:

One option could be a totally opaque syntax (field_simp 2 3 7 indicating which denominators to multiply out, for a well-defined numbering of the denominators which the user isn't expected to be able to predict) together with a widget like Patrick Massot 's congr widget to generate this tactic call, selecting the desired denominators by clicking on them.

The widget indeed makes this easy to write, but this sounds unpleasant to maintain if a proof changes slightly

[Kevin Buzzard]

Perhaps then the tactic should just consume the terms corresponding to the nonzero denominators themselves?

[Terence Tao]

Kevin Buzzard said:

Perhaps then the tactic should just consume the terms corresponding to the nonzero denominators themselves?

If the tactic could also clear denominators in inequalities, adding a hypothesis that the denominators are positive, that would also be convenient. I've had to do this a couple times now when proving inequalities and can hack things out using some combination of gcongr, mul_le_mul, apply_fun, and rewriting the left and right-hand sides using equalities proven byfield_simp, but it would be nice to have an automated tool that does all of this for you.

[Heather Macbeth]

At some point I experimented with adding docs#div_le_div_iff and docs#div_lt_div_iff to the basic field_simp simp-set (which would allow ⊢ A/B ≤ C/D to be converted to ⊢ AD ≤ BC), and it seemed to work without problems. If someone wanted to try this out on the scale of all of mathlib, it's possible that it would Just Work™.

[Kevin Buzzard]

@Terence Tao can I interest you in learning how to write lean tactics? :-)

[Heather Macbeth]

If you want to try this out yourself, you can write attribute [local field_simps] div_le_div_iff div_lt_div_iff at the top of a file.

example {a b x : ℝ} (h : a + 1 ≤ b) : a / (x ^ 2 + 3) ≤ (b - 1) / (x ^ 2 + 3) := by
  field_simp -- does nothing
  sorry

attribute [local field_simps] div_le_div_iff div_lt_div_iff

example {a b x : ℝ} (h : a + 1 ≤ b) : a / (x ^ 2 + 3) ≤ (b - 1) / (x ^ 2 + 3) := by
  field_simp
  linarith

[Terence Tao]

Heather Macbeth said:

If you want to try this out yourself, you can write attribute [local field_simps] div_le_div_iff div_lt_div_iff at the top of a file.

Thanks, this helps, though still it doesn't handle all the use cases I'm seeing. For instance, in

attribute [local field_simps] div_le_div_iff div_lt_div_iff div_le_iff'

example (x y z w : ℝ) (h: x ≠ 0) (h2: y ≠ 0) (h3: x * z / (x * y) ≤ w ) : z / y ≤ w := by
   convert h3 using 1
   field_simp
   ring

I would ideally like to apply field_simp to h3 directly, but it doesn't want to clear denominators on an inequality at all. Could this also be solved through attribute [local field_simps]?

[Heather Macbeth]

That's a good (hard) example. Since the sign of x is unknown (it's nonzero but could be positive or negative), one really needs field_simp to cancel the x * z / (x * y) down to z / y before proceeding further. This is a feature of field_simp which I've seen before: it sometimes multiplies through by more factors than necessary.

It seems like this is already hard in the equality case: note the extra apply mul_left_cancel₀ h line:

import Mathlib.Data.Real.Basic

example (x y z w : ℝ) (h: x ≠ 0) (h2: y ≠ 0) (h3: x * z / (x * y) = w ) : z / y = w := by
  field_simp at h3 ⊢
  apply mul_left_cancel₀ h
  linarith

I guess this means that the "targeted simp-set" approach is not a complete solution for the problem field_simp tries to solve, just a heuristic that works in common cases.

[Heather Macbeth]

Heather Macbeth said:

If you want to try this out yourself, you can write attribute [local field_simps] div_le_div_iff div_lt_div_iff at the top of a file.

(by the way, going back to the quick and dirty version,

attribute [local field_simps] div_le_iff le_div_iff div_lt_iff lt_div_iff

might be a bit more powerful than my first suggestion.)