perm equal to sorted list indices

Stream: new members

[Evan Lohn]

Hi all, can someone point me in the right direction for the following proof:

import tactic.linarith

variables (α : Type*)

lemma mergesort_length_preserve (lst: list α) {lt: α → α → Prop} [decidable_rel lt]: (list.merge_sort lt lst).length = lst.length :=
begin
  exact list.perm.length_eq (list.perm_merge_sort lt lst),
end

lemma ind_in_sorted_list (lst: list α) (ind: fin (lst.length)) (lt: α → α → Prop) [∀ v1, decidable_pred (lt v1)]:
↑ind < (list.merge_sort lt lst).length :=
begin
  rw mergesort_length_preserve,
  exact fin.is_lt ind,
end

lemma exists_perm_eq_sort (lst: list α) (lt: α → α → Prop) [∀ v1, decidable_pred (lt v1)]:
∃ (perm : equiv.perm (fin (lst.length))), ∀ ind: fin (lst.length), lst.nth_le (perm ind) (fin.is_lt _) = (list.merge_sort lt lst).nth_le ind (ind_in_sorted_list _ lst ind lt) :=
begin
  sorry
end

Namely, I'm not sure how to instantiate the ∃ perm. My idea was to sort a modified version of the original list where each element is a pair that also contains the original list index and reconstruct the index permutation from that... is there a better way?

P.S. In case it's relevant, I need something of this form because my proofs for my larger project require me to show that sorting the rows of a matrix is equivalent to some permutation of the matrix's rows.

[Patrick Johnson]

Not sure what the best way to prove it is (we probably have something along those lines in mathlib, although I don't know what), but as an answer to your question "How to instantiate the ∃ perm" - you can write a simple function that takes two list and some index i in the first list and returns the index of the same element in the second list. In case there are duplicates, you would subtract the number of equal elements previously encountered. But it would be painful to prove that it is a bijection.

Another way would be to use an inductive data type to represent list permutations:

import tactic.induction

inductive {u} perm {α : Type u} : list α → list α → Type (u+1)
| nil   : perm [] []
| cons  : Π (x : α) {l₁ l₂ : list α}, perm l₁ l₂ → perm (x::l₁) (x::l₂)
| swap  : Π (x y : α) (l : list α), perm (y::x::l) (x::y::l)
| trans : Π {l₁ l₂ l₃ : list α}, perm l₁ l₂ → perm l₂ l₃ → perm l₁ l₃

noncomputable def perm_of_list_perm {α : Type*} {xs ys : list α} (h : xs ~ ys) : perm xs ys :=
begin
  refine (_ : nonempty _).some, induction' h,
  { exact ⟨perm.nil⟩ },
  { cases ih, exact ⟨perm.cons x ih⟩ },
  { exact ⟨perm.swap x y l⟩ },
  { cases ih_h, cases ih_h_1, exact ⟨perm.trans ih_h ih_h_1⟩ },
end

Then you can obtain a prop permutation from list.perm_merge_sort and convert it to data using perm_of_list_perm. Then you can implement a function that constructs equiv.perm from perm recursively. Finally, you will need to prove that such permutation satisfies the nth_le relation that you need.

As a side note, when using nth_le in a lemma statement, you don't need to actually prove the requirement in order to invoke nth_le. You can simply assert that a proof exists. Your lemma statement can be simplified to:

lemma exists_perm_eq_sort (lst : list α) (lt : α → α → Prop) [Π (v1 : α), decidable_pred (lt v1)] :
  ∃ (perm : equiv.perm (fin lst.length)), ∀ (ind : fin lst.length), ∃ h₁ h₂,
  lst.nth_le (perm ind) h₁ = (list.merge_sort lt lst).nth_le ind h₂ :=
begin
  sorry
end

[Kyle Miller]

The module where docs#tuple.sort is might be helpful

[Kyle Miller]

You could pass it the fin version of docs#list.nth_le (I forget what that is, if there is one)