field_simp failure

Stream: mathlib4

[Junyan Xu]

The following two examples are similar in form, except that the latter is more complicated, and indeed field_simp succeeds on the former (when followed by ring) but fails on the latter. What could be the problem?

import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring

lemma smulX_add_aux {F} [Field F] {m n m₂ n₂ a s : F}
    (hm : m ≠ 0) (hn : n ≠ 0) (ha : a ≠ 0) (hs : s ≠ 0) :
    m₂ / m ^ 4 * (n₂ / n ^ 4) / (a * s / (n * m) ^ 2) ^ 2 = n₂ * m₂ / (a * s) ^ 2 := by
  field_simp; ring

lemma smulY_add_sub_negY_aux {F} [Field F] {m n m₂ n₂ a s am an : F}
    (hm : m ≠ 0) (hn : n ≠ 0) (ha : a ≠ 0) (hs : s ≠ 0) :
    (m₂ / m ^ 4 * (an * m / (a * n) ^ 2) - n₂ / n ^ 4 * (am * n / (a * m) ^ 2))
      / (a * s / (n * m) ^ 2)
      = (an * m₂ * n - am * n₂ * m) * a / (s * n * m) / a ^ 4 := by
  /- `field_simp; ring` produces
    ⊢ m₂ * an * m ^ 6 * n ^ 7 * a ^ 6 * s * m⁻¹ ^ 6 * n⁻¹ ^ 6 * a⁻¹ ^ 5 * s⁻¹ -
      m ^ 7 * n ^ 6 * a ^ 6 * n₂ * am * s * m⁻¹ ^ 6 * n⁻¹ ^ 6 * a⁻¹ ^ 5 * s⁻¹ =
    m₂ * an * n * a - m * a * n₂ * am -/
  field_simp; rw [div_eq_iff]
  · ring
  apply_rules [pow_ne_zero, mul_ne_zero]

When working with elliptic curves I find that field_simp is not fast enough and I had to extract lemmas that capture the pattern (it's probably the field being complicated that makes it slow). How could we make it faster so it's more convenient to use?

[Junyan Xu]

cc author @Sébastien Gouëzel and porter @David Renshaw

[David Renshaw]

Increasing the max discharge depth makes it work:

lemma smulY_add_sub_negY_aux {F} [Field F] {m n m₂ n₂ a s am an : F}
    (hm : m ≠ 0) (hn : n ≠ 0) (ha : a ≠ 0) (hs : s ≠ 0) :
    (m₂ / m ^ 4 * (an * m / (a * n) ^ 2) - n₂ / n ^ 4 * (am * n / (a * m) ^ 2))
      / (a * s / (n * m) ^ 2)
      = (an * m₂ * n - am * n₂ * m) * a / (s * n * m) / a ^ 4 := by
  field_simp (config := {maxDischargeDepth := 9}); ring

[Junyan Xu]

Thank you! I think this configuration should be in the docstring. Here is another small issue with field_simp:

import Mathlib.Tactic.FieldSimp

variable {F} [Field F] {x₁ x₂ : F} (hx : x₁ - x₂ ≠ 0)

lemma neg_sub_div_sub : -(x₁ - x₂) / (x₁ - x₂) = -1 := by
  field_simp /- successful -/

lemma sub_div_neg_sub : (x₁ - x₂) / -(x₁ - x₂) = -1 := by
  field_simp /- goal: (x₁ - x₂) / (x₂ - x₁) = -1 -/

[Richard Copley]

It can do a little more inference if you lift to the group of units:

import Mathlib.Tactic.FieldSimp

variable {F} [Field F] {x₁ x₂ : F} (hx : x₁ - x₂ ≠ 0)

lemma sub_div_neg_sub : (x₁ - x₂) / -(x₁ - x₂) = -1 := by
  lift x₁ - x₂ to Fˣ using hx.isUnit with h
  field_simp -- successful

Sadly it doesn't do the same with NeZero instances, so even adding this silly thing doesn't help much:

instance {F} [SubtractionMonoid F] {x y : F} [inst: NeZero (x - y)] : NeZero (y - x) :=
  have ⟨hx⟩ := inst
  ⟨by rwa [← neg_zero, ← neg_sub, neg_inj.ne]⟩

maxDischargeDepth is passed straight to simp (after increasing it to at least 7 if necessary). See #11070, #12239, previous discussion.

[Junyan Xu]

Thanks for the pointers!
The issue with sub_div_neg_sub is field_simp somehow "simplified" -(x₁ - x₂) to (x₂ - x₁) so it can no longer use hx. Switching x₁ and x₂ in hx makes it work again:

lemma sub_div_neg_sub : (x₁ - x₂) / -(x₁ - x₂) = -1 := by
  rw [sub_ne_zero, ne_comm, ← sub_ne_zero] at hx
  field_simp -- successful

It also suffices to use set instead of lift:

lemma sub_div_neg_sub : (x₁ - x₂) / -(x₁ - x₂) = -1 := by
  set x := x₁ - x₂
  field_simp

[Junyan Xu]

Consider also the following four examples, whose behaviors hinge upon that docs#neg_sq is a simp lemma but there's no such lemma for the cube:

import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring

variable {F} [Field F] {x : F}

lemma pow_three_div_neg_pow_three (hx : -x ≠ 0) : x ^ 3 / (-x) ^ 3 = -1 := by
  field_simp; ring -- successful

lemma pow_three_div_neg_pow_three' (hx : x ≠ 0) : x ^ 3 / (-x) ^ 3 = -1 := by
  field_simp -- simp made no progress

lemma sq_div_neg_sq (hx : -x ≠ 0) : x ^ 2 / (-x) ^ 2 = 1 := by
  field_simp -- ⊢ x ^ 2 / x ^ 2 = 1

lemma sq_div_neg_sq' (hx : x ≠ 0) : x ^ 2 / (-x) ^ 2 = 1 := by
  field_simp -- successful