# Zulip Chat Archive

## Stream: general

### Topic: perm of permutations

#### Eric Wieser (Jul 03 2021 at 18:47):

This statement handwaves to "it's obvious", but the implementation of docs#list.permutations is so inscrutable to me (how are the permutations even ordered?), that I have no idea how to begin to prove it.

```
import data.list.perm
variables {α : Type*} [decidable_eq α] {l₁ l₂ : list α}
/-- Two lists equivalent up to permutations have a list of permutations that are
equivalent up to permutation -/
lemma list.perm_permutations (h : l₁ ~ l₂) :
l₁.permutations ~ l₂.permutations :=
sorry
```

#### Eric Wieser (Jul 03 2021 at 18:48):

(I already asked this on the Discord, but figured I might have more luck here since the authors of `perm.lean`

, Leo, Jeremy, and Mario aren't all on discord)

#### Eric Wieser (Jul 03 2021 at 18:54):

Regarding ordering, the python order looks much more obvious at a glance:

```
#eval [1, 2, 3].permutations
-- [[1, 2, 3], [2, 1, 3], [3, 2, 1], [2, 3, 1], [3, 1, 2], [1, 3, 2]]
```

```
import itertools
list(itertools.permutations([1, 2, 3]))
# [(1, 2, 3), (1, 3, 2), (2, 1, 3), (2, 3, 1), (3, 1, 2), (3, 2, 1)]
```

#### Bhavik Mehta (Jul 03 2021 at 19:02):

It looks to me like it's implemented like the Haskell version: https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-List.html#v:permutations

#### Bhavik Mehta (Jul 03 2021 at 19:04):

And it's implemented like that in Haskell to take full advantage of laziness: https://stackoverflow.com/questions/24484348/what-does-this-list-permutations-implementation-in-haskell-exactly-do

#### Chris Hughes (Jul 03 2021 at 19:24):

It doesn't need to be redefined but it does need more lemmas about it. The trouble is that the permutations seem to be in a strange order so there's no nice statement of `permuations_cons`

. Maybe it's best to basically treat it like a multiset, and not prove any lemmas about the order.

#### Eric Wieser (Jul 03 2021 at 19:32):

Is laziness relevant to lean?

#### Bhavik Mehta (Jul 03 2021 at 19:36):

I don't think so, but there are also properties of this implementation which are nice though they're not proved in Lean

#### Eric Wieser (Jul 03 2021 at 19:37):

I guess in principle we could have a `list.lexicographic_permutations`

function

#### Eric Wieser (Jul 03 2021 at 19:37):

But proving its equivalence modulo permutation to the current implementation seems every bit as hard as my original lemma statement

#### Bhavik Mehta (Jul 03 2021 at 19:38):

Eric Wieser said:

I guess in principle we could have a

`list.lexicographic_permutations`

function

We have something similar for list.sublists and list.sublists' so there is precedent for this kind of duplication

#### Eric Wieser (Jul 03 2021 at 19:39):

Chris, we have docs#list.permutations_aux_cons; I think the API of permutations is "unfold it first, then use the API of permutations_aux".

#### David Wärn (Jul 03 2021 at 20:00):

Do we have any of these?

- every permutation of
`l`

occurs in`l.permutations`

`l.permutations`

has length`l.length!`

`l.permutations`

is natural in functions`\a -> \b`

At least in principle these 3 should be enough to prove the result at the top of this thread

#### Bhavik Mehta (Jul 03 2021 at 20:01):

We have your first and second points certainly, at the bottom of data/list/perm

#### Eric Wieser (Jul 03 2021 at 20:04):

What does "is natural" mean there?

#### David Wärn (Jul 03 2021 at 20:04):

`(l.map f).permutations = ...`

#### David Wärn (Jul 03 2021 at 20:05):

You should be able to use this to reduce to the universal case where `l1`

and `l2`

are permutations of `[1, 2, ... n]`

#### Eric Wieser (Jul 03 2021 at 20:05):

Where the `...`

is `l.permutations.map (\lam l, l.map f)`

?

#### Eric Wieser (Jul 03 2021 at 20:05):

That does seem like an easier result to prove

#### Eric Wieser (Jul 03 2021 at 20:44):

Even proving that seems challenging, although my approach was just to hope that guessing the right induction would get me where I need to be:

```
lemma list.permutations_aux_map {α β : Type*} (l is : list α) (f : α → β) :
(l.map f).permutations_aux (is.map f) = (l.permutations_aux is).map (list.map f) :=
begin
apply @list.permutations_aux.rec _ (λ l is, (l.map f).permutations_aux (is.map f) = (l.permutations_aux is).map (list.map f)),
{ dsimp,
intros is,
simp, },
{ dsimp,
intros t ts is h₁ h₂,
simp [h₁, list.permutations, h₂],
clear h₁ h₂,
induction is with h_is t_is ih_is,
{ simp },
simp only [list.map_cons,
list.permutations_aux2_snd_cons],
refine ⟨by simp, _⟩,
sorry
}
end
lemma list.permutations_map {α β : Type*} (l : list α) (f : α → β) :
(l.map f).permutations = l.permutations.map (list.map f) :=
begin
unfold list.permutations,
dsimp,
congr,
convert list.permutations_aux_map l [] f,
end
```

#### Mario Carneiro (Jul 03 2021 at 21:05):

The definition of `permutations`

is definitely not supposed to be observable beyond the API, because it's a very messy definition

#### Mario Carneiro (Jul 03 2021 at 21:06):

While lean doesn't have to worry about laziness, it does have to worry about blowing the stack, so something like the haskell definition is still required

#### Mario Carneiro (Jul 03 2021 at 21:08):

all the key lemmas about `permutations_aux`

are proven at the end of `data.list.perm`

#### Mario Carneiro (Jul 03 2021 at 21:14):

Chris Hughes said:

It doesn't need to be redefined but it does need more lemmas about it. The trouble is that the permutations seem to be in a strange order so there's no nice statement of

`permuations_cons`

. Maybe it's best to basically treat it like a multiset, and not prove any lemmas about the order.

Indeed, although it doesn't have `permutations_cons`

, it is possible to state `permutations_cons`

using `~`

instead of equality

#### Mario Carneiro (Jul 03 2021 at 22:12):

I have a proof of `map_permutations`

in #8188, but I'm not sure how @David Wärn was thinking of using it to prove the perm permutation theorem

#### Eric Wieser (Jul 03 2021 at 22:57):

Those proofs are gnarly, pattern matching on `_match_1`

#### Eric Wieser (Jul 03 2021 at 22:58):

Are those just golfed to oblivion, or is there something going on that makes more conventional approaches tricky?

#### Yakov Pechersky (Jul 04 2021 at 02:05):

You can form an iso between members of list.permutations l and equiv.perm of the subtype of members of l, when nodup l. Then, by a cardinality argument, l.permutations must be nodup too. Then the result at the top of this thread follows. To form the iso, one needs the cycle.form_perm that I've been working on.

#### David Wärn (Jul 04 2021 at 09:00):

I had in mind something along the lines of

- prove that if
`l.nodup`

then`l.permutations.nodup`

using a cardinality argument, like Yakov said. I think here you just need the fact that each`e : equiv.perm (fin l.length)`

defines a distinct permutation of`l`

. - If
`l1 ~ l2`

, then`l1.permutations`

and`l2.permutations`

have the same elements, not counting multiplicity. So if`l1.nodup`

, then everything is`nodup`

, and so`l1.permutations ~ l2.permutations`

. - If
`l.map f ~ t`

, then there exists`l'`

such that`l ~ l'`

and`t = l'.map f`

. Using this (or something else, I don't know what's in mathlib), you can prove that if`l1 ~ l2`

, with`l1 : list \a`

, then there exists`\b`

and`f : \b -> \a`

and`l1', l2' : list \b`

such that`l1 = l1'.map f`

,`l2 = l2'.map f`

, and`l1'.nodup`

. Concretely you can take`\b = fin l1.length`

,`f i = l1.nth i`

,`l1 = [0, 1, ...]`

. - Deduce the original result, using
`map_permutations`

#### Eric Wieser (Jul 04 2021 at 12:00):

I had another stab at proving it from induction alone, but I'm running into a total lack of understanding about the semantics of `permutations_aux`

, and can't work out any of the properties it has. Is this true?

```
lemma list.perm.permutations_aux :
∀ (l i₁ i₂ : list α) (h : i₁ ~ i₂),
l.permutations_aux i₁ ~ l.permutations_aux i₂ :=
```

#### Eric Wieser (Jul 04 2021 at 12:01):

(if anyone who does understand `permutations_aux`

could write a docstring for it, that would be amazing! Otherwise I guess I should read the thorough explanation of the haskell code that Bhavik linked to...)

#### Mario Carneiro (Jul 04 2021 at 12:23):

I wrote `permutations`

and all the lemmas, but I can't say I have a deep understanding of what it does. For the most part, my understanding is already encoded in lemmas like docs#list.mem_foldr_permutations_aux2 and docs#list.mem_permutations_aux_of_perm that give a sense of what the inductive invariant is

#### Mario Carneiro (Jul 04 2021 at 12:25):

Eric Wieser said:

Those proofs are gnarly, pattern matching on

`_match_1`

What is this a reference to? I didn't do any match like that in that PR

#### Mario Carneiro (Jul 04 2021 at 12:26):

Oh, you are talking about `permutations_aux2_fst`

et al. I didn't write those for the PR, they were just moved from data.list.perm to data.list.basic

#### Mario Carneiro (Jul 04 2021 at 12:27):

That kind of dependent matching is a rather old style, I think we have better tactics for doing that today but I don't feel like rewriting the proofs

#### Mario Carneiro (Jul 04 2021 at 12:31):

Eric Wieser said:

I had another stab at proving it from induction alone, but I'm running into a total lack of understanding about the semantics of

`permutations_aux`

, and can't work out any of the properties it has. Is this true?`lemma list.perm.permutations_aux : ∀ (l i₁ i₂ : list α) (h : i₁ ~ i₂), l.permutations_aux i₁ ~ l.permutations_aux i₂ :=`

That looks like a good job for `slim_check`

#### Eric Wieser (Jul 04 2021 at 13:19):

I take it that means it is false

#### Yakov Pechersky (Jul 04 2021 at 13:23):

`slim_check`

hangs on this because checking that two lists are `perm`

works by enumerating over all appendings:

```
import tactic.slim_check
import data.list.perm
example (l l' : list ℕ) :
l.permutations_aux l' ~ l.permutations_aux (l'.rotate 1) := by slim_check
```

#### Mario Carneiro (Jul 04 2021 at 13:34):

Here's a reconstruction of the argument as a literate lean file:

```
import data.list.perm
open list
variables {α β : Type}
def foo (t : α) (ts : list α) (ys : list α) : list (list α) :=
(permutations_aux2 t ts [] ys id).2
-- permutations_aux2 is a bunch of functorial nonsense over the foo function:
example (t : α) (ts : list α) (ys : list α) (r : list β) (ys : list α) (f : list α → β) :
permutations_aux2 t ts r ys f = (ys ++ ts, (foo t ts ys).map f ++ r) := sorry
def bar (t : α) (ys : list α) : list (list α) := foo t [] ys
-- foo is also a simple mapping of bar:
example (t : α) (ts : list α) (ys : list α) :
foo t ts ys = (bar t ys).map (λ l, l ++ ts) := sorry
-- bar inserts x into every position of xs except the last:
#eval bar 10 [1, 2, 3]
-- [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]]
-- permutations_aux is defined using the following recursion,
-- where I've moved the contribution of each iteration into a separate definition:
def grouping (t : α) (ts is : list α) : list (list α) :=
(permutations is).bind (λ ys, foo t ts ys)
example (t : α) (ts is : list α) :
permutations_aux (t :: ts) is = grouping t ts is ++ permutations_aux ts (t :: is) := sorry
-- You should think of `is` as a side parameter here;
-- just pretend `permutations is` is already defined earlier so that this
-- is a simple recursion on `ts`.
-- The one other oddity here is the definition of `permutations` itself:
example (l : list α) : permutations l = l :: permutations_aux l [] := rfl
-- We're handling the identity permutation separately, so `permutations_aux` only deals with
-- the non-identity permutations. It's something like decomposing integers by powers of 10;
-- zero requires special handling.
-- So what's the big idea? We are going to partition the (non-identity) permutations
-- according to the longest fixed suffix. You can see that here:
#eval permutations [1, 2, 3, 4]
-- [[1, 2, 3, 4], [2, 1, 3, 4], [3, 2, 1, 4], [2, 3, 1, 4], [3, 1, 2, 4], [1, 3, 2, 4],
-- [4, 3, 2, 1], [3, 4, 2, 1], [3, 2, 4, 1], [4, 2, 3, 1], [2, 4, 3, 1], [2, 3, 4, 1],
-- [4, 1, 2, 3], [1, 4, 2, 3], [1, 2, 4, 3], [4, 2, 1, 3], [2, 4, 1, 3], [2, 1, 4, 3],
-- [4, 1, 3, 2], [1, 4, 3, 2], [1, 3, 4, 2], [4, 3, 1, 2], [3, 4, 1, 2], [3, 1, 4, 2]]
-- is partitioned like so:
#eval grouping 1 [2, 3, 4] [] -- []
#eval grouping 2 [3, 4] [1] -- [[2, 1, 3, 4]]
#eval grouping 3 [4] [2, 1] -- [[3, 2, 1, 4], [2, 3, 1, 4], [3, 1, 2, 4], [1, 3, 2, 4]]
#eval grouping 4 [] [3, 2, 1]
-- [[4, 3, 2, 1], [3, 4, 2, 1], [3, 2, 4, 1], [4, 2, 3, 1], [2, 4, 3, 1], [2, 3, 4, 1],
-- [4, 1, 2, 3], [1, 4, 2, 3], [1, 2, 4, 3], [4, 2, 1, 3], [2, 4, 1, 3], [2, 1, 4, 3],
-- [4, 1, 3, 2], [1, 4, 3, 2], [1, 3, 4, 2], [4, 3, 1, 2], [3, 4, 1, 2], [3, 1, 4, 2]]
-- There no nonidentity permutations that fix 2,3,4, one permutation that fixes 3,4,
-- 4 permutations that fix 4, and the remaining 18 permutations don't fix 4.
-- So how does `grouping` accomplish this? It is defined like so:
example (t : α) (ts is : list α) :
grouping t ts is = (permutations is).bind (λ ys, (bar t ys).map (λ l, l ++ ts)) := sorry
-- We know that `ts` is the fixed suffix, and also that `t::ts` is *not* fixed,
-- or else we would be in the next group. Given a permutation of `is++t::ts` that fixes `ts`
-- and does not fix `t::ts`, we know that `t` and `is` are mixed in some way, which we
-- express as a permutation of `is` with `t` inserted anywhere except the last position.
-- We then append `ts` at the end as required, and that's what `grouping` does.
-- Appending all these lists for different suffixes produces all permutations except the
-- identity, because we assumed that `t::ts` was not fixed so the identity permutation is
-- never in any of the groups. So `permutations` has to do one final fixup to put it in.
```

#### Mario Carneiro (Jul 04 2021 at 13:44):

Yakov Pechersky said:

`slim_check`

hangs on this because checking that two lists are`perm`

works by enumerating over all appendings:`import tactic.slim_check import data.list.perm example (l l' : list ℕ) : l.permutations_aux l' ~ l.permutations_aux (l'.rotate 1) := by slim_check`

Ooh, that's probably kernel computation coming to bite us

#### Mario Carneiro (Jul 04 2021 at 13:44):

`slim_check`

doesn't use `#eval`

#### Mario Carneiro (Jul 04 2021 at 13:50):

Eric Wieser said:

I take it that means it is false

Having written all that, I think that it is true. Anything that goes into the `is`

argument is either an input of `permutations is`

for the current group or is passed to the next iteration as `t::is`

, so it will only ever be scrambled. Therefore permuting the `is`

should result in a permutation of the output, and moreover it will be a permutation individually in the groups, that is, you can prove each group is separately a permutation

#### Eric Wieser (Jul 04 2021 at 21:07):

Thanks for that thorough explanation @Mario Carneiro, it was enough for me to spot the pattern!

I guess this statement is true then?

```
lemma permutations_concat (l : list α) (x : α) :
(l ++ [x]).permutations =
l.permutations.map (λ p, p ++ [x]) ++ l.permutations.bind (bar x) := sorry
```

#### Eric Wieser (Jul 04 2021 at 21:09):

Edit: no, #eval tells me its false

#### Eric Wieser (Jul 04 2021 at 21:12):

In which case, I'm still confused by how the order of the elements in `grouping 3 [4] [2, 1]`

is determined.

#### Mario Carneiro (Jul 04 2021 at 23:33):

`grouping 3 [4] [2, 1]`

is `[[3, 2, 1, 4], [2, 3, 1, 4], [3, 1, 2, 4], [1, 3, 2, 4]]`

. It is defined as:

```
grouping t ts is = ((permutations is).bind (bar t)).map (λ l, l ++ ts)
```

So we're putting `[4]`

on the end of each list, without that it's `[[3, 2, 1], [2, 3, 1], [3, 1, 2], [1, 3, 2]]`

. These are obtained by taking `permutations [2, 1] = [[2, 1], [1, 2]]`

, and then inserting `3`

at the first and second positions of each. Inserting `3`

in `[2, 1]`

yields `[3, 2, 1], [2, 3, 1]`

, and inserting `3`

in `[1, 2]`

yields `[3, 1, 2], [1, 3, 2]`

.

Now the particular ordering of `permutations [2, 1] = [[2, 1], [1, 2]]`

depends on a recursive call, so we're back to stage one here. This is why `permutations_aux`

has such a convoluted recursor. But your inductive hypothesis should supply whatever you need to know about this function.

#### Eric Wieser (Jul 05 2021 at 09:48):

Ah, it's the fact that the second argument to `grouping`

is reversed that threw me off

#### Eric Wieser (Jul 05 2021 at 09:48):

The true version of my statement appears to be

```
abbreviation permutations_concat_statement (l : list α) (x : α) :=
(l ++ [x]).permutations =
l.permutations.map (λ p, p ++ [x]) ++ l.reverse.permutations.bind (bar x)
#eval (permutations_concat_statement [1, 2, 3] 4 : bool)
#eval (permutations_concat_statement [] 4 : bool)
```

#### Eric Wieser (Jul 05 2021 at 09:49):

I assume the `.reverse`

in there for some efficiency reason regarding assembling lists

#### Eric Wieser (Jul 05 2021 at 11:01):

This looks like it will probably help with `permutations_aux2`

:

```
/-- The `ts`, `r`, and `f` arguments of `permutations_aux2` are just post-processing. -/
lemma permutations_aux2_snd_f (t : α) (ts : list α) (ys : list α) (r : list β)
(f : list α → β) :
(permutations_aux2 t ts r ys f).snd =
(permutations_aux2 t [] [] ys id).snd.map (λ xs, f (xs ++ ts)) ++ r :=
calc (permutations_aux2 t ts r ys f).snd
= (permutations_aux2 t ts [] ys f).snd ++ r : begin
induction ys with y ys generalizing f,
{ simp },
{ simp [ys_ih (λ xs, f (y :: xs))] }
end
... = (permutations_aux2 t ts [] ys id).snd.map f ++ r : begin
congr' 1,
convert (map_permutations_aux2' id _ _ _ _ _ _ _ _).symm; simp,
end
... = (permutations_aux2 t [] [] ys id).snd.map (λ xs, f (xs ++ ts)) ++ r : begin
rw ←map_map f (++ ts),
congr' 2,
induction ys,
{ simp },
simp,
sorry,
-- convert (map_permutations_aux2' _ _ _ _ _ _ _ _ _).symm,
end
```

Unfortunately I'm not sure how to show the `sorry`

.

#### Eric Rodriguez (Jul 05 2021 at 11:19):

does

```
induction ts,
simp only [append_nil],
rw map_permutations_aux2' id,
simp,
intro, rw map_id,
```

make any useful progress? I don't really understand `permutations_aux2`

so I went for "goal-driven development"

#### Bhavik Mehta (Jul 05 2021 at 12:04):

```
example {t : α} {ts ys : list α} (f : list α → β) (g : list α → list α)
(hg : ∀ l₁ l₂, g (l₁ ++ l₂) = g l₁ ++ l₂) :
(permutations_aux2 t ts [] ys g).2.map f =
(permutations_aux2 t [] [] ys g).2.map (λ xs, f (xs ++ ts)) :=
begin
induction ys generalizing g,
{ simp },
simp only [true_and, id.def, map, eq_self_iff_true, permutations_aux2_snd_cons, append_nil],
refine ⟨_, _⟩,
{ rw hg },
{ rw ys_ih,
intros l₁ l₂,
rw [←cons_append, hg] }
end
```

Solves your sorry Eric! By the way, your first begin/end in the calc is already in mathlib: `permutations_aux2_append`

#### Mario Carneiro (Jul 05 2021 at 12:40):

There are already lemmas which eliminate the `f`

and `r`

parameters of `permutations_aux2`

, so you don't need them in the lemma statement. It's a lot easier to tackle these arguments one at a time

#### Mario Carneiro (Jul 05 2021 at 12:42):

Actually, I don't think it's worth eliminating the `ts`

argument. In the context of `grouping`

, the `foo`

function makes a bit more sense than `bar`

: we have a list `is ++ t :: ts`

and are permuting the left half of it and moving `t`

out of place

#### Eric Wieser (Jul 05 2021 at 12:51):

Perhaps this is the lemma that's missing then?

```
/-- The `ts` argument to `permutations_aux2` can be folded into the `f` argument. -/
lemma permutations_aux2_comp_append {t : α} {ts ys : list α} {r : list β} (f : list α → β) :
(permutations_aux2 t [] r ys $ λ x, f (x ++ ts)).2 = (permutations_aux2 t ts r ys f).2 :=
begin
symmetry,
induction ys generalizing f,
{ simp },
simp only [true_and, id.def, map, eq_self_iff_true, permutations_aux2_snd_cons, append_nil],
refine ys_ih _,
end
```

#### Eric Wieser (Jul 05 2021 at 12:52):

Stated backwards to match docs#list.permutations_aux2_append

#### Mario Carneiro (Jul 05 2021 at 13:01):

Looking again, I actually don't see a lemma that says that `f`

can be eliminated, but most of the lemmas are about `f = id`

so apparently they (that is, past me) managed to get around it

#### Eric Wieser (Jul 05 2021 at 13:03):

I'll add the lemma that eliminates `f`

too, even if it doesn't get used - it's good for explaining what the function does

#### Bhavik Mehta (Jul 05 2021 at 13:06):

Isn't `map_permutations_aux2'`

the one that eliminates `f`

?

#### Eric Wieser (Jul 05 2021 at 13:06):

Yes, but it's stated very generally which makes it hard to apply

#### Eric Wieser (Jul 05 2021 at 13:26):

The yellow bars are stuck in "refresh every time I hit a key" mode so this is taking forever

#### Johan Commelin (Jul 05 2021 at 13:27):

Do you have any other open files?

#### Eric Wieser (Jul 05 2021 at 13:27):

They're all "plaintext" files

#### Eric Wieser (Jul 05 2021 at 13:27):

Although only because I told Vscode to not process them as lean any more

#### Eric Wieser (Jul 05 2021 at 13:27):

They're also all unsaved anonymous buffers

#### Johan Commelin (Jul 05 2021 at 13:28):

Aha

#### Johan Commelin (Jul 05 2021 at 13:28):

For me, it usually worked to restart VScode with only 1 file open.

#### Eric Wieser (Jul 05 2021 at 13:29):

I restarted vscode, reopening to 1 lean file + 5 plaintext buffers and it still behaves poorly.

#### Eric Wieser (Jul 05 2021 at 13:29):

Maybe CI can build for me: #8198

#### Mario Carneiro (Aug 09 2021 at 09:49):

Done in #8587 :tada:

#### Mario Carneiro (Aug 09 2021 at 09:51):

That PR also introduces `list.permutations'`

which has much more straightforward equations:

```
@[simp] def permutations'_aux (t : α) : list α → list (list α)
| [] := [[t]]
| (y::ys) := (t :: y :: ys) :: (permutations'_aux ys).map (cons y)
@[simp] def permutations' : list α → list (list α)
| [] := [[]]
| (t::ts) := (permutations' ts).bind $ permutations'_aux t
```

#### Yaël Dillies (Aug 09 2021 at 10:13):

Oh wow! I was genuinely banging my hand against this problem.

#### Yaël Dillies (Aug 09 2021 at 10:14):

@Yakov Pechersky, it's Christmas before December!

#### Yaël Dillies (Aug 09 2021 at 10:16):

I was wondering, what's the difference in practice between a new inductive definition and a new recursor? Could you have proven `perm.permutations`

with just the new recursor?

#### Mario Carneiro (Aug 09 2021 at 10:17):

no, because `list.permutations'`

is not equal to `list.permutations`

#### Mario Carneiro (Aug 09 2021 at 10:18):

it is a complicated permutation thereof

#### Mario Carneiro (Aug 09 2021 at 10:20):

If you replaced `=`

with `~`

everywhere, then possibly, however all of the theorems expressing list.permutation in terms of permutations of pieces of itself only come after all the main lemmas are proven, so it's no good for proving the theorem itself

#### Mario Carneiro (Aug 09 2021 at 10:20):

I think the key lemma that is actually true about `list.permutations`

and doesn't need `~`

is this one:

```
theorem permutations_append (is ts : list α) :
permutations (is ++ ts) = (permutations is).map (++ ts) ++ permutations_aux ts is.reverse :=
```

#### Mario Carneiro (Aug 09 2021 at 10:27):

In terms of the description up thread, `permutations_aux`

is defined as an append of a bunch of `grouping`

s, satisfying the recursion `permutations_aux (t :: ts) is = grouping ts t is ++ permutations_aux ts (t :: is)`

, so this suggests that you can also collect the groupings from the left, to define `permutations_left (t :: is) ts = permutations_left is (t :: ts) ++ grouping ts t is`

such that `permutations_left ts is ++ permutations_aux ts is = permutations (ts ++ is.reverse)`

. Then observe that every element of `permutations_left`

is supposed to fix `ts`

, so it can be factored as `permutations_left is ts = (???).map (++ ts)`

, and by great good luck (or simple consideration of the defining equation) `???`

turns out to be `permutations is`

itself, so you get this lovely equation

#### Mario Carneiro (Aug 09 2021 at 10:31):

If you plug in `ts = [t]`

, it simplifies to this slightly awkward theorem (cut from the final version):

```
theorem permutations_concat (t) (ts : list α) :
permutations (ts ++ [t]) = (permutations ts).map (++ [t]) ++
ts.reverse.permutations.bind (λ ys, (permutations_aux2 t [] [] ys id).2) :=
```

The `ts.reverse.permutations`

that occurs here is why `list.permutations`

has such terrible equations, because it's reversing the permutations for some of it and not for other parts, so it's hard to see what this does until you already have `perm.permutations`

#### Mario Carneiro (Aug 09 2021 at 10:35):

but if you assume that `ts.reverse.permutations`

is a permutation of `ts.permutations`

then this simplifies to

```
theorem permutations_perm_lem1 (t) (ts : list α)
(h : permutations ts ~ ts.reverse.permutations) :
permutations (ts ++ [t]) ~ ts.permutations.bind (permutations'_aux t) :=
```

because `permutations'_aux t ys = (permutations_aux2 t [] [] ys id).2 ++ [ys ++ [t]]`

, and at this point we are basically done because this is the defining equation for `permutations'`

(and we can prove `perm.permutations'`

directly without too much trouble)

#### Eric Wieser (Aug 09 2021 at 10:39):

This is excellent, thanks Mario!

#### Yakov Pechersky (Aug 09 2021 at 11:31):

Wonderful, thanks Mario! In particular I like the double induction on the length of ts and then the reverse induction.

Last updated: Aug 03 2023 at 10:10 UTC