In lean, how to work around "invalid pattern, 'x' already appeared in this pattern"

Question

I am trying to define what it means for an item to be in a list. I wrote this case breakdown:

inductive NatList : Type
| nil : NatList
| cons : nat → NatList → NatList

def contains : nat -> NatList -> Prop
| _ NatList.nil := false
| x (NatList.cons x _) := true   -- error here
| x (NatList.cons _ tail) := contains x tail

On the | x (NatList.cons x _) := true line I get the error invalid pattern, 'x' already appeared in this pattern. I can see that I have in fact used x twice. But that's because I actually want it to pattern match to the case where the list item matches the query item. How do I rephrase what I want in a way that Lean will accept?

Answer 1

The simplest solution I know of is this:

def contains : nat -> NatList -> Prop
| _ NatList.nil := false
| x (NatList.cons y tail) := 
  if x = y then 
    true
  else 
    contains x tail

Note that for Lean to decide if x = y is true, you need equality to be decidable, like it is for nat. If you replace nat with another type without decidable equality like nat -> nat, then this definition will fail. I assume it is for subtle reasons like this that Lean doesn't support the notation you had in mind.

Edit: Actually, if you are working with Prop, you likely don't care about computability and decidability. Further, the general list version of this is in the library as list.mem with definition:

protected def mem : α → list α → Prop
| a []       := false
| a (b :: l) := a = b ∨ mem a l

Answer 2

If you want to use x multiple times during a pattern match you need to use .(x) for each additional appearance of x. But even after fixing this Lean complains that equation 3 isn't being used in the compilation (not sure what is happening here).