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

Question

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.
Admitted.

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

Answer 1

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 *)
  admit.
- induction i as [|i IHi].
  + intros j.
    (* missing lemmas about ij_error 0 j and ij_error i 0 *)
    admit.
  + (* missing lemmas about ij_error (S i) j and ij_error j (S i *)
    admit.
Qed.

Good luck!