Unused simp arguments linter firing wrongly

Stream: mathlib4

[Michael Stoll]

I just noticed the following. In the example below, the unusedSimpArgs linter complains, but leaving the argument out shows that it is indeed necessary.

import Mathlib

open Nat

/- This simp argument is unused:
  Nat.factorial_ne_zero k -/
example (k : ℕ) : (-1 / k ! : ℂ)⁻¹ / k ! = -1 := by
  simp [field, Nat.factorial_ne_zero k]

example (k : ℕ) : (-1 / k ! : ℂ)⁻¹ / k ! = -1 := by
  simp [field]
  /- 1 goal left : ↑k ! / ↑k ! = 1 -/
  sorry

/- no warning -/
example (k : ℕ) : (1 / k ! : ℂ)⁻¹ / k ! = 1 := by
  simp [field, Nat.factorial_ne_zero k]

/- also works -/
example (k : ℕ) : (-1 / k ! : ℝ)⁻¹ / k ! = -1 := by
  simp [field]

The warning goes away when removing the minus signs. A bit surprisingly, when replacing ℂ by ℝ, the warning is correct. I have no idea what is going on here. @Heather Macbeth ?

[Aaron Liu]

this is a known problem

[Aaron Liu]

found it #29041

[Michael Stoll]

This still does not explain the difference between ℂ and ℝ, though...

[Aaron Liu]

maybe because the reals are ordered?

[Michael Stoll]

It should only matter that k ! is nonzero, regardless of the field (as long as it is of char 0).

[Heather Macbeth]

The field_simp discharger works a bit differently on ℂ compared to on ordered fields such as ℝ. On ordered fields, it uses positivity; on ℂ, positivity is not available (although @Floris van Doorn may have a student working on this) and so, for now, we sometimes need lemmas like Nat.factorial_ne_zero to "fake" it.

[Damiano Testa]

By the way, here are also a few show_term surprises:

• it times out on the first proof;
• shows nothing after a long time on the middle two proofs;
• works on the last.

[Floris van Doorn]

@Pan Lin is indeed working currently working on positivity supporting nonzeroness on non-partial orders.