perm of permutations

Stream: general

[Eric Wieser]

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]

(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]

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]

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]

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]

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]

Is laziness relevant to lean?

[Bhavik Mehta]

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]

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

[Eric Wieser]

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

[Bhavik Mehta]

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]

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]

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]

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

[Eric Wieser]

What does "is natural" mean there?

[David Wärn]

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

[David Wärn]

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]

Where the ... is l.permutations.map (\lam l, l.map f)?

[Eric Wieser]

That does seem like an easier result to prove

[Eric Wieser]

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]

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

[Mario Carneiro]

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]

all the key lemmas about permutations_aux are proven at the end of data.list.perm

[Mario Carneiro]

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]

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]

Those proofs are gnarly, pattern matching on _match_1

[Eric Wieser]

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

[Yakov Pechersky]

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]

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]

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]

(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]

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]

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]

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]

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]

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]

I take it that means it is false

[Yakov Pechersky]

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]

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]

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]

slim_check doesn't use #eval

[Mario Carneiro]

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]

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]

Edit: no, #eval tells me its false

[Eric Wieser]

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

[Mario Carneiro]

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]

Ah, it's the fact that the second argument to grouping is reversed that threw me off

[Eric Wieser]

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]

I assume the .reverse in there for some efficiency reason regarding assembling lists

[Eric Wieser]

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]

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]

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]

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]

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]

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]

Stated backwards to match docs#list.permutations_aux2_append

[Mario Carneiro]

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]

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]

Isn't map_permutations_aux2' the one that eliminates f?

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

Do you have any other open files?

[Eric Wieser]

They're all "plaintext" files

[Eric Wieser]

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

[Eric Wieser]

They're also all unsaved anonymous buffers

[Johan Commelin]

Aha

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

Maybe CI can build for me: #8198

[Mario Carneiro]

Done in #8587 :tada:

[Mario Carneiro]

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]

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

[Yaël Dillies]

@Yakov Pechersky, it's Christmas before December!

[Yaël Dillies]

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]

no, because list.permutations' is not equal to list.permutations

[Mario Carneiro]

it is a complicated permutation thereof

[Mario Carneiro]

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]

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]

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]

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]

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]

This is excellent, thanks Mario!

[Yakov Pechersky]

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