existence of equiv mapping nodup same length lists

Stream: Is there code for X?

[Kayla Thomas]

Is there a theorem or set of theorems in mathlib that would help to prove this?

theorem foo (l1 l2 : list ℕ) (h1 : l1.length = l2.length) (h2 : l1.nodup) (h3 : l2.nodup) :
  ∃ f : ℕ ≃ ℕ, l1.map f = l2

[Kayla Thomas]

Title should read "equiv" not "function". Not sure how to change it.

[Anne Baanen]

I couldn't find anything precisely matching your description. The closest I found is you might be able to compose two usages of docs#list.nodup.nth_le_equiv_of_forall_mem_list.

[Yakov Pechersky]

Maybe there is something that connects equiv.perm and list.perm that you could use.

[Kyle Miller]

Here's a crude proof of a slight generalization of this:

import tactic
import logic.equiv.fintype

theorem foo {α : Type*}
  (l1 l2 : list α) (h1 : l1.length = l2.length) (h2 : l1.nodup) (h3 : l2.nodup) :
  ∃ f : α ≃ α, l1.map f = l2 :=
begin
  classical,
  induction l1 with x l1 ih generalizing l2,
  { rw [list.length, eq_comm] at h1,
    cases list.eq_nil_of_length_eq_zero h1,
    use equiv.refl _,
    refl, },
  cases l2 with y l2,
  { cases h1 },
  simp only [list.length, add_left_inj] at h1,
  simp only [list.nodup_cons] at h2 h3,
  obtain ⟨f, hf⟩ := ih h2.2 l2 h1 h3.2,
  have : f x ∉ l2 := by simp [← hf, h2],
  use f.trans (equiv.swap y (f x)),
  simp only [list.map, equiv.coe_trans, function.comp_app, equiv.swap_apply_right,
    eq_self_iff_true, true_and],
  rw ← hf,
  refine list.map_congr (λ z hz, _),
  simp only [function.comp_app],
  apply equiv.swap_apply_of_ne_of_ne,
  { rintro rfl,
    apply h3.1,
    simpa only [←hf, list.mem_map, embedding_like.apply_eq_iff_eq, exists_eq_right] using hz },
  { intro h,
    apply this,
    rw [← h, ← hf],
    simpa using hz }
end

[Junyan Xu]

Interesting, wasn't expecting an inductive proof using equiv.swap. Was thinking of a proof using docs#cardinal.mk_compl_eq_mk_compl_finite, and docs#list.nodup.nth_le_equiv_of_forall_mem_list will be helpful there.

[Yakov Pechersky]

Just spitballing here, what's wrong with an explicit construction here? I'm hitting a roadblock in proving, I feel like I forgot to capture some edge case:

 refine ⟨⟨
   λ x, if h : x ∈ l1 then l2.nth_le (l1.index_of x) ((list.index_of_lt_length.mpr h).trans_le h1.le) else x,
   λ x, if h : x ∈ l2 then l1.nth_le (l2.index_of x) ((list.index_of_lt_length.mpr h).trans_le h1.ge) else x,
   _, _⟩, _⟩,

[Kevin Buzzard]

Yeah I feel like there might even be a "minimal equiv", which does what it has to do on l1, closes every chain x1 -> x2 -> x3 -> ... -> xn by sending xn to x1, and then is the identity away from l1 union l2 (but Yakov I think that your code as it stands has problems with l1=[1] and l2=[2] because it sends 1 to 2 and also 2 to 2)

[Eric Wieser]

I'm pretty sure I saw a PR linking list.perm to equiv.perm

[Kayla Thomas]

Thank you for all of the suggestions. I'm thinking through how to proceed.

[Kayla Thomas]

Anne Baanen said:

I couldn't find anything precisely matching your description. The closest I found is you might be able to compose two usages of docs#list.nodup.nth_le_equiv_of_forall_mem_list.

I'm not sure I understand what this theorem says. What would l and αbe in this instance? Is α = ℕ? If so, can a list be infinite and hold all of the elements of ℕ?

[Kevin Buzzard]

No, lists can't be infinite. This lemma can be used to give a bijection between l1 and l2 but there's still more work to do after that.

[Kayla Thomas]

Ok. Thank you.

[Kayla Thomas]

Would the rest consist of getting a bijection between (ℕ - l1) and (ℕ - l2) and then somehow combining the two bijections?

[Kevin Buzzard]

Right, but there's already a full proof above, written after Anne's suggestion

[Kayla Thomas]

I was just curious if it could be made more succinct.

[Kevin Buzzard]

That's an NP hard problem but the answer is probably "yes".