erase_duplicates

Stream: new members

[Keeley Hoek]

Does mathlib have a function which erases list duplicates?

[Bryan Gin-ge Chen]

Maybe list.pw_filter?

import data.list.basic

#eval list.pw_filter (≠) [1,2,3,5,5,5,5,2,1,4,1] -- [3, 5, 2, 4, 1]

[Bryan Gin-ge Chen]

Oh, list.erase_dup is defined to be pw_filter (≠). But its docstring is wrong:

/- `erase_dup l` removes duplicates from `l` (taking only the first occurrence).

     erase_dup [1, 2, 2, 0, 1] = [1, 2, 0] -/

#eval list.erase_dup [1, 2, 2, 0, 1] -- [2, 0, 1]

[Kevin Buzzard]

It removed the first "1" and the first "2"

[Kevin Buzzard]

Should it say "...leaving only the last occurrence"?

[Mario Carneiro]

yeah, obviously I meant first from the right end ;)

[Bryan Gin-ge Chen]

I'm putting together a PR that fixes this and also improves the other docstrings in data.list.basic. I found that the example given for list.sigma is also wrong:

/- `sigma l₁ l₂` is the list of dependent pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂ a`.

     sigma [1, 2] (λ_, [5, 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)] -/

#eval list.sigma [1, 2] (λ_, [5, 6])
/- don't know how to synthesize placeholder
context:
⊢ ℕ → Type ?
-/

The following works, but I don't think this would make a good example:

#eval @list.sigma _ (λ_, ℕ) [1, 2] (λ_, [5,6]) --[(1, 5), (1, 6), (2, 5), (2, 6)]

Any suggestions?

[Mario Carneiro]

hm, that's weird

[Mario Carneiro]

does a type ascription on [5,6] work?

[Mario Carneiro]

or even just on 5

[Bryan Gin-ge Chen]

Ah, yes, that works.

[Bryan Gin-ge Chen]

https://github.com/leanprover/mathlib/pull/493