Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/matrices.agda
Created Aug 30, 2019

Embed
What would you like to do?
{-# OPTIONS --safe --cubical #-}
module Bits where
open import Cubical.Data.Nat asusing (ℕ; suc; zero)
open import Agda.Primitive using (Level)
open import Cubical.Foundations.Function
variable
a : Level
A : Set a
data Fin : ℕ → Set where
zero : {n} Fin (suc n)
suc : {n} Fin n Fin (suc n)
infixr 5 _∷_
data Vec (A : Set a) : ℕ → Set a where
[] : Vec A zero
_∷_ : {n} A Vec A n Vec A (suc n)
Vec′ : Set a Set a
Vec′ A n = Fin n A
_[_] : {n} Vec A n Vec′ A n
(x ∷ xs) [ zero ] = x
(x ∷ xs) [ suc i ] = xs [ i ]
tabulate : {n} Vec′ A n Vec A n
tabulate {n = zero} f = []
tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)
open import Cubical.Foundations.Prelude
v→tab→v : {n} (xs : Vec A n) tabulate (_[_] xs) ≡ xs
v→tab→v [] = refl
v→tab→v (x ∷ xs) = cong (x ∷_) (v→tab→v xs)
tab→v→tab′ : {n} (xs : Vec′ A n) i tabulate xs [ i ] ≡ xs i
tab→v→tab′ xs zero = refl
tab→v→tab′ xs (suc i) = tab→v→tab′ (xs ∘ suc) i
tab→v→tab : {n} (xs : Vec′ A n) _[_] (tabulate xs) ≡ xs
tab→v→tab xs = funExt (tab→v→tab′ xs)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Core.Glue
Vec≃Vec′ : {n} Vec A n ≃ Vec′ A n
Vec≃Vec′ = isoToEquiv (iso _[_] tabulate tab→v→tab v→tab→v)
record Semiring ℓ : Set (ℓ-suc ℓ) where
infixl 6 _+_
infixl 7 _×_
field
Carrier : Set ℓ
_+_ : Carrier Carrier Carrier
_×_ : Carrier Carrier Carrier
0# : Carrier
1# : Carrier
module Matrices {ℓ} (rng : Semiring ℓ) where
open Semiring rng
Mat : Set ℓ
Mat n m = Vec′ (Vec′ Carrier m) n
0ᵐ : {n m} Mat n m
0ᵐ _ _ = 0#
1ᵐ : {n m} Mat n m
1ᵐ zero zero = 1#
1ᵐ zero (suc _) = 0#
1ᵐ (suc _) zero = 0#
1ᵐ (suc i) (suc j) = 1ᵐ i j
_+ᵐ_ : {n m} Mat n m Mat n m Mat n m
(xs +ᵐ ys) i j = xs i j + ys i j
infix 2 Sum
Sum : (n : ℕ) (Fin n Carrier) Carrier
Sum zero f = 0#
Sum (suc n) f = f zero + Sum n (f ∘ suc)
syntax Sum m (λ k e) = Σ[ k ≡0][ m ] e
_×ᵐ_ : {n m p} Mat n m Mat m p Mat n p
(xs ×ᵐ ys) i j = Σ[ k ≡0][ _ ] xs i k × ys k j
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.