module EqRes where open import Algebra.Structures open import Data.Nat open import Data.Nat.Properties open import Data.Vec open import Relation.Binary.PropositionalEquality import Relation.Binary.EqReasoning as EqR Matrix : Set -> ℕ -> ℕ -> Set Matrix A m n = Vec (Vec A m) n transpose : forall {A m n} -> Matrix A m n -> Matrix A n m transpose [] = replicate [] transpose (v ∷ vs) = zipWith _∷_ v (transpose vs) unitMatrix : forall {n} -> Matrix ℕ n n unitMatrix {zero} = [] unitMatrix {suc y} = (1 ∷ replicate 0) ∷ map (_∷_ 0) unitMatrix transpose-map : forall {A m n} -> (x : A) -> (vs : Matrix A m n) -> transpose (map (_∷_ x) vs) ≡ (replicate x) ∷ transpose vs transpose-map x [] = ≡-refl transpose-map x (v ∷ vs) = ≡-cong (zipWith _∷_ (x ∷ v)) (transpose-map x vs) zipVec : forall {A m n} -> (x : A) -> (vs : Matrix A m n) -> zipWith _∷_ (replicate x) vs ≡ map (_∷_ x) vs zipVec x [] = ≡-refl zipVec x (v ∷ vs) = ≡-cong (_∷_ (x ∷ v)) (zipVec x vs) transpose-unit : forall {n} -> transpose (unitMatrix {n}) ≡ unitMatrix {n} transpose-unit {zero} = ≡-refl transpose-unit {suc y} = let open EqR (≡-setoid (Matrix ℕ (suc y) (suc y))) in begin transpose (unitMatrix {suc y}) ≡⟨ byDef ⟩ transpose ((1 ∷ replicate 0) ∷ map (_∷_ 0) (unitMatrix {y})) ≡⟨ byDef ⟩ zipWith _∷_ (1 ∷ replicate 0) (transpose (map (_∷_ 0) (unitMatrix {y}))) ≡⟨ ≡-cong (zipWith _∷_ (1 ∷ replicate 0)) (transpose-map 0 (unitMatrix {y})) ⟩ zipWith _∷_ (1 ∷ replicate 0) ((replicate 0) ∷ transpose (unitMatrix {y})) ≡⟨ byDef ⟩ (1 ∷ replicate 0) ∷ (zipWith _∷_ (replicate 0) (transpose (unitMatrix {y}))) ≡⟨ ≡-cong (_∷_ (1 ∷ replicate 0)) (zipVec 0 (transpose (unitMatrix {y}))) ⟩ (1 ∷ replicate 0) ∷ (map (_∷_ 0) (transpose (unitMatrix {y}))) ≡⟨ ≡-cong (\m -> (1 ∷ replicate 0) ∷ (map (_∷_ 0) m)) (transpose-unit {y}) ⟩ (1 ∷ replicate 0) ∷ (map (_∷_ 0) (unitMatrix {y})) ≡⟨ byDef ⟩ unitMatrix {suc y} ∎ -- trans (cong (vecZipWith _::_ (1 :: vec 0)) -- (transpose-map 0 (unitMatrix {y}))) -- (cong (_::_ (1 :: vec 0)) -- (trans (zipVec 0 (transpose (unitMatrix {y}))) -- (cong (vecMap (_::_ 0)) -- (transpose-unit {y}))))