# Proving transpose function: now refactored!

I am still trying to understand Coq and working on a matrix transpose algorithm. I have refactored what I had before:

``````Require Import Ensembles.
Require Import ZArith.
Require Extraction.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.

From Coq Require Import List.

Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Definition vector := list.

Definition matrix A := list (vector A).

(*M = [ (v1) , (v2), (v3), ..., (vn) ]*)
Definition column A (M:matrix A) (i:nat) : list A := nth i M nil.

Fixpoint row A (M:matrix A) (i:nat) (bottom: A) : list A :=
match M with
| nil => nil
| v1::M => (nth i v1 bottom)::(row A M i bottom)
end.

Definition transp A (M:matrix A) (Mt:matrix A) :=
forall bottom, forall i,
column A M i = row A Mt i bottom /\
row A M i bottom = column A Mt i.

Theorem transp_transp_eq A M Mt Mtt:
transp A M Mt ->
transp A Mt Mtt ->
M = Mtt.
``````

However, I don’t know how to discharge a proof about my theorem. I’ve tried a lot of different tactics, but I can’t exactly figure out what to do.

I have

``````Proof.
intros HMMt HMtMtt.
unfold transp.
induction M.
``````

But I can’t even prove the nil case!

1 Like

The definitions do not seem to match what you have in mind:

``````Eval compute in (column nat [] 1).    (* = [] : list nat *)
Eval compute in (row nat [] 1 23).    (* =  : list nat *)
``````

so that you can prove: `~ transp nat [] []`.

proof
``````Lemma not_transp : ~ transp nat [] [].
Proof.
unfold transp; intros Ht.
specialize Ht with 23 1 as [Hc Hr].
unfold column in Hc; simpl in Hc.
inversion Hc.
Qed.
``````

Just a little hint: I think you should enforce that your `list (list A)` actually represents an `m x n` matrix. First, you could define a function `isMatrix (A : matrix) (m n : nat) : bool` (e.g. using `List.Forall` and `List.length`).Then define a function `get (A : matrix) (i j : nat) : option A` (e.g. using `List.nth_error`) and show that it always returns a value if the indexes are ‘in range’. You could try to proof that if you have a `m x n` matrix, inverting it makes an `n x m` matrix. Prove that two matrixes are equal if and only if they contain the same elements, using the function `get` for all in-range coordinates. Finally, the crutial property for transpose is that `get (transpose M) m n = get M n m` (if `n, m` are in-range).

(I always forget whether `n` or `m` is the number of columns / rows, but this is up to you to define.)

An alternative approach is to use `Vector.t`, which is a list of fixed length (see my last post). Unfortunately, using this depdent data type can be a bit complicated for beginners, because the standard library lacks a lot of useful definitions and lemmas.

1 Like

After you destruct `Mt`, can you prove the case where both matrices are nil, and show that "M = nil and Mt <> nil` is impossible? If not, there might be a bug in the definitions…

`nth` is 0 based, so those `Eval compute` don’t seem to be actual bugs.
Similarly, `~ transp nat [] []` seems correct, as `[] []` is not the transpose of itself (it’s not even square!). Matrix `[[1 2]] [[2 1]]` is its own transpose (because it’s symmetrical), so that seems a better testcase?

On the other hand, I’m not sure that letting `i` range on all numbers (as oppose to valid indexes) is good in the definition of `transp`.
And if you avoid that (say, by using @mwuttke97’s ideas) you can make `transp` decidable (aka, a function that returns a boolean that tells you whether the proposition holds); even better, you could have a function that computes the transpose of a matrix.

EDIT: striked through nonsense, thanks @olaure01 for patiently noticing…

Thank you so much for this! You’ve all been really helpful. I need to read and digest, but I don’t want to wait until I understood to say thank you ``````Require Import Ensembles.
Require Import ZArith.
Require Extraction.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.
From Coq Require Import List.
Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

(** The spec bit: matrices like in a textbook *)
Definition vector := list.
Definition matrix A := list (vector A).
(*M = [ (v1) , (v2), (v3), ..., (vn) ]*)
Definition column A (M:matrix A) (i:nat) : list A := nth i M nil.
Fixpoint row A (M:matrix A) (i:nat) (bottom: A) : list A :=
match M with
| nil => nil
| v1::M => (nth i v1 bottom)::(row A M i bottom)
end.
Definition transp A (M Mt:matrix A) :=
forall bottom, forall i,
column A M i = row A Mt i bottom /\
row A M i bottom = column A Mt i.

Lemma eq_cols_eq_rows_implies_eq A M1 M2 :
(forall i, column A M1 i = column A M2 i) ->
(forall bottom, forall i, row A M1 i bottom = row A M2 i bottom) ->
M1 = M2.
Proof.
intros Hc Hr.
unfold column in *.

Theorem transp_transp_eq A M Mt Mtt (bottom : A) :
transp A M Mt ->
transp A Mt Mtt ->
M = Mtt.
Proof.
intros HMMt HMtMtt.
unfold transp in *.
generalize (HMMt bottom); clear HMMt; intro HMMt.
generalize (HMtMtt bottom); clear HMtMtt; intro HMtMtt.

apply eq_cols_eq_rows_implies_eq; auto.

intro i.
generalize (HMMt i); intros [H1 H2].
rewrite H1.
generalize (HMtMtt i); intros [H3 H4].
rewrite H4.
auto.
intuition.

Qed.

(** The program part: an algorithm to compute the transpose *)
Fixpoint maptl A (l: matrix A) : matrix A:=
match l with
| nil => nil
| nil :: t => maptl A t
| (a :: r) :: t  => r :: (maptl A t)
end.
Fixpoint maphd A (l: matrix A) : (list A):=
match l with
| nil => nil
| nil :: t => maphd A t
| (a :: r) :: t  => a :: (maphd A t)
end.
Definition size A (l : matrix A) : nat := fold_right (fun b a => S (length b + a)) 0 l.
Program Fixpoint transp_eval A (l: matrix A) { measure (size A l)} : matrix A :=
match l with
| nil => nil
| nil :: t => transp_eval A t
| (a :: r) :: t => (a :: maphd A t) :: transp_eval A (r :: maptl A t)
end.
Next Obligation.
Theorem program_respects_spec :
forall A M Mt, Mt = transp_eval A M -> transp A M Mt.

Proof.

unfold transp in *.
intuition.
rewrite H.
unfold column.
unfold transp_eval.

``````

Is what I now have. I can’t quite manage to finish off the proofs though, although I think they are all now in reasonable shape to be finished!

Sorry if my notations were not clear, but I still think your definition of `transp` is not what you want, since using this definition you get:

``````Eval compute in (column nat [] 1).   (* = [] : list nat *)
Eval compute in (row nat [] 1 9).    (* =  : list nat *)
Goal ~ transp nat [] [].
Proof.
unfold transp; intros Ht.
specialize Ht with 9 1 as [Ht _].
unfold column in Ht; simpl in Ht.
inversion Ht.
Qed.
``````

Meaning that the matrix (3) containing only 1 cell (1 line and 1 column) would not be its own transpose.

1 Like

@olaure01’s examples indeed show valid bugs — I was very confused.

Ah, ok. I’m not sure I understand where I’ve gone wrong, I don’t suppose you can see anything obvious? Regardless, thanks for your help I think yes: for all indexes `i` and default values `bottom`, `column A M i = row A Mt i bottom ` requires the `i`-th column of `M` to coincide with the `i`-th row of `Mt`. That must also hold if `i` is out of bounds, but then the two functions return different error codes, as shown in @olaure01’s examples — for instance,
`column nat [] 1` is the empty list `[]`, but `row nat [] 1 bottom` is `[bottom]` (their last example has `bottom = 9`); in particular, `transp nat [] []` implies that `[] = [bottom]` for any natural value bottom, which is very absurd.

To fix that, `transp` needs to use the size of the matrix, and to use `forall i, 0 <= i < size` to only quantify over valid indexes. That’s why various answers talk about the size of the matrix, and ensure the matrix does have a valid size — see e.g. Proving transpose function: now refactored! - #3 by mwuttke97.