Mat.idr

module Matrices


-- Vector stuff ~ maybe put Prelude.Vect

||| Dot product between numerical vectors
dot : Num a => Vect n a -> Vect n a -> a
dot w v = sum (zipWith (*) w v)

||| Numerical vector times a scalar of the appropriate type
vxs : Num a => Vect n a -> a -> Vect n a
vxs v s = map (* s) v

||| Tensor product for numerical vectors
ox : Num a => Vect n a -> Vect m a -> Vect (n * m) a
ox {n} {m} q w = zipWith (*) (oextend m q) (orep n w) where
  orep : {N : Nat} -> (M : Nat) -> Vect N a -> Vect (M * N) a
  orep M Q = concat $ replicate M Q
  oextend : (j : Nat) -> Vect k a -> Vect (k * j) a
  oextend {k} j w = concat $ map (replicate j) w

||| Vector addition
vPlus : Num a => Vect n a -> Vect n a -> Vect n a
vPlus v w = zipWith (+) v w

||| Vector subtraction
vMinus : Num a => Vect n a -> Vect n a -> Vect n a
vMinus v w = zipWith (-) v w

||| Squared-Norm of a numerical vector
sqNorm : Num a => Vect n a -> a
sqNorm v = sum $ map (\x => x*x) v

||| Make an n-dimensional vector from a function of Fin-n
vectorMaker : {n : Nat} -> (Fin n -> a) -> Vect n a
vectorMaker {n} f = map f (reverse $ allN n) where
  allN : (n : Nat) -> Vect n (Fin n)
  allN Z     = Nil
  allN (S n) = last :: (map weaken $ allN n)


-- Matrix stuff ~ maybe put in Prelude.Matrix

||| Matrix with n cols and m rows
Matrix : Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

||| Gets the specified row of a matrix. For cols use the vector function 'index'
getRow : Fin m -> Matrix n m a -> Vect n a
getRow fm q = map (index fm) q

||| Deletes the specified row of a matrix. For cols use the vector function 'deleteAt'
deleteRow : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
deleteRow f m = map (deleteAt f) m

||| Numerical matrix times scalar of the appropriate type
mxs : Num a => Matrix n m a -> a -> Matrix n m a
mxs m s = map (map (* s)) m

||| Matrix times a vector
mxv : Num a => Matrix n m a -> Vect n a -> Vect m a
mxv m v = vectorMaker (rowApply m v) where
  rowApply : Num b => {N,M : Nat} -> Matrix N M b -> Vect N b -> Fin M -> b
  rowApply mat v f = dot (getRow f mat) v

||| Matrix multiplication
mxm : Num a => Matrix k m a -> Matrix n k a -> Matrix n m a
mxm m1 m2 = map (mxv m1) m2

||| Tensor product for numerical matrices
otimes : Num a => Matrix w1 h1 a -> Matrix w2 h2 a -> Matrix (w1 * w2) (h1 * h2) a
otimes m1 m2 = zipWith ox (stepOne m1 m2) (stepTwo m1 m2) where
  stepOne : Matrix w1 h1 a -> Matrix w2 h2 a -> Matrix (w1 * w2) h1 a
  stepOne {w2} m1 m2 = concat $ map (replicate w2) m1
  stepTwo : Matrix w1 h1 a -> Matrix w2 h2 a -> Matrix (w1 * w2) h2 a
  stepTwo {w1} m1 m2 = concat $ (Vect.replicate w1) m2

||| Cast a standard Vect to a proper n x 1 matrix 
castCol : Vect n a -> Matrix 1 n a
castCol v = [v]

||| Cast a Vect to a 1 x n Matrix, i.e. a row
castRow : Vect n a -> Matrix n 1 a
castRow v = map (\x => [x]) v

||| Outer product of numerical vectors
outer : Num a => Vect n a -> Vect m a -> Matrix n m a
outer x y ?= (castRow x) `otimes` (castCol y)

||| Matrix addition
mPlus : Num a => Matrix n m a -> Matrix n m a -> Matrix n m a
mPlus m1 m2 = zipWith vPlus m1 m2

||| Matrix subtraction
mMinus : Num a => Matrix n m a -> Matrix n m a -> Matrix n m a
mMinus m1 m2 = zipWith vMinus m1 m2


---------- Proofs ----------

outer_lemma_1 = proof
  intros
  rewrite (multOneRightNeutral n)
  rewrite (multOneLeftNeutral m)
  trivial