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.
Extraction Language Haskell.
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.
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.
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 [[12]] [[12]] seems correct, as [[12]] [[12]] 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…
Require Import Ensembles.
Require Import ZArith.
Require Extraction.
Extraction Language Haskell.
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 *.
Admitted.
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.
Admitted.
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.
Admitted.
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!
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 [[3]] 1 is the empty list [], but row nat [[3]] 1 bottom is [bottom] (their last example has bottom = 9); in particular, transp nat [[3]] [[3]] 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.
striked through nonsense, thanks 
