From 60ba3d15ffe8fcc7e234807ac1a6c4360cedd505 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 1 Aug 2015 19:33:31 +0100
Subject: [PATCH] feat(library/data/matrix): add basic matrix module

---
 library/data/matrix.lean  | 108 ++++++++++++++++++++++++++++++++++++++
 src/frontends/lean/pp.cpp |   4 +-
 2 files changed, 110 insertions(+), 2 deletions(-)
 create mode 100644 library/data/matrix.lean

diff --git a/library/data/matrix.lean b/library/data/matrix.lean
new file mode 100644
index 000000000..bb40ed547
--- /dev/null
+++ b/library/data/matrix.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+
+Matrices
+-/
+import algebra.ring data.fin data.fintype
+open algebra fin nat
+
+definition matrix [reducible] (A : Type) (m n : nat) := fin m → fin n → A
+
+namespace matrix
+variables {A B C : Type} {m n p : nat}
+
+definition val [reducible] (M : matrix A m n) (i : fin m) (j : fin n) : A :=
+M i j
+
+namespace ops
+notation M `[` i `,` j `]` := val M i j
+end ops
+
+open ops
+
+protected lemma ext {M N : matrix A m n} (h : ∀ i j, M[i,j] = N[i, j]) : M = N :=
+funext (λ i, funext (λ j, h i j))
+
+protected lemma has_decidable_eq [h : decidable_eq A] (m n : nat) : decidable_eq (matrix A m n) :=
+_
+
+definition to_matrix (f : fin m → fin n → A) : matrix A m n :=
+f
+
+definition map (f : A → B) (M : matrix A m n) : matrix B m n :=
+λ i j, f (M[i,j])
+
+definition map₂ (f : A → B → C) (M : matrix A m n) (N : matrix B m n) : matrix C m n :=
+λ i j, f (M[i, j]) (N[i,j])
+
+definition transpose (M : matrix A m n) : matrix A n m :=
+λ i j, M[j, i]
+
+definition symmetric (M : matrix A n n) :=
+transpose M = M
+
+section
+variable [r : comm_ring A]
+include r
+
+definition identity (n : nat) : matrix A n n :=
+λ i j, if i = j then 1 else 0
+
+definition I {n : nat} : matrix A n n :=
+identity n
+
+definition zero (m n : nat) : matrix A m n :=
+λ i j, 0
+
+definition add (M : matrix A m n) (N : matrix A m n) : matrix A m n :=
+λ i j, M[i, j] + N[i, j]
+
+definition sub (M : matrix A m n) (N : matrix A m n) : matrix A m n :=
+λ i j, M[i, j] - N[i, j]
+
+definition smul (a : A) (M : matrix A m n) : matrix A m n :=
+λ i j, a * M[i, j]
+
+definition mul (M : matrix A m n) (N : matrix A n p) : matrix A m p :=
+λ i j, fin.foldl has_add.add 0 (λ k : fin n, M[i,k] * N[k,j])
+
+infix + := add
+infix - := sub
+infix * := mul
+infix * := smul
+notation 0 := zero _ _
+
+lemma add_zero (M : matrix A m n) : M + 0 = M :=
+matrix.ext (λ i j, !algebra.add_zero)
+
+lemma zero_add (M : matrix A m n) : 0 + M = M :=
+matrix.ext (λ i j, !algebra.zero_add)
+
+lemma add.comm (M : matrix A m n) (N : matrix A m n) : M + N = N + M :=
+matrix.ext (λ i j, !algebra.add.comm)
+
+lemma add.assoc (M : matrix A m n) (N : matrix A m n) (P : matrix A m n) : (M + N) + P = M + (N + P) :=
+matrix.ext (λ i j, !algebra.add.assoc)
+
+definition is_diagonal (M : matrix A n n) :=
+∀ i j, i = j ∨ M[i, j] = 0
+
+definition is_zero (M : matrix A m n) :=
+∀ i j, M[i, j] = 0
+
+definition is_upper_triangular (M : matrix A n n) :=
+∀ i j, i > j → M[i, j] = 0
+
+definition is_lower_triangular (M : matrix A n n) :=
+∀ i j, i < j → M[i, j] = 0
+
+definition inverse (M : matrix A n n) (N : matrix A n n) :=
+M * N = I ∧ N * M = I
+
+definition invertible (M : matrix A n n) :=
+∃ N, inverse M N
+
+end
+end matrix
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index eac3b28c1..5acbd666e 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1000,14 +1000,14 @@ static bool add_extra_space_first(name const & tk) {
     // TODO(Leo): this is a hard-coded temporary solution for deciding whether extra
     // spaces should be added or not when pretty printing notation.
     // We should implement a better solution in the future.
-    return tk != "(" && tk != ")";
+    return tk != "(" && tk != ")" && tk != "[";
 }
 
 static bool add_extra_space(name const & tk) {
     // TODO(Leo): this is a hard-coded temporary solution for deciding whether extra
     // spaces should be added or not when pretty printing notation.
     // We should implement a better solution in the future.
-    return tk != "," && tk != "(" && tk != ")";
+    return tk != "," && tk != "(" && tk != ")" && tk != "[";
 }
 
 static bool is_atomic_notation(notation_entry const & entry) {