field_simp weirdness

Stream: mathlib4

[Michael Stoll]

Compare

import Mathlib.Tactic.FieldSimp

variable {F} [Field F]

example (a b c : F) (h : c ≠ 0) (h' : a = b) : -a / c = -c⁻¹ * b := by
  field_simp -- ⊢ a = b
  sorry

with

import Mathlib.Tactic.FieldSimp
import Mathlib.Algebra.Field.Basic -- extra import

variable {F} [Field F]

example (a b c : F) (h : c ≠ 0) (h' : a = b) : -a / c = -c⁻¹ * b := by
  field_simp -- ⊢ a = b ∨ c = 0
  sorry

A possible difference: in the first case #synth NoZeroDivisors F says GroupWithZero.noZeroDivisors, but in the second case, it is IsDomain.to_noZeroDivisors F. Still, it is completely unclear to me how this difference would affect field_simp. In any case, I would think that the second behavior does not conform to specifications.

[Yury G. Kudryashov]

Unfortunately, field_simp generates code with lots of "aux" lemmas from other files which makes it harder to inspect it.

[Mario Carneiro]

those aux lemmas are from simp, they are eq versions of iff lemmas marked @[simp]

[Yury G. Kudryashov]

It looks like with Field.Basic, it multiplies by the denominators, then gets a * c = b * c and simplifies it to a = b ∨ c = 0.

[Yury G. Kudryashov]

Without Field.Basic, it goes along a different path because, e.g., docs#neg_div' is not available.

[Yury G. Kudryashov]

field_simp [*] solves the goal in both cases.

[Michael Stoll]

Maybe field_simp should check whether it "knows" that c ≠ 0 when simplifying a * c = b * c? After all, c ≠ 0 is available in the context in the example above.

[Ruben Van de Velde]

That's what field_simp [hc] is for

[Michael Stoll]

In the example, c occurs in the denominator, and field_simp uses h from the context without being specifically asked to do so to clear denominators (which is, as far as I understand, the expected behavior). So it is natural to expect that it would continue to use h in later simplification steps. (In particular seeing that it works without the extra import...)

[Eric Rodriguez]

I thought field_simp didn't inspect the context unless asked to?

[Yury G. Kudryashov]

AFAIR, field_simp uses positivity to discharge side goals.

[Yury G. Kudryashov]

So, if c ≠ 0 appears as a side goal, then field_simp can discharge it. However, if c = 0 appears as a part of the simplified goal, then field_simp can't use c ≠ 0 to simplify it.

[Ruben Van de Velde]

Aha!

[Eric Rodriguez]

Maybe then some lemmas that state assumptions using or should be removed from field simp's default set then!

[Eric Rodriguez]

I guess the issue is that sometimes they'll be resolved with or_true if its something like a term that is passed in but not findable by positivity

[Eric Rodriguez]

So it'll break a fair few proofs