@@ -0,0 +1,249 @@
7+infixl 1 \+\ -- Vector plus (mnemonic: V begins with '\'
8+infixl 1 /+/ -- Matrix plus M begins with '/')
9+infixl 1 \-\ -- Vector minus
10+infixl 1 /-/ -- Matrix minus
11+infixr 2 <.> -- Vector inner product
12+infixr 2 >< -- Vector outer product
13+infixr 2 <<>> -- Matrix commutator
14+infixr 2 >><< -- Matrix anticommutator
15+infixl 3 <\> -- row times a matrix
16+infixr 4 </> -- matrix times a column
17+infixr 5 <> -- matrix multiplication
18+infixr 7 \&\ -- vector tensor product
19+infixr 7 <&> -- matrix tensor product
21+-----------------------------------------------------------------------
23+-----------------------------------------------------------------------
25+||| Inner product of ring vectors
26+(<.>) : Ring a => Vect n a -> Vect n a -> a
27+(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
29+||| Scale a ring vector by the appropriate scalar
30+scale : Ring a => a -> Vect n a -> Vect n a
31+scale s v = map (<*> s) v
34+(\+\) : Ring a => Vect n a -> Vect n a -> Vect n a
35+(\+\) v w = zipWith (<+>) v w
37+||| Vector subtraction
38+(\-\) : Ring a => Vect n a -> Vect n a -> Vect n a
39+(\-\) v w = zipWith (<->) v w
41+||| Tensor multiply (⊗) ring vectors
42+(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
43+(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
44+ orep : (n : Nat) -> Vect m a -> Vect (n * m) a
45+ orep n v = concat $ replicate n v
46+ oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
47+ oextend n w = concat $ map (replicate n) w
50+zero : Monoid a => {d : Nat} -> Vect d a
51+zero {d} = replicate d neutral
53+||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
54+basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
55+basis i = replaceAt i unity $ zero
58+flat : RingWithUnity a => {d : Nat} -> Vect d a
59+flat {d} = replicate d unity
62+-----------------------------------------------------------------------
64+-----------------------------------------------------------------------
66+||| Matrix with n rows and m columns
67+Matrix : Nat -> Nat -> Type -> Type
68+Matrix n m a = Vect n (Vect m a)
70+||| Gets the specified column of a matrix. For rows use the vector function 'index'
71+getCol : Fin m -> Matrix n m a -> Vect n a
72+getCol fm q = map (index fm) q
74+||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
75+deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
76+deleteCol f m = map (deleteAt f) m
78+||| Matrix element at specified row and column indices
79+indices : Fin n -> Fin m -> Matrix n m a -> a
80+indices f1 f2 m = index f2 (index f1 m)
83+(/+/) : Ring a => Matrix n m a -> Matrix n m a -> Matrix n m a
86+||| Matrix subtraction
87+(/-/) : Ring a => Matrix n m a -> Matrix n m a -> Matrix n m a
90+||| Ring scalar times a matrix
91+RescaleBy.(*) : Ring a => a -> Matrix n m a -> Matrix n m a
92+RescaleBy.(*) s m = map (map (s <*>)) m
94+||| Rescale matrix by a ring scalar
95+RescaleMatrix.(*) : Ring a => Matrix n m a -> a -> Matrix n m a
96+RescaleMatrix.(*) m s = map (map (<*> s)) m
98+||| Matrix times a column vector
99+(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
100+(</>) m v = map (v <.>) m
102+||| Matrix times a row vector
103+(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
104+(<\>) r m = map (r <.>) $ transpose m
106+||| Matrix Multiplication
107+(<>) : Ring a => Matrix n k a ->
110+(<>) m1 m2 = map (<\> m2) m1
112+||| Tensor multiply (⊗) for ring matrices
113+(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
114+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
115+ stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
116+ stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
117+ stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
118+ stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
120+||| Cast a vector from a standard Vect to a proper n x 1 matrix
121+col : Vect n a -> Matrix n 1 a
122+col v = map (\x => [x]) v
124+||| Cast a row from a standard Vect to a proper 1 x n matrix
125+row : Vect n a -> Matrix 1 n a
128+||| Outer product between ring vectors
129+(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
130+(><) x y = (col x) <> (row y)
132+||| All finite numbers up to the given bound
133+allN : (n : Nat) -> Vect n (Fin n)
135+allN (S n) = FZ :: (map FS $ allN n)
138+Id : RingWithUnity a => {d : Nat} -> Matrix d d a
139+Id {d} = map (\n => basis n) $ allN d
142+Zero : Monoid a => {d : Nat} -> Matrix d d a
143+Zero {d} = replicate d zero
145+||| Matrix Commutator
146+(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
147+(<<>>) m1 m2 = (m1 <> m2) /-/ (m2 <> m1)
149+||| Matrix Anti-Commutator
150+(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
151+(>><<) m1 m2 = (m1 <> m2) /+/ (m2 <> m1)
154+-----------------------------------------------------------------------
155+-- Matrix Algebra Properties
156+-----------------------------------------------------------------------
159+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
162+-----------------------------------------------------------------------
163+-- Numberic data types as rings
164+-----------------------------------------------------------------------
166+instance Semigroup Integer where
169+instance Monoid Integer where
172+instance Group Integer where
175+instance AbelianGroup Integer
177+instance Ring Integer where
180+instance RingWithUnity Integer where
184+instance Semigroup Int where
187+instance Monoid Int where
190+instance Group Int where
193+instance AbelianGroup Int
195+instance Ring Int where
198+instance RingWithUnity Int where
202+instance Semigroup Float where
205+instance Monoid Float where
208+instance Group Float where
211+instance AbelianGroup Float
213+instance Ring Float where
216+instance RingWithUnity Float where
220+instance Semigroup a => Semigroup (Complex a) where
221+ (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
223+instance (Num a, Monoid a) => Monoid (Complex a) where
226+instance (Num a, Neg a, Group a) => Group (Complex a) where
227+ inverse = (\(r :+ i) => -r :+ -i)
229+instance Group (Complex a) => AbelianGroup (Complex a) where {}
231+instance (Num a, AbelianGroup (Complex a)) => Ring (Complex a) where
232+ (<*>) (a :+ b) (c :+ d) = (a*c - b*d) :+ (a*d + b*c)
234+instance (Num a, Ring (Complex a)) => RingWithUnity (Complex a) where
238+instance Semigroup Nat where
241+instance Monoid Nat where
244+instance VerifiedSemigroup Nat where
245+ semigroupOpIsAssociative = plusAssociative
247+instance VerifiedMonoid Nat where
248+ monoidNeutralIsNeutralL = plusZeroRightNeutral
249+ monoidNeutralIsNeutralR = plusZeroLeftNeutral