@@ -6,6 +6,7 @@ import Builtins
66infixl 6 <->
77infixl 6 <+>
88infixl 6 <*>
9+infixl 5 <#>
910
1011%access public
1112
@@ -298,25 +299,27 @@ class (VerifiedRing a, Field a) => VerifiedField a where
298299 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299300 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
300301
301−-- vector spaces.
302302||| A Vector Space over a Field can be considered as an additive Abeliean Group
303−||| of Vectors adjoined to the Field structure by distributivity laws relating
304−||| the two operations. Such that we satisfy the following laws:
303+||| of Vectors adjoined to the Field structure with a scale operation multiplying
304+||| vectors by field elements, and distributivity laws relating the scale
305+||| operation to both field addition and vector space addition. Must satisfy the
306+||| following laws:
305307|||
306−||| + Unity for `<*>`:
307−||| forall a, a <*> unity == a
308−||| forall a, unity <*> a == a
309−||| + Distributivity of `<*>` and `<+>`:
310−||| forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)
311−||| forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)
312−class (Field a, AbelianGroup a) => VectorSpace a a where {}
313−
314−class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where
315− total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l
316− total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r
317− total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)
318− total vectorspaceScalarIsDistributiveWRTFieldAddition : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)
319−
308+||| + Compatibility of scalar multiplication with field multiplication:
309+||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v
310+||| + Field unity is the identity element of scalar multiplication:
311+||| forall v, unity <#> v = v
312+||| + Distributivity of `<#>` and `<+>`:
313+||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
314+||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
315+class (Field a, AbelianGroup b) => VectorSpace a b where
316+ (<#>) : a -> b -> b
317+
318+class (VerifiedField a, VerifiedAbelianGroup b, VectorSpace a b) => VerifiedVectorSpace a b where
319+ total vectorspaceScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
320+ total vectorspaceScalarUnityIsUnity : (v : b) -> unity <#> v = v
321+ total vectorspaceScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
322+ total vectorspaceScalarMultDistributiveWRTFieldAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
320323
321324-- XXX todo:
322325-- Structures where "abs" make sense.