module Lunes where
open import Data.Nat
open import Data.Bool
eq : ℕ → ℕ → Bool
eq zero zero = true
eq zero (suc n) = false
eq (suc n) zero = false
eq (suc n) (suc n') = eq n n'
open import Data.List
snoc : {A : Set} → List A → A → List A
snoc [] a = a ∷ []
snoc {A} (x ∷ xs) a = x ∷ snoc {A} xs a
rev : {A : Set} → List A → List A
rev [] = []
rev (x ∷ xs) = snoc (rev xs) x
data ⊥ : Set where
open import Data.Maybe
_!!_ : {A : Set} → List A → ℕ → Maybe A
[] !! n = nothing
(a ∷ as) !! zero = just a
(a ∷ as) !! suc n = as !! n
open import Data.Vec
snoc' : {A : Set}{n : ℕ} → Vec A n → A → Vec A (suc n)
snoc' [] a = a ∷ []
snoc' (x ∷ xs) a = x ∷ (snoc' xs a)
rev' : {A : Set}{n : ℕ} → Vec A n → Vec A n
rev' [] = []
rev' (x ∷ xs) = snoc' (rev' xs) x
open import Data.Fin hiding (_+_)
enum : (n : ℕ) → Vec (Fin n) n
enum zero = []
enum (suc n) = zero ∷ Data.Vec.map suc (enum n)
max : {n : ℕ} → Fin (suc n)
max {zero} = zero {0}
max {suc n} = suc (max {n})
emb : {n : ℕ} → Fin n → Fin (suc n)
emb zero = zero
emb (suc i) = suc (emb i)
inv : {n : ℕ} → Fin n → Fin n
inv zero = max
inv (suc i) = emb (inv i)
_!!'_ : {A : Set}{n : ℕ} → Vec A n → Fin n → A
[] !!' ()
(x ∷ xs) !!' zero = x
(x ∷ xs) !!' suc i = xs !!' i
Vector : ℕ → Set
Vector m = Vec ℕ m
Matrix : ℕ → ℕ → Set
Matrix m n = Vec (Vector n) m
_*v_ : {n : ℕ} → ℕ → Vector n → Vector n
k *v [] = []
k *v (x ∷ xs) = k * x ∷ k *v xs
v1 : Vector 3
v1 = 1 ∷ 2 ∷ 3 ∷ []
test1 : Vector 3
test1 = 2 *v v1
_+v_ : {n : ℕ} → Vector n → Vector n → Vector n
[] +v [] = []
(x ∷ xs) +v (y ∷ ys) = x + y ∷ xs +v ys
v2 : Vector 3
v2 = 2 ∷ 3 ∷ 0 ∷ []
test2 : Vector 3
test2 = v1 +v v2
zeros : {n : ℕ} → Vector n
zeros {zero} = []
zeros {suc n} = zero ∷ zeros {n}
_*vm_ : {m n : ℕ} → Vector m → Matrix m n → Vector n
[] *vm [] = zeros
(x ∷ xs) *vm (ys ∷ yss) = (x *v ys) +v (xs *vm yss)
id3 : Matrix 3 3
id3 = (1 ∷ 0 ∷ 0 ∷ [])
∷ (0 ∷ 1 ∷ 0 ∷ [])
∷ (0 ∷ 0 ∷ 1 ∷ [])
∷ []
test3 : Vector 3
test3 = v1 *vm id3
_*mm_ : {l m n : ℕ} → Matrix l m → Matrix m n → Matrix l n
[] *mm yss = []
(xs ∷ xss) *mm yss = xs *vm yss ∷ xss *mm yss
inv3 : Matrix 3 3
inv3 = (0 ∷ 0 ∷ 1 ∷ [])
∷ (0 ∷ 1 ∷ 0 ∷ [])
∷ (1 ∷ 0 ∷ 0 ∷ [])
∷ []
test4 : Matrix 3 3
test4 = inv3 *mm inv3
vreturn : {A : Set}{n : ℕ} → A → Vec A n
vreturn {n = zero} a = []
vreturn {n = suc m} a = a ∷ vreturn {n = m} a
vapp : {A B : Set}{n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
vapp [] [] = []
vapp (f ∷ fs) (a ∷ as) = f a ∷ vapp fs as
transpose : {m n : ℕ} → Matrix m n → Matrix n m
transpose [] = vreturn []
transpose (as ∷ ass) = vapp (vapp (vreturn _∷_) as) (transpose ass)
rect : Matrix 2 3
rect = (1 ∷ 2 ∷ 3 ∷ [])
∷ (4 ∷ 5 ∷ 6 ∷ [])
∷ []
test5 : Matrix 3 2
test5 = transpose rect