Functional vector module

CHANGELOG.md

@@ -3027,3 +3027,54 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   <-weakInduction-startingFrom : P i →  (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j
   ```
+
+* In `Data.Vec.Functional.Algebra.Base`
+```agda
+  _≈ᴹ_ : Rel (VC n) ℓ
+  _+ᴹ_ : Op₂ $ VC n
+  0ᴹ : VC n
+  -ᴹ_ : Op₁ $ VC n
+  _*ₗ_ : Opₗ Carrier (VC n)
+```
+
+* Added algebraic properties in `Data.Vec.Functional.Algebra.Properties`
+```agda
+  +ᴹ-cong : Congruent₂ (_+ᴹ_ {n})
+  +ᴹ-assoc : Associative (_+ᴹ_ {n})
+  +ᴹ-comm : Commutative (_+ᴹ_ {n})
+  +ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_
+  +ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_
+  +ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_
+  -ᴹ‿cong : Congruent₁ (-ᴹ_ {n})
+  -ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_
+  -ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_
+  -ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_
+  *ₗ-cong : Congruent SR._≈_ (_*ₗ_ {n})
+  *ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_
+  *ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n})
+  *ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n})
+  *ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n})
+  *ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_
+  *ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n})
+```
+
+* Added structures in `Data.Vec.Functional.Algebra.Properties`
+```agda
+  isMagma : IsMagma (_+ᴹ_ {n})
+  isSemigroup : IsSemigroup (_+ᴹ_ {n})
+  isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ
+  isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ
+  isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_
+  isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_
+  isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_
+```
+
+* Added bundles in `Data.Vec.Functional.Algebra.Properties`
+```agda
+  magma : ℕ → Magma _ _
+  semiGroup : ℕ → Semigroup _ _
+  monoid : ℕ → Monoid _ _
+  commutativeMonoid : ℕ → CommutativeMonoid _ _
+  leftSemimodule : ℕ → LeftSemimodule _ _ _
+  leftModule : ℕ → LeftModule _ _ _
+```

src/Data/Vec/Functional/Algebra/Base.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some Vector-related module Definitions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Function using (_$_)
+open import Data.Product hiding (map)
+open import Data.Nat using (ℕ)
+open import Data.Fin using (Fin)
+open import Data.Vec.Functional
+open import Algebra.Core
+open import Algebra.Bundles
+open import Algebra.Module
+open import Relation.Binary
+import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid
+import Algebra.Definitions as AD
+import Algebra.Structures as AS
+
+module Data.Vec.Functional.Algebra.Base
+  {c ℓ} (ring : Ring c ℓ) where
+
+private variable
+  n : ℕ
+
+open Ring ring
+open VecSetoid setoid
+
+VC = Vector Carrier
+
+_≈ᴹ_ : Rel (VC n) ℓ
+_≈ᴹ_ = _≋_
+
+_+ᴹ_ : Op₂ $ VC n
+_+ᴹ_ = zipWith _+_
+
+0ᴹ : VC n
+0ᴹ = replicate 0#
+
+-ᴹ_ : Op₁ $ VC n
+-ᴹ_ = map $ -_
+
+_*ₗ_ : Opₗ Carrier (VC n)
+_*ₗ_ r = map (r *_)

src/Data/Vec/Functional/Algebra/Properties.agda

@@ -0,0 +1,173 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some Vector-related module properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Function using (_$_)
+open import Data.Product hiding (map)
+open import Data.Nat using (ℕ)
+open import Data.Fin using (Fin)
+open import Data.Vec.Functional
+open import Algebra.Core
+open import Algebra.Bundles
+open import Algebra.Module
+open import Relation.Binary
+import Data.Vec.Functional.Relation.Binary.Equality.Setoid as VecSetoid
+import Algebra.Definitions as AD
+import Algebra.Structures as AS
+import Data.Vec.Functional.Algebra.Base as VFA
+
+module Data.Vec.Functional.Algebra.Properties
+  {c ℓ} (ring : Ring c ℓ) where
+
+private variable
+  n : ℕ
+
+open Ring ring
+open VecSetoid setoid
+open VFA ring
+module SR = Semiring semiring
+open module AD' {n} = AD (_≈ᴹ_ {n})
+open module AS' {n} = AS (_≈ᴹ_ {n})
+open module LD {n} = LeftDefs Carrier (_≈ᴹ_ {n}) using (Congruent)
+
+------------------------------------------------------------------------
+-- Algebraic properties of _+ᴹ_ -ᴹ_ _*ₗ_
+
++ᴹ-cong : Congruent₂ (_+ᴹ_ {n})
++ᴹ-cong x≈y u≈v _ = +-cong (x≈y _) (u≈v _)
+
++ᴹ-assoc : Associative (_+ᴹ_ {n})
++ᴹ-assoc _ _ _ _ = +-assoc _ _ _
+
++ᴹ-comm : Commutative (_+ᴹ_ {n})
++ᴹ-comm _ _ _ = +-comm _ _
+
++ᴹ-identityˡ : LeftIdentity (0ᴹ {n}) _+ᴹ_
++ᴹ-identityˡ _ _ = +-identityˡ _
+
++ᴹ-identityʳ : RightIdentity (0ᴹ {n}) _+ᴹ_
++ᴹ-identityʳ _ _ = +-identityʳ _
+
++ᴹ-identity : Identity (0ᴹ {n}) _+ᴹ_
++ᴹ-identity = +ᴹ-identityˡ , +ᴹ-identityʳ
+
+-ᴹ‿cong : Congruent₁ (-ᴹ_ {n})
+-ᴹ‿cong f _ = -‿cong (f _)
+
+-ᴹ‿inverseˡ : AD'.LeftInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_
+-ᴹ‿inverseˡ _ _ = -‿inverseˡ _
+
+-ᴹ‿inverseʳ : AD'.RightInverse (0ᴹ {n}) -ᴹ_ _+ᴹ_
+-ᴹ‿inverseʳ _ _ = -‿inverseʳ _
+
+-ᴹ‿inverse : AD'.Inverse (0ᴹ {n}) -ᴹ_ _+ᴹ_
+-ᴹ‿inverse = -ᴹ‿inverseˡ , -ᴹ‿inverseʳ
+
+*ₗ-cong : Congruent SR._≈_ (_*ₗ_ {n})
+*ₗ-cong x≈y u≈v i = *-cong x≈y (u≈v i)
+
+*ₗ-zeroˡ : LD.LeftZero SR.0# (0ᴹ {n}) _*ₗ_
+*ₗ-zeroˡ f i = zeroˡ (f i)
+
+*ₗ-distribʳ : _*ₗ_ LD.DistributesOverʳ SR._+_ ⟶ (_+ᴹ_ {n})
+*ₗ-distribʳ _ _ _ _ = distribʳ _ _ _
+
+*ₗ-identityˡ : LD.LeftIdentity SR.1# (_*ₗ_ {n})
+*ₗ-identityˡ _ _ = *-identityˡ _
+
+*ₗ-assoc : LD.Associative SR._*_ (_*ₗ_ {n})
+*ₗ-assoc _ _ _ _ = *-assoc _ _ _
+
+*ₗ-zeroʳ : LD.RightZero (0ᴹ {n}) _*ₗ_
+*ₗ-zeroʳ _ _ = zeroʳ _
+
+*ₗ-distribˡ : _*ₗ_ LD.DistributesOverˡ (_+ᴹ_ {n})
+*ₗ-distribˡ _ _ _ _ = distribˡ _ _ _
+
+------------------------------------------------------------------------
+-- Structures
+
+isMagma : IsMagma (_+ᴹ_ {n})
+isMagma = record
+  { isEquivalence = ≋-isEquivalence _
+  ; ∙-cong = +ᴹ-cong
+  }
+
+isSemigroup : IsSemigroup (_+ᴹ_ {n})
+isSemigroup = record
+  { isMagma = isMagma
+  ; assoc = +ᴹ-assoc
+  }
+
+isMonoid : IsMonoid (_+ᴹ_ {n}) 0ᴹ
+isMonoid = record
+  { isSemigroup = isSemigroup
+  ; identity = +ᴹ-identity
+  }
+
+isCommutativeMonoid : IsCommutativeMonoid (_+ᴹ_ {n}) 0ᴹ
+isCommutativeMonoid = record
+  { isMonoid = isMonoid
+  ; comm = +ᴹ-comm
+  }
+
+isPreleftSemimodule : IsPreleftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_
+isPreleftSemimodule = record
+  { *ₗ-cong = *ₗ-cong
+  ; *ₗ-zeroˡ = *ₗ-zeroˡ
+  ; *ₗ-distribʳ = *ₗ-distribʳ
+  ; *ₗ-identityˡ = *ₗ-identityˡ
+  ; *ₗ-assoc = *ₗ-assoc
+  ; *ₗ-zeroʳ = *ₗ-zeroʳ
+  ; *ₗ-distribˡ = *ₗ-distribˡ
+  }
+
+isLeftSemimodule : IsLeftSemimodule semiring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ _*ₗ_
+isLeftSemimodule = record
+  { +ᴹ-isCommutativeMonoid = isCommutativeMonoid
+  ; isPreleftSemimodule = isPreleftSemimodule
+  }
+
+isLeftModule : IsLeftModule ring (_≈ᴹ_ {n}) _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_
+isLeftModule = record
+  { isLeftSemimodule = isLeftSemimodule
+  ; -ᴹ‿cong = -ᴹ‿cong
+  ; -ᴹ‿inverse = -ᴹ‿inverse
+  }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : ℕ → Magma _ _
+magma n = record
+  { isMagma = isMagma {n}
+  }
+
+semiGroup : ℕ → Semigroup _ _
+semiGroup n = record
+  { isSemigroup = isSemigroup {n}
+  }
+
+monoid : ℕ → Monoid _ _
+monoid n = record
+  { isMonoid = isMonoid {n}
+  }
+
+commutativeMonoid : ℕ → CommutativeMonoid _ _
+commutativeMonoid n = record
+  { isCommutativeMonoid = isCommutativeMonoid {n}
+  }
+
+leftSemimodule : ℕ → LeftSemimodule _ _ _
+leftSemimodule n = record
+  { isLeftSemimodule = isLeftSemimodule {n}
+  }
+
+leftModule : ℕ → LeftModule _ _ _
+leftModule n = record
+  { isLeftModule = isLeftModule {n}
+  }