Proof that matrix transpose is an involution.

matrix-transpose-involution.agda

module test where

open import Relation.Binary.PropositionalEquality
open import Data.Nat

infixr 5 _∷_ 

data Vec (A : Set) : ℕ -> Set where
  [] : Vec A 0
  _∷_ : {n : ℕ} -> A -> Vec A n -> Vec A (1 + n)

head : {A : Set} {n : ℕ} -> Vec A (1 + n) -> A
head (x ∷ _) = x

tail : {A : Set} {n : ℕ} -> Vec A (1 + n) -> Vec A n
tail (_ ∷ xs) = xs

map : {A B : Set} {n : ℕ} -> (A -> B) -> Vec A n -> Vec B n
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

Matrix : (A : Set) -> ℕ -> ℕ -> Set
Matrix A w h = Vec (Vec A w) h

transpose : {A : Set} {w h : ℕ} -> Matrix A w h -> Matrix A h w
transpose {A} {zero} m = []
transpose {A} {suc w} m = map head m ∷ transpose (map tail m)

theorem : {A : Set} {w h : ℕ} -> (m : Matrix A w h) -> m ≡ transpose (transpose m)
theorem [] = refl
theorem (c ∷ m) = trans (cong (_∷_ c) (theorem m)) (cong₂ _∷_ (lem₂ c m) (cong transpose (lem₁ c m)))
  where

    lem₁ : {A : Set} {w h : ℕ} (c : Vec A h) (m : Matrix A h w) -> transpose m ≡ map tail (transpose (c ∷ m))
    lem₁ {A} {w} {zero} c m = refl
    lem₁ {A} {w} {suc h} (x ∷ c) m = cong (_∷_ (map head m)) (lem₁ c (map tail m))

    lem₂ : {A : Set} {w h : ℕ} (c : Vec A h) (m : Matrix A h w) -> c ≡ map head (transpose (c ∷ m))
    lem₂ {A} {w} {zero} [] m = refl
    lem₂ {A} {w} {suc h} (x ∷ c) m = cong (_∷_ x) (lem₂ c (map tail m))