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.
Proof. intros HMMt HMtMtt. unfold transp. induction M.
But I can’t even prove the nil case!