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.
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.

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 [[12]] 1).    (* = [] : list nat *)
Eval compute in (row nat [[12]] 1 23).    (* = [23] : list nat *)

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

proof
Lemma not_transp : ~ transp nat [[12]] [[12]].
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.

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: :man_facepalming: 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 :slight_smile:

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!

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 [[3]] 1).   (* = [] : list nat *)
Eval compute in (row nat [[3]] 1 9).    (* = [9] : list nat *)
Goal ~ transp nat [[3]] [[3]].
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 :slight_smile:

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!.