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.