# How to prove this correctness principle of transposition of lists of lists in Coq?

I have defined the function transpose as follows:

Fixpoint transpose {X : Type} (len : nat) (tapes : list (list X)) : list (list X) :=
match tapes with
| [] => repeat [] len
| t :: ts => zipWith cons t (transpose len ts)
end.


where

Definition zipWith {X Y Z} (f : X -> Y -> Z) (xs : list X) (ys : list Y) : list Z :=
map (fun '(x, y) => f x y) (combine xs ys).


Since the 0 x n matrix is encoded as [], I use the additional parameter len to denote the number n.

I define the function

Definition ij_error {X : Type} (i j : nat) (l : list (list X)) : option X :=
match nth_error l i with
| Some l' => nth_error l' j
| None => None
end.


Note that nth_error and combine are Library Functions

I would like to prove the following lemma, but I am not sure how I should do so. The large number of variables for inducting, and the nested cases is quite overwhelming. Any help is appreciated.

Lemma transpose_spec {X : Type} : forall len (tapes : list (list X)),
(forall t,
In t tapes -> length t = len)
-> forall i j,
ij_error i j tapes = ij_error j i (transpose len tapes).
Proof.


Note: I have proven a number of other lemmas about transpose and zipWith which may be useful.

I think you should not be scared. While doing the induction, we will discover the lemmas you are still missing to finish the proof.

Lemma transpose_spec {X : Type} : forall len (tapes : list (list X)),
(forall t,
In t tapes -> length t = len)
-> forall i j,
ij_error i j tapes = ij_error j i (transpose len tapes).
Proof.
induction tapes as [|l tapes IHt]; simpl; intros H.
- intros i j; rewrite ij_error_nil.
(* missing lemmas about ij_error and repeat *)
- induction i as [|i IHi].
+ intros j.
(* missing lemmas about ij_error 0 j and ij_error i 0 *)
+ (* missing lemmas about ij_error (S i) j and ij_error j (S i *)

• Did you manage to do it with a single induction on tapes? (maybe Hi is not used so a simple destruct i is enough)
• You are right. destruct i was enough. Apr 17 at 16:16