Basic definitions and properties of matrices (#300)

* Add Fin defined using data and prove that vectors are equal to maps out of Fin

* oops

* start working on matrices

* wip

* finish the matrix addition example

* nicer addition syntax

* comments

* simplify a definition (thanks Andrea!)

Cubical/Algebra/Matrix.agda

@@ -0,0 +1,145 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Algebra.Matrix where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Functions.FunExtEquiv
+
+import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Nat hiding (_+_)
+open import Cubical.Data.Vec
+open import Cubical.Data.FinData
+open import Cubical.Relation.Nullary
+
+open import Cubical.Structures.CommRing
+
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+-- Equivalence between Vec matrix and Fin function matrix
+
+FinMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
+FinMatrix A m n = FinVec (FinVec A n) m
+
+VecMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
+VecMatrix A m n = Vec (Vec A n) m
+
+FinMatrix→VecMatrix : {m n : ℕ} → FinMatrix A m n → VecMatrix A m n
+FinMatrix→VecMatrix M = FinVec→Vec (λ fm → FinVec→Vec (λ fn → M fm fn))
+
+VecMatrix→FinMatrix : {m n : ℕ} → VecMatrix A m n → FinMatrix A m n
+VecMatrix→FinMatrix M fn fm = lookup fm (lookup fn M)
+
+FinMatrix→VecMatrix→FinMatrix : {m n : ℕ} (M : FinMatrix A m n) → VecMatrix→FinMatrix (FinMatrix→VecMatrix M) ≡ M
+FinMatrix→VecMatrix→FinMatrix {m = zero} M = funExt λ f → ⊥.rec (¬Fin0 f)
+FinMatrix→VecMatrix→FinMatrix {n = zero} M = funExt₂ λ _ f → ⊥.rec (¬Fin0 f)
+FinMatrix→VecMatrix→FinMatrix {m = suc m} {n = suc n} M = funExt₂ goal
+  where
+  goal : (fm : Fin (suc m)) (fn : Fin (suc n)) →
+         VecMatrix→FinMatrix (_ ∷ FinMatrix→VecMatrix (λ z → M (suc z))) fm fn ≡ M fm fn
+  goal zero zero = refl
+  goal zero (suc fn) i = FinVec→Vec→FinVec (λ z → M zero (suc z)) i fn
+  goal (suc fm) fn i = FinMatrix→VecMatrix→FinMatrix (λ z → M (suc z)) i fm fn
+
+VecMatrix→FinMatrix→VecMatrix : {m n : ℕ} (M : VecMatrix A m n) → FinMatrix→VecMatrix (VecMatrix→FinMatrix M) ≡ M
+VecMatrix→FinMatrix→VecMatrix {m = zero} [] = refl
+VecMatrix→FinMatrix→VecMatrix {m = suc m} (M ∷ MS) i = Vec→FinVec→Vec M i ∷ VecMatrix→FinMatrix→VecMatrix MS i
+
+FinMatrixIsoVecMatrix : (A : Type ℓ) (m n : ℕ) → Iso (FinMatrix A m n) (VecMatrix A m n)
+FinMatrixIsoVecMatrix A m n =
+  iso FinMatrix→VecMatrix VecMatrix→FinMatrix VecMatrix→FinMatrix→VecMatrix FinMatrix→VecMatrix→FinMatrix
+
+FinMatrix≃VecMatrix : {m n : ℕ} → FinMatrix A m n ≃ VecMatrix A m n
+FinMatrix≃VecMatrix {_} {A} {m} {n} = isoToEquiv (FinMatrixIsoVecMatrix A m n)
+
+FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
+FinMatrix≡VecMatrix _ _ _ = ua FinMatrix≃VecMatrix
+
+
+-- We could have constructed the above Path as follows, but that
+-- doesn't reduce as nicely as ua isn't on the toplevel:
+--
+-- FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
+-- FinMatrix≡VecMatrix A m n i = FinVec≡Vec (FinVec≡Vec A n i) m i
+
+
+-- Experiment using addition. Transport commutativity from one
+-- representation to the the other and relate the transported
+-- operation with a more direct definition.
+module _ (R : CommRing {ℓ}) where
+
+  open commring-·syntax R
+
+  addFinMatrix : ∀ {m n} → FinMatrix ⟨ R ⟩ m n → FinMatrix ⟨ R ⟩ m n → FinMatrix ⟨ R ⟩ m n
+  addFinMatrix M N = λ k l → M k l + N k l
+
+  addFinMatrixComm : ∀ {m n} → (M N : FinMatrix ⟨ R ⟩ m n) → addFinMatrix M N ≡ addFinMatrix N M
+  addFinMatrixComm M N i k l = commring+-comm R (M k l) (N k l) i
+
+  addVecMatrix : ∀ {m n} → VecMatrix ⟨ R ⟩ m n → VecMatrix ⟨ R ⟩ m n → VecMatrix ⟨ R ⟩ m n
+  addVecMatrix {m} {n} = transport (λ i → FinMatrix≡VecMatrix ⟨ R ⟩ m n i
+                                        → FinMatrix≡VecMatrix ⟨ R ⟩ m n i
+                                        → FinMatrix≡VecMatrix ⟨ R ⟩ m n i)
+                                   addFinMatrix
+
+  addMatrixPath : ∀ {m n} → PathP (λ i → FinMatrix≡VecMatrix ⟨ R ⟩ m n i
+                                       → FinMatrix≡VecMatrix ⟨ R ⟩ m n i
+                                       → FinMatrix≡VecMatrix ⟨ R ⟩ m n i)
+                                  addFinMatrix addVecMatrix
+  addMatrixPath {m} {n} i = transp (λ j → FinMatrix≡VecMatrix ⟨ R ⟩ m n (i ∧ j)
+                                        → FinMatrix≡VecMatrix ⟨ R ⟩ m n (i ∧ j)
+                                        → FinMatrix≡VecMatrix ⟨ R ⟩ m n (i ∧ j))
+                                   (~ i) addFinMatrix
+
+  addVecMatrixComm : ∀ {m n} → (M N : VecMatrix ⟨ R ⟩ m n) → addVecMatrix M N ≡ addVecMatrix N M
+  addVecMatrixComm {m} {n} = transport (λ i → (M N : FinMatrix≡VecMatrix ⟨ R ⟩ m n i)
+                                            → addMatrixPath i M N ≡ addMatrixPath i N M)
+                                       addFinMatrixComm
+
+
+  -- More direct definition of addition for VecMatrix:
+
+  addVec : ∀ {m} → Vec ⟨ R ⟩ m → Vec ⟨ R ⟩ m → Vec ⟨ R ⟩ m
+  addVec [] [] = []
+  addVec (x ∷ xs) (y ∷ ys) = x + y ∷ addVec xs ys
+
+  addVecLem : ∀ {m} → (M N : Vec ⟨ R ⟩ m)
+            → FinVec→Vec (λ l → lookup l M + lookup l N) ≡ addVec M N
+  addVecLem {zero} [] [] = refl
+  addVecLem {suc m} (x ∷ xs) (y ∷ ys) = cong (λ zs → x + y ∷ zs) (addVecLem xs ys)
+
+  addVecMatrix' : ∀ {m n} → VecMatrix ⟨ R ⟩ m n → VecMatrix ⟨ R ⟩ m n → VecMatrix ⟨ R ⟩ m n
+  addVecMatrix' [] [] = []
+  addVecMatrix' (M ∷ MS) (N ∷ NS) = addVec M N ∷ addVecMatrix' MS NS
+
+  -- The key lemma relating addVecMatrix and addVecMatrix'
+  addVecMatrixEq : ∀ {m n} → (M N : VecMatrix ⟨ R ⟩ m n) → addVecMatrix M N ≡ addVecMatrix' M N
+  addVecMatrixEq {zero} {n} [] [] j = transp (λ i → Vec (Vec ⟨ R ⟩ n) 0) j []
+  addVecMatrixEq {suc m} {n} (M ∷ MS) (N ∷ NS) =
+    addVecMatrix (M ∷ MS) (N ∷ NS)
+      ≡⟨ transportUAop₂ FinMatrix≃VecMatrix addFinMatrix (M ∷ MS) (N ∷ NS) ⟩
+    FinVec→Vec (λ l → lookup l M + lookup l N) ∷ _
+      ≡⟨ (λ i → addVecLem M N i ∷ FinMatrix→VecMatrix (λ k l → lookup l (lookup k MS) + lookup l (lookup k NS))) ⟩
+    addVec M N ∷ _
+      ≡⟨ cong (λ X → addVec M N ∷ X) (sym (transportUAop₂ FinMatrix≃VecMatrix addFinMatrix MS NS) ∙ addVecMatrixEq MS NS) ⟩
+    addVec M N ∷ addVecMatrix' MS NS ∎
+
+  -- By binary funext we get an equality as functions
+  addVecMatrixEqFun : ∀ {m} {n} → addVecMatrix {m} {n} ≡ addVecMatrix'
+  addVecMatrixEqFun i M N = addVecMatrixEq M N i
+
+  -- We then directly get the properties about addVecMatrix'
+  addVecMatrixComm' : ∀ {m n} → (M N : VecMatrix ⟨ R ⟩ m n) → addVecMatrix' M N ≡ addVecMatrix' N M
+  addVecMatrixComm' M N = sym (addVecMatrixEq M N) ∙∙ addVecMatrixComm M N ∙∙ addVecMatrixEq N M
+
+  -- TODO: prove more properties about addition of matrices for both
+  -- FinMatrix and VecMatrix
+
+
+
+-- TODO: define multiplication of matrices and do the same kind of
+-- reasoning as we did for addition

Cubical/Data/FinData.agda

@@ -0,0 +1,4 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.FinData where
+
+open import Cubical.Data.FinData.Base public

Cubical/Data/FinData/Base.agda

@@ -0,0 +1,21 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.FinData.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat
+open import Cubical.Relation.Nullary
+
+data Fin : ℕ → Type₀ where
+  zero : {n : ℕ} → Fin (suc n)
+  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
+
+toℕ : ∀ {n} → Fin n → ℕ
+toℕ zero    = 0
+toℕ (suc i) = suc (toℕ i)
+
+fromℕ : (n : ℕ) → Fin (suc n)
+fromℕ zero    = zero
+fromℕ (suc n) = suc (fromℕ n)
+
+¬Fin0 : ¬ Fin 0
+¬Fin0 ()

Cubical/Data/Vec/Base.agda

@@ -6,6 +6,7 @@ module Cubical.Data.Vec.Base where
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Nat
+open import Cubical.Data.FinData
 
 private
   variable
@@ -47,3 +48,7 @@ _++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
 concat : ∀ {m n} → Vec (Vec A m) n → Vec A (n * m)
 concat []         = []
 concat (xs ∷ xss) = xs ++ concat xss
+
+lookup : ∀ {n} {A : Type ℓ} → Fin n → Vec A n → A
+lookup zero    (x ∷ xs) = x
+lookup (suc i) (x ∷ xs) = lookup i xs

Cubical/Data/Vec/Properties.agda

@@ -2,18 +2,61 @@
 module Cubical.Data.Vec.Properties where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
 
+import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
 open import Cubical.Data.Vec.Base
+open import Cubical.Data.FinData
+open import Cubical.Relation.Nullary
 
 private
   variable
     ℓ : Level
+    A : Type ℓ
 
 
 -- This is really cool!
 -- Compare with: https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Properties/WithK.agda#L32
-++-assoc : ∀ {m n k} {A : Type ℓ} (xs : Vec A m) (ys : Vec A n) (zs : Vec A k) →
+++-assoc : ∀ {m n k} (xs : Vec A m) (ys : Vec A n) (zs : Vec A k) →
            PathP (λ i → Vec A (+-assoc m n k (~ i))) ((xs ++ ys) ++ zs) (xs ++ ys ++ zs)
 ++-assoc {m = zero} [] ys zs = refl
 ++-assoc {m = suc m} (x ∷ xs) ys zs i = x ∷ ++-assoc xs ys zs i
+
+
+-- Equivalence between Fin n → A and Vec A n
+
+FinVec : (A : Type ℓ) (n : ℕ) → Type ℓ
+FinVec A n = Fin n → A
+
+FinVec→Vec : {n : ℕ} → FinVec A n → Vec A n
+FinVec→Vec {n = zero}  xs = []
+FinVec→Vec {n = suc _} xs = xs zero ∷ FinVec→Vec (λ x → xs (suc x))
+
+Vec→FinVec : {n : ℕ} → Vec A n → FinVec A n
+Vec→FinVec xs f = lookup f xs
+
+FinVec→Vec→FinVec : {n : ℕ} (xs : FinVec A n) → Vec→FinVec (FinVec→Vec xs) ≡ xs
+FinVec→Vec→FinVec {n = zero} xs = funExt λ f → ⊥.rec (¬Fin0 f)
+FinVec→Vec→FinVec {n = suc n} xs = funExt goal
+  where
+  goal : (f : Fin (suc n))
+       → Vec→FinVec (xs zero ∷ FinVec→Vec (λ x → xs (suc x))) f ≡ xs f
+  goal zero = refl
+  goal (suc f) i = FinVec→Vec→FinVec (λ x → xs (suc x)) i f
+
+Vec→FinVec→Vec : {n : ℕ} (xs : Vec A n) → FinVec→Vec (Vec→FinVec xs) ≡ xs
+Vec→FinVec→Vec {n = zero}  [] = refl
+Vec→FinVec→Vec {n = suc n} (x ∷ xs) i = x ∷ Vec→FinVec→Vec xs i
+
+FinVecIsoVec : (n : ℕ) → Iso (FinVec A n) (Vec A n)
+FinVecIsoVec n = iso FinVec→Vec Vec→FinVec Vec→FinVec→Vec FinVec→Vec→FinVec
+
+FinVec≃Vec : (n : ℕ) → FinVec A n ≃ Vec A n
+FinVec≃Vec n = isoToEquiv (FinVecIsoVec n)
+
+FinVec≡Vec : (n : ℕ) → FinVec A n ≡ Vec A n
+FinVec≡Vec n = ua (FinVec≃Vec n)
+

Cubical/Foundations/Univalence.agda

@@ -215,12 +215,26 @@ univalencePath = ua (compEquiv univalence LiftEquiv)
 -- The computation rule for ua. Because of "ghcomp" it is now very
 -- simple compared to cubicaltt:
 -- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202
-uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ e .fst x
-uaβ e x = transportRefl (e .fst x)
+uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x
+uaβ e x = transportRefl (equivFun e x)
 
 uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P
 uaη = J (λ _ q → ua (pathToEquiv q) ≡ q) (cong ua pathToEquivRefl ∙ uaIdEquiv)
 
+-- Useful lemma for unfolding a transported function over ua
+-- If we would have regularity this would be refl
+transportUAop₁ : ∀ {A B : Type ℓ} → (e : A ≃ B) (f : A → A) (x : B)
+               → transport (λ i → ua e i → ua e i) f x ≡ equivFun e (f (invEq e x))
+transportUAop₁ e f x i = transportRefl (equivFun e (f (invEq e (transportRefl x i)))) i
+
+-- Binary version
+transportUAop₂ : ∀ {ℓ} {A B : Type ℓ} → (e : A ≃ B) (f : A → A → A) (x y : B)
+               → transport (λ i → ua e i → ua e i → ua e i) f x y ≡
+                 equivFun e (f (invEq e x) (invEq e y))
+transportUAop₂ e f x y i =
+    transportRefl (equivFun e (f (invEq e (transportRefl x i))
+                                 (invEq e (transportRefl y i)))) i
+
 -- Alternative version of EquivJ that only requires a predicate on functions
 elimEquivFun : {A B : Type ℓ} (P : (A : Type ℓ) → (A → B) → Type ℓ')
              → (r : P B (idfun B)) → (e : A ≃ B) → P A (e .fst)

Cubical/Structures/CommRing.agda

@@ -1,5 +1,4 @@
 {-# OPTIONS --cubical --safe #-}
-
 module Cubical.Structures.CommRing where
 
 open import Cubical.Foundations.Prelude