Bad warning advice when local variable resembles constructor

Stream: general

[Valentin Robert]

In a large proof, I was trying to pattern match on zero vs. succ zero vs. succ (succ m), so I started writing (removing all the noise):

example (n : Nat) : n = n := by
  cases n with
  | zero => sorry
  | succ zero => sorry

to which the linter helpfully warns me:

Local variable 'zero' resembles constructor 'Nat.zero' - write '.zero' (with a dot) or 'Nat.zero' to use the constructor.

Sure thing, let's apply the first advice:

example (n : Nat) : n = n := by
  cases n with
  | zero => sorry
  | succ .zero => sorry

Oh no:

unexpected token '.'; expected command

Well, let's try the second suggestion:

example (n : Nat) : n = n := by
  cases n with
  | zero => sorry
  | succ Nat.zero => sorry

Well, this looks like it worked, but it's actually a catch-all with the introduced variable named Nat.zero...

So what's the correct way of pattern-matching on zero vs succ zero vs succ (succ m)?
And, should this linter message be fixed to not give wrong advice?

[Valentin Robert]

Looks like this works, at least:

example (n : Nat) : n = n := by
  match n with
  | .zero => sorry
  | .succ .zero => sorry
  | .succ (.succ m) => sorry

[Aaron Liu]

cases isn't like match

[Aaron Liu]

You can't have recursive cases patterns

[Kenny Lau]

if you want recursive cases, do rcases

[Aaron Liu]

There is a tactic called rcases (the r is for recursive) that can do recursive patterns

[Aaron Liu]

But match works fine too

[Rob Simmons]

Thanks for deatailing this misleading experience. I’ve notes this and will look into it over the next few weeks

[Rob Simmons]

You are definitely getting bad advice from the linter here; sometimes no warning is better than a misleading one

[Kenny Lau]

maybe our strategy of making tactics look like term mode is working too well that it's fooling the linter