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

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?

• You need to convince Lean that equality on natural numbers is decidable. It is not the case for e.g. real numbers, so the definition would be uncomputable.
– Trebor
Commented Aug 23, 2022 at 8:33
• @Trebor you can safely assume that if I am struggling with syntax errors, "convince Lean equality is decidable" is beyond my current ability to turn from an abstract goal into concrete steps. Also, I would have assumed the built-in nat would already do things like that. Commented Aug 23, 2022 at 13:12

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

• Argh, I actually tried the one with ∨ but I was tricked by my editor that it was wrong! The online editor at leanprover.github.io/live/latest happens to do a bad substitution for \/ in this context, and it leaves behind sneaky zero-width unprintable characters that were the actual syntax error (as opposed to using \/ causing the error which was what I thought was happening). Commented Aug 22, 2022 at 17:02

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).