Perm on the other side of sublist

Stream: Is there code for X?

[Yaël Dillies]

docs#list.subperm is defined as ∃ l ~ l₁, l <+ l₂. It's obviously equivalent to ∃ l ~ l₂, l₁ <+ l, but does mathlib know it? I did not manage to find it nor to prove it myself.

import data.list.perm

namespace list
variables {α : Type*} {l₁ l₂ : list α} {a : α}

lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l ~ l₂, l₁ <+ l := sorry

end list

[Yaël Dillies]

In general, I find it very hard to work with list.perm. Do we have any API about how it relates to reordering the elements of the list?

[Yaël Dillies]

@Mario Carneiro, this is probably a question for you.

[Mario Carneiro]

mathlib does know it

[Mario Carneiro]

Do we have any API about how it relates to reordering the elements of the list?

this is a confusing statement for me, because it is literally the definition of "reordering the elements of the list"

[Yaël Dillies]

list.perm means "The two lists are related by a series of local permutations", as opposed to "The two lists are related by a global permutation". If I had a global permutation, proving list.subperm_iff and using list.perm in general would be much easier.

[Mario Carneiro]

I'm not sure that's a distinction that exists

[Mario Carneiro]

any permutation is expressible as a series of local permutations, and list.perm is a Prop

[Mario Carneiro]

there are loads of theorems that characterize list.perm however you care to think about it

[Mario Carneiro]

but I know that the theorem you are looking for is proved quite early as part of the setup

[Yaël Dillies]

Then can I get an actual reordering of the elements from a l₁ ~ l₂ hypothesis? Like, a permutation σ : equiv.perm (fin l₁.length) such that ∀ i, l₁.get (σ i) = l₂.get i?

[Mario Carneiro]

surely that theorem is somewhere in the equiv.perm file

[Mario Carneiro]

but keep in mind that this reasoning is not in line with the dependency structure, we wouldn't be able to use it in data.list.perm

[Yaël Dillies]

Really? equiv.perm is very low in the import hierarchy now.

[Yaël Dillies]

Mario Carneiro said:

surely that theorem is somewhere in the equiv.perm file

What is "the" file? Having a cursory read through logic.equiv.defs, group_theory.perm.basic, group_theory.perm.list didn't yield anything.

[Yaël Dillies]

Mario Carneiro said:

mathlib does know it

At any rate, if you have an answer to my original question, I'll take it :grinning:

[Mario Carneiro]

do you want a lean 3 proof?

[Yaël Dillies]

Yes please, I'm reviving #10865 so I don't have the luxury to go to Lean 4 just yet.

[Mario Carneiro]

import data.list.perm

namespace list
variables {α : Type*} {l₁ l₂ : list α} {a : α}

lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l ~ l₂, l₁ <+ l :=
begin
  refine ⟨_, λ ⟨l, h₁, h₂⟩, h₂.subperm.trans h₁.subperm⟩,
  rintro ⟨l, h₁, h₂⟩,
  obtain ⟨l', h₂⟩ := h₂.exists_perm_append,
  exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩,
end

end list

[Yaël Dillies]

Aaah, exists_perm_append is the ingredient I was missing. Thanks Mario!