## 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

#### 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]  -- [[2, 1, 3, 4]]
#eval grouping 3  [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  [2, 1] is determined.

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

grouping 3  [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  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 groupings, 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