simpNF claims LHS doesn't simplify, but it does

Stream: mathlib4

[Jireh Loreaux]

I'm really beginning to hate the simpNF linter. It is claimed here: https://github.com/leanprover-community/mathlib4/blob/a34afbb01d496f13578c002ddc997dd0cab0a083/Mathlib/GroupTheory/Subgroup/Basic.lean#L164 that simpNF says the linter complains when adding the simp attribute (which it does). However, the simpNF linter's claim is false:

import Mathlib.GroupTheory.Subgroup.Basic

variable [Group G] (H : Subgroup G)

@[to_additive (attr := simp)] -- porting note: `simp` cannot simplify LHS
theorem foo_inv {P : G → Prop} :
    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := by
  constructor <;>
    · rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

theorem bar {P : G → Prop} :
    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := by
  simp? -- Try this: simp only [foo_inv]

-- just to make sure there was no weird trickery by using the exact same statement.
theorem baz {P : G → Prop} :
    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ False := by
  simp? -- Try this: simp only [foo_inv]
  sorry

#lint -- `simpNF` claims `foo_inv` can't apply to the LHS and thus will never apply, but it's wrong.

[Jireh Loreaux]

This definitely seems like a bug in simpNF to me.

[Matthew Ballard]

!4#1689 had 3 of these

[Jireh Loreaux]

Moreover, simpNF is doubly wrong (because I'm working on GroupTheory.Coset and I have an in-practice example where this simp lemma fires in that file if it is marked with @[simp])

[Jireh Loreaux]

@Gabriel Ebner see above

[Jireh Loreaux]

In !4#1874 I just added the simp attribrute to this lemma and marked nolint simpNF.

[Jireh Loreaux]

@Matthew Ballard will you check the ones from !4#1689 like I did above to see if simpNF is wrong in those cases too?

[Matthew Ballard]

They were. I just nolinted them all with a Porting note

[Gabriel Ebner]

The linter has a point here. foo_inv and foo_neg should not be simp lemmas. Lean has no good way to match against the pattern ?P x⁻¹ and this will fail in all but toy examples.

[Gabriel Ebner]

example (P : G → G → Prop) : (∃ x : G, x ∈ H ∧ P x⁻¹ 1) ↔ ∃ x ∈ H, P x 1 := by
   simp -- unsolved goals

[Jireh Loreaux]

@Gabriel Ebner please see line 330 of !4#1874. Do you consider that a toy example? If so, then I defer to your judgement.

[Gabriel Ebner]

"Toy example" was maybe a slightly too colorful expression in the heat of the moment..

[Gabriel Ebner]

The technical issue here is that the lemma wouldn't apply if the sides of the equation were swapped.

[Jireh Loreaux]

Okay, thanks. Sorry if my question came across as confrontational; it wasn't intended as such.

Do you think it would be better to keep these lemmas in the simp set for now with nolints to prevent simp calls from breaking during porting, or should we obey the linter? The only downside is performance due to a bigger simp set, right? Or am I wrong about that?

[Yury G. Kudryashov]

More examples: docs4#Filter.tendsto_comp_val_Ioi_atTop (same reason? should I remove @[simp]?), !4#2108 (why?)

[Yury G. Kudryashov]

In !4#2108, it doesn't like MeasurableSpace.measurableSet_inf and MeasurableSpace.measurableSet_infᵢ.

[Yury G. Kudryashov]

In the latter case, it says that simp can prove it using MeasurableSpace.measurableSet_infₛ but why would simp unfold infᵢ here?

[Yury G. Kudryashov]

UPD: it does unfold infᵢ. removing one @[simp]