Proving matrix transpose function

Using Coq
3

I am answering this part of your question:

It is problematic, because you can’t evaluate the function, because the computation gets stuck. It gets stuck, because the function can’t be defined by measure (length l). Actually, the length is the same in each recursive call! What you want is measure (size l), where size l returns the number of elements in the matrix:

From Coq Require Import List.
Import ListNotations.
From Coq Require Import Program.Wf.
From Coq Require Import Lia.

Set Implicit Arguments.

Section Mat.

  Variable A : Type.

  Fixpoint maphd (l: list (list A)) : (list A):=
    match l with
    | nil => nil
    | nil :: t => maphd t
    | (a :: r) :: t => a :: (maphd t)
    end.

  Fixpoint maptl (l: list (list A)) : (list (list A)):=
    match l with
    | nil => nil
    | r :: t => tl r :: (maptl t)
    end.

  Definition size (l : list (list A)) : nat := fold_right (fun b a => S (length b + a)) 0 l.

  Lemma size_cons (x : list A) (l : list (list A)) :
    size (x :: l) = S (length x + size l).
  Proof. reflexivity. Qed.

  (* This lemma belongs into the stdlib! *)
  Lemma length_tl (X : Type) (l : list X) :
    length (tl l) = pred (length l).
  Proof. now destruct l. Qed.

  Lemma size_maptl_le (l : list (list A)) :
    size (maptl l) <= size l.
  Proof.
    induction l.
    - reflexivity.
    - cbn [maptl]. rewrite !size_cons, length_tl. lia.
  Qed.

  Program Fixpoint transp (l: list (list A)) { measure (size l)} : list(list A) :=
    match l with
    | nil => nil
    | nil :: t => transp t
    | (a :: r) :: t => (a :: maphd t) :: transp (maptl (r :: t))  
    end.
  Next Obligation.
    rewrite size_cons; cbn.
    pose proof size_maptl_le t.
    rewrite length_tl. lia.
  Qed.

End Mat.

(I took the maphd function from here).

For the verification: You should test your definition first! Now that we have given the right measure, you can compute the function using Eval cbv in (or equivalently Compute):

Section Test.

  Let test := [[1;2;3]; [4;5;6]].
  Eval cbv in transp test.
  (* = [[1; 4]; [3; 5]; [6]] *)

  Eval cbv in transp (transp test).
  (* = [[1; 3; 6]; [5]] *)

End Test.

That looks like there is a mistake in your definition. Or maybe I did something wrong in the definition of maptl. :thinking:

PS: It is sometimes a good idea to first implement a prototype of your algorithm in a functional PL like ocaml or Standard ML. This sometimes makes testing easier, in particular when you’re working with discrete data types. However, I often find it useful to ‘debug’ a function while proving it correct. :slight_smile: