1
$\begingroup$

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.

$\endgroup$

1 Answer 1

3
$\begingroup$

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!

$\endgroup$
4
  • $\begingroup$ Thanks, that proof scheme worked out. I have updated the gist in case someone is curious $\endgroup$ Commented Apr 17, 2023 at 15:56
  • $\begingroup$ Did you manage to do it with a single induction on tapes? (maybe Hi is not used so a simple destruct i is enough) $\endgroup$
    – Lolo
    Commented Apr 17, 2023 at 16:08
  • $\begingroup$ You are right. destruct i was enough. $\endgroup$ Commented Apr 17, 2023 at 16:16
  • 1
    $\begingroup$ ssreflect version for OP or anyone else who would like it. $\endgroup$
    – djao
    Commented Apr 20, 2023 at 7:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.