possible linter bugs

Stream: lean4

[Kevin Buzzard]

Do questions about Std4 (or about linters) go in this stream?

I don't know much about linters but both of these surprised me. Are these bugs or is there something wrong with my structure?

import Std.Tactic.Lint

universe u v

structure MulOpposite (α : Type u) : Type u where
  op :: unop : α

postfix:max "ᵐᵒᵖ" => MulOpposite

namespace MulOpposite

@[simp]
theorem unop_op (x : α) : unop (op x) = x :=
  rfl

@[simp]
theorem unop_inj {x y : αᵐᵒᵖ} : unop x = unop y ↔ x = y := by
  cases x; cases y; simp

#lint
/- The `simpComm` linter reports:
COMMUTATIVITY LEMMA IS SIMP.
Some commutativity lemmas are simp lemmas: -/
#check @unop_inj /- should not be marked simp -/

/- The `simpVarHead` linter reports:
LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.
Some simp lemmas have a variable as head symbol of the left-hand side (after whnfR): -/
#check @unop_op /- Left-hand side has variable as head symbol: x -/

[Kevin Buzzard]

wooah

theorem unop_op (x : α) : unop (op x) = x :=
  by simp only

What black magic is this? That would never work in Lean 3.

[Mario Carneiro]

Kevin Buzzard said:

Do questions about Std4 (or about linters) go in this stream?

There is a #std4 stream

[Mario Carneiro]

These could be bugs in the linters. Simp recently changed its discrimination tree index to unfold less stuff like this, although if the simp only example is any indication then this is still happening in this case

[Reid Barton]

Isn't this just iota reduction? I thought simp only does this by default?

[Mario Carneiro]

no, that was what was disabled

[Mario Carneiro]

well, simp only does iota reduction, it just doesn't pattern match modulo iota reduction any more

[Mario Carneiro]

so actually yes that explains why simp only closes the goal, and the linter is still possibly faulty

[Eric Wieser]

Kevin Buzzard said:

wooah

theorem unop_op (x : α) : unop (op x) = x :=
  by simp only

What black magic is this? That would never work in Lean 3.

This only happens in Lean3 on days ending in y

-- lean3 code but I'm too lazy to use lean3 names
structure {u} MulOpposite (α : Type u) : Type u :=
  op :: (unop : α)

namespace MulOpposite

theorem unop_op {α} (x : α) : unop (op x) = x := by simp only

end MulOpposite

[Kevin Buzzard]

So why doesn't the simp linter complain in lean 3 when this gets tagged simp?

[Eric Wieser]

It only does that on days with an a in:

import tactic.lint

@[nolint doc_blame nolint has_nonempty_instance]
structure {u} MulOpposite (α : Type u) : Type u := op :: (unop : α)

namespace MulOpposite
@[simp] theorem unop_op {α} (x : α) : unop (op x) = x := by simp only
end MulOpposite

#lint  -- fails

[Eric Wieser]

I think your real question is "why does this not happen on docs#mul_opposite in Lean 3?", to which the answer is "because mul_opposite is not a structure".

[Kevin Buzzard]

Thanks! So the conclusion is simply that unop_op should not be tagged with simp in mathlib4 if MulOpposite is a structure, which resolves the simpVarHead question (in some sense at least). The unop_inj / simpComm question remains open. Shall I open an issue on Std for that one?

[Eric Wieser]

Yes, the unop_inj remains mysterious to me; but I'd make sure to really check it is accepted by Lean 3 before reporting it!

[Kevin Buzzard]

Do we have that linter in Lean 3?? I'd never heard of it before I saw that error in the file I was porting.

[Eric Wieser]

I thought we had something similar in the simp attribute itself

[Kevin Buzzard]

More Lean 4 declarations rejected by simpComm:

@[simp, to_additive]
theorem semiconj_by_unop [Mul α] {a x y : αᵐᵒᵖ} :
    SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y :=

and

theorem commute_unop [Mul α] {x y : αᵐᵒᵖ} : Commute (unop x) (unop y) ↔ Commute x y :=
  semiconj_by_unop

[Kevin Buzzard]

And indeed in Lean 3 there is no objection to unop_inj.

import tactic.lint.default

-- lean3 code but I'm too lazy to use lean3 names
structure {u} MulOpposite (α : Type u) : Type u :=
  op :: (unop : α)

namespace MulOpposite

variable (α : Type*)

@[simp]
theorem unop_inj {x y : MulOpposite α} : unop x = unop y ↔ x = y := by
  cases x; cases y; simp

end MulOpposite

#lint -- no objection

This is holding up mathlib4#1036 which is needed to make some opposite-related files less painful to port. How should I proceed? At the minute we're just working around this, but given that these opposite types should be structures (because we can't use the trick of making them irreducible later on in Lean 4), probably the sooner they're turned into structures the better.