[Merged by Bors] - feat(data/list/perm): perm.permutations #8587

digama0 · 2021-08-09T09:49:37Z

This proves the theorem from Zulip:

theorem perm.permutations {s t : list α} (h : s ~ t) : permutations s ~ permutations t := ...

It also introduces a permutations' function which has simpler equations (and indeed, this function is used to prove the theorem, because it is relatively easier to prove perm.permutations' first).

src/data/list/defs.lean

src/data/list/perm.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/list/perm.lean

eric-wieser

LGTM 🎉! Thanks again.

@pechersky, do you have any interest in trying to golf any proofs?

pechersky · 2021-08-09T13:16:49Z

LGTM. I will be using these proofs in at least #8170, and likely will made a follow-up PR about count l l.permutations to golf #8494.

eric-wieser · 2021-08-09T13:54:52Z

bors d+

It seems this is hitting a random timeout though, so lets not merge until CI passes.

bors · 2021-08-09T13:54:53Z

✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser · 2021-08-10T09:45:36Z

bors r+

This proves the theorem from [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/perm.20of.20permutations): ```lean theorem perm.permutations {s t : list α} (h : s ~ t) : permutations s ~ permutations t := ... ``` It also introduces a `permutations'` function which has simpler equations (and indeed, this function is used to prove the theorem, because it is relatively easier to prove `perm.permutations'` first).

bors · 2021-08-10T12:50:24Z

Pull request successfully merged into master.

Build succeeded:

digama0 added 2 commits August 9, 2021 05:46

feat(data/list/perm): perm.permutations

0bac890

fix

373fd1c