1
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Trebor
    Commented Aug 23, 2022 at 8:33
  • $\begingroup$ @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. $\endgroup$ Commented Aug 23, 2022 at 13:12

2 Answers 2

1
$\begingroup$

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
$\endgroup$
1
  • 1
    $\begingroup$ 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). $\endgroup$ Commented Aug 22, 2022 at 17:02
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.