Confused about simp_nf linter

Stream: general

[Matej Penciak]

In PR #15513 one of the reviewers suggested that a particular lemma (coe_inv) would make for a good simp lemma (which it definitely does!)...

Unfortunately I keep running into a simp_nf linter error with it, in particular the try_for tactic failing variety. The suggestions in the mathlib docs here are a little unclear on how to troubleshoot the issue. What does it mean to apply squeeze_simp (or try_for { simp }) to the "right hand side"? The proof of the lemma doesn't use any simps, and if I extract the statement of the lemma into a separate example I'm not getting any looping issues when I try to use simp :neutral: .

Any help would be appreciated!

[Johan Commelin]

@Matej Penciak What happens if you do

example : the_LHS = 0 :=
begin
  simp,
  -- did the LHS simplify
end

And idem dito with the RHS.

I'm just guessing, but I think at least one of those two is simplifying...

[Yaël Dillies]

You wrote the lemma the wrong way around. Also, isn't the proof rfl?

[Matej Penciak]

Johan Commelin said:

Matej Penciak What happens if you do

example : the_LHS = 0 :=
begin
  simp,
  -- did the LHS simplify
end

And idem dito with the RHS.

I'm just guessing, but I think at least one of those two is simplifying...

If I put in the RHS then simp fails and nothing happens, but putting in the LHS it simplifies according to the lemma

0. [simplify.rewrite] [symplectic_group.coe_inv]: -(J l R ⬝ (↑A)ᵀ ⬝ J l R) ==> ↑A⁻¹

This seems like it's behaving as it should, right?

[Matej Penciak]

Yaël Dillies said:

You wrote the lemma the wrong way around. Also, isn't the proof rfl?

The lemma originally was the other way around, and was proved with rfl but in the last commit I fixed another simp_nf linter issue telling me to swap the sides and fix the LHS, so the proof is no longer refl.

My understanding was that the LHS should always be more complicated than the RHS?

[Yaël Dillies]

Yes, and ↑A⁻¹ contains something more complicated than everything else: the inverse operation on symplectic_group. Everything in -(J l R ⬝ (↑A)ᵀ ⬝ J l R) is already defined at that point.

[Johan Commelin]

The LHS should indeed be more complicated than the RHS. At the same time the LHS should not be simplifiable by other simp lemmas, otherwise it doesn't get a chance to trigger.