how to prove `(a.insertionSort).all p = a.all p`

Stream: new members

[Zihao Zhang]

import Aesop
theorem insertionSort_preserves_all (a : Array Int) (p : Int → Bool) :
    (a.insertionSort).all p = a.all p:= by

[Vlad Tsyrklevich]

There is no API at all provided for Array.insertionSort so this seems like you want some basic API. It would be easy if you could e.g. reduce it to another sorting function that does have basic API like in the below:

import Aesop
import Mathlib

theorem Array_insertionSort_eq_List_insertionSort (a : Array Int) :
    a.insertionSort = (a.toList.insertionSort (· < ·)).toArray := by
  sorry

theorem insertionSort_preserves_all (a : Array Int) (p : Int → Bool) :
    (a.insertionSort).all p = a.all p := by
  rw [Array_insertionSort_eq_List_insertionSort]
  rw [List.all_toArray, ← Array.all_toList]
  apply List.Perm.all_eq
  exact List.perm_insertionSort (· < ·) a.toList

[Wrenna Robson]

Note that Mathlib does have List.insertionSort and that may not be a bad place to start to work out what API is necessary.

[Wrenna Robson]

Ah I guess you are saying this! But it would be nice if at least Batteries supported Array.insertionSort.

[Jakub Nowak]

Vlad Tsyrklevich said:

There is no API at all provided for Array.insertionSort so this seems like you want some basic API. It would be easy if you could e.g. reduce it to another sorting function that does have basic API like in the below:

import Aesop
import Mathlib

theorem Array_insertionSort_eq_List_insertionSort (a : Array Int) :
    a.insertionSort = (a.toList.insertionSort (· < ·)).toArray := by
  sorry

theorem insertionSort_preserves_all (a : Array Int) (p : Int → Bool) :
    (a.insertionSort).all p = a.all p := by
  rw [Array_insertionSort_eq_List_insertionSort]
  rw [List.all_toArray, ← Array.all_toList]
  apply List.Perm.all_eq
  exact List.perm_insertionSort (· < ·) a.toList

I've tried filling in the sorry, but it seems like it's impossible because Array.insertionSort.traverse is private.

[Wrenna Robson]

Yeah I think you might have to prove it in Init.Data.Array.InsertionSort

[Jakub Nowak]

Wrenna Robson said:

Yeah I think you might have to prove it in Init.Data.Array.InsertionSort

Well, you can't either. Because List.insertionSort is in Mathlib.