[Merged by Bors] - feat(data/list/destutter): add list.destutter to remove chained duplicates

[ericrbg]

---

[eric-wieser]

Am I blind, or are you missing the lemma that the list with no pairwise duplicates satisfies list.chain' ne?

On that note, should this be called chain'_dedup, since list.pairwise isn't about adjacency?

[ericrbg]

I like chain'_dedup. I had no real good idea on what to call it. I'll add that proof! Do you have any other ideas what other lemmas to add, maybe that it's idempotent & that if list.chain ne' then it's the identity?

[ericrbg]

oh, I now see why the naming is as it is. I guess I can name the aux chain_dedup and the non-aux chain'_dedup; I'd argue that these should be the other way round, but ¯\_(ツ)_/¯

[ericrbg]

well, that's a bug in the buildscript! we can't have 's in names of files

[eric-wieser]

Yes, that's #11001

[ericrbg]

it's a separate one from that; https://github.com/leanprover-community/mathlib/runs/5140357750?check_suite_focus=true

it's to do with xargs, not Lean itself

[eric-wieser]

I pushed a couple more golfs, and a l.chain'_dedup = l ↔ l.chain' ne simp lemma

[eric-wieser]

LGTM, let's let a fresh pair of eyes confirm.

If you're feeling brave, the following lemmas would probably be useful:

• something about concat (l ++ [a])
• something about append
• l.reverse.chain'_dedup = l.chain'_dedup.reverse

[digama0]

1. This and chain_dedup' should be in data.list.defs. Also could there be a version that accepts a relation?
2. The chain naming suggests that it is related to list.chain, but that definition takes a relation.
3. The use of h :: chain_dedup h l looks like a typo. Shouldn't it be a ::? This will always discard a even if a :: l has no duplicates.

[ericrbg]

I thought about the relation generalisation, but then if !a R b, which one would I discard?

[ericrbg]

and on 3, it seems to break all my proofs in ways that make it seem genuinely different from what I'd expect - if I'm honest, I focused mainly on chain'_dedup, so I didn't pay as close attention as to how exactly to implement chain_dedup without it. Do you think the base case should be | a [] := [a]? That seems reasonable, now that I think about it a little

[eric-wieser]

Discarding the later entry in the list is probably the right choice - the description then becomes "greedily take items from the list (in order) discarding any that do not satisfy R last_accepted candidate", and the current definitions are just the special case when R = ne

[ericrbg]

I'm busy for the next while, but when I next get a chance I'll try work on that generalisation.

[eric-wieser]

Note that with that generalization, this is the chain version of list.pw_filter

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests