Instability of the denominator in `field_simp` tactic

Stream: mathlib4

[Weiyi Wang]

(here is a demo. Not exactly my real code but it reproduces the problem

import Mathlib
variable (x y u r z : ℂ)

example (h : -2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2) ≠ 0 ) :
  (1 / (-2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2))) = z + 3 / (-2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2)) := by
  field_simp
  sorry

)

First I have this in the context

have hdeno : -2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2) ≠ 0 = by ...

(all involved variables are complex numbers, if it matters)
I have a goal of a rational equation involving the same set of variables, and the only ones that appear in the denominator are the one proven non-zero above.
However, when I do field_simp, it couldn't resolve all the denominators. When I looked closely, I see that it randomly permutates the term order in the denominator, leaving me to prove things such as

have deno' : (-(2 * r ^ 2 * ((u + r) ^ 2 - 1) * y * (r * x - u)) +
      (r * x + u) * (r * x * (r * (u + r) * x + 2 * (1 - r * (u + r))) + u ^ 2 * (u + r))) ≠ 0 := by

and it is not a consistent order, either. I have two sub goals with similar expression, and field_simp permutates it in different way.
I could add more auxiliary haves to make it work, but I am concerned that this will randomly break after updates. Is there a better way to teach field_simp to look for all possible permutation of non-zero lemmas?

[Kevin Buzzard]

(deleted)

[Michael Rothgang]

I presume what happens is that your have is not in "field-simp normal form", and what happens is that

• field_simp converts the goal into normal form
• this changes the denominator into normal form also
• as your have is not in field_simp normal form, it cannot be used to discharge the non-zeroness hypotheses

You can

• change your have statement to bring it into field_simp normal form, or
• do so automatically using field_simp at h, or
• use set to extract this as a constant.

I'm not sure what exactly your question is. Does that answer it?

[Michael Rothgang]

Here's code for the "field_simp at h" approach:

import Mathlib
variable (x y u r z : ℂ)

example (h : -2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2) ≠ 0 ) :
  (1 / (-2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2))) = z + 3 / (-2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2)) := by
  field_simp at h ⊢
  sorry

[Michael Rothgang]

Here's how to write it using set:

import Mathlib
variable (x y u r z : ℂ)

example (h : -2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2) ≠ 0 ) :
  (1 / (-2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2))) = z + 3 / (-2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2)) := by
  set A := -2 * r ^ 2 * ((u + r) ^ 2 - 1) * (r * x - u) * y +
      (r * x + u) *
      (r ^ 2 * (u + r) * x ^ 2 + 2 * r * (1 - r * (u + r)) * x + (u + r) * u ^ 2)
  field_simp
  -- goal is now "1 = A * z + 3"
  sorry

[Michael Rothgang]

This question is independent of real or complex numbers, by the way. (Making all variables real does not change the behaviour here.)

[Michael Rothgang]

I agree that field_simp could be more helpful by telling you which denominators I cannot prove are non-zero. This will be coming; @Arend Mellendijk is working on that.

[Michael Rothgang]

Let me also add that the field_simp normal form is not random (though I don't remember the precise details how it is decided). In general, you should not have to rely on it too much - and with one of the strategies above, you indeed need not.

[Weiyi Wang]

Thanks! I do have a case where the normal form is seemingly random (as in, the same denominator got transformed differently in two expressions). I haven't been able to minimize it, but I can soon upload the code for further investigation

[Weiyi Wang]

I also wish field_simp can have a mode where I can say "I guarantee that all denominators are not zero. Could you try harder with the list of hypothesis I provided? You might need to use ring to transform it, or multiply it by -1"

[Ruben Van de Velde]

There's been discussion before about having an option to field_simp that leaves subgoals for any denominators that it can't prove to be nonzero on its own. That seems like a more scalable approach

[Weiyi Wang]

@Michael Rothgang Here is an example of seemingly inconsistent normal form: https://github.com/wwylele/Poncelet/blob/0532e61afdc89a0032978b07fa53eaf9c3a08385/Poncelet/TransferAux.lean#L73-L74

• field on line 73 requires the presence of hdeno' on line 35
• field_simp on line 74 requires the presence of hdeno'' on line 40
• field_simp on line 107 requires the presence of hdeno''' on line 45

By commenting out either hypothesis, you can observe the error on the corresponding tactic.
(warning: this file also contains very ugly long expressions that makes vscode slow. You can comment those out first and it won't impact this problem)

[Weiyi Wang]

Let me try the approaches you suggested

[Weiyi Wang]

The set approach works pretty well! and I think it also makes my code cleaner. Funnily enough, this also resulted in another weird inconsistency: the field on line 35 still doesn't work after I use set to hide the denominator, and it seems that it can see through it, but when I replaced it with field_simp it worked (It is just a giant A = A / B * B expression so I guess it doesn't need extra ring power)