List.transpose for proofs

Stream: Is there code for X?

[Daniel Weber]

docs#List.transpose is defined using monads, and it seems quite hard to prove stuff for it (there is also no API for it). In my particular case I can prove all of the lists have the same size which isn't zero, and I need the theorems that the transpose is involutive, and that the length of each list in the transpose is equal to the length of the original list. What's the best way to do that?

[Kim Morrison]

You could replace the definition of List.transpose.

[Daniel Weber]

I managed to do stuff using the definition:

def List.transpose {α : Type*} : List (List α) → List (List α)
| [] => []
| [a] => a.map ([·])
| a :: b => zipWith cons a (transpose b)

would this change to the definition be accepted on Batteries? Should it be a different definition (it handles lists which don't have the same length differently), either on Batteries or Mathlib?

[Kim Morrison]

Do you actually need the singleton case?

[Kim Morrison]

Can you describe how it differs from the current version? Being on involution on tableaux (i.e. the lengths are non-increasing) is a pretty useful property, and I'd prefer to have that.

[Kim Morrison]

It may be worth running a benchmark as well, but your version seems pretty reasonable.

[Daniel Weber]

Currently the length of transpose is the length of the longest list in the input, and for each index it takes the value at that index from all lists in the inputs which are long enough. For example [[1, 2, 3], [4], [5, 6], [7, 8, 9]].transpose = [[1, 4, 5, 7], [2, 6, 8], [3, 9]]. On the other hand, the length of the list this returns is the shortest list in the input, and it drops values from lists that are too long, e.g. [[1, 2, 3], [4], [5, 6], [7, 8, 9]].transpose = [[1, 4, 5, 7]]

[Daniel Weber]

Kim Morrison said:

Do you actually need the singleton case?

It is the base case of the recursion, as zipWith cons a [] = []

[Kim Morrison]

Oh, in that case I definitely prefer the old behaviour, for the non-increasing length case.

[Daniel Weber]

So should my definition be added to Mathlib with a different name?

[Mario Carneiro]

what's the motivation for this different definition if you are giving it a rectangle anyway?

[Daniel Weber]

I found it easier to use because I have ∀ v ∈ l, l.transpose'.length ≤ v.length and l.transpose'[i] = l.pmap (·[i]'·) _ without having to prove that everything has the same length

[Eric Wieser]

Your proposed definition doesn't preserve all inputs in the output:

import Mathlib

def List.transpose' {α : Type*} : List (List α) → List (List α)
| [] => []
| [a] => a.map ([·])
| a :: b => zipWith cons a (transpose b)

/-- info: [[4, 5, 7], [6, 8], [9]] -/
#guard_msgs in
#eval [[4], [5, 6], [7, 8, 9]].transpose

/-- info: [[4, 5, 7]] -/
#guard_msgs in
#eval [[4], [5, 6], [7, 8, 9]].transpose'

[Daniel Weber]

Yes, I'm aware - it truncates them if the lengths aren't equal

[Giacomo Stevanato]

Not sure if this is easier to understand or work with, but it should match the behaviour of the current List.transpose

import Mathlib

def List.transpose' {α : Type*} (l : List (List α)) : List (List α) := l.foldr aux []
where
  aux : List α → List (List α) → List (List α)
  | [],  acc => acc
  | l, [] => l.map fun a => [a]
  | (a :: b), (x :: y) => (a :: x) :: (aux b y)