Library Matrix_arith

Require Import types.
Require Import Array.
Require Import Vector.
Require Export Matrix_base.
Require Import EnsembleFacts.

Definition MatrixAdd_d (U:Type) (m n:nat) (add:Operation U)
(default:U) (A B:array2D U m n):array2D U m n:=
matrix_from_func m n
(fun i j:nat=>add (ijth default i j A) (ijth default i j B)).

Lemma MatrixAdd_d_nil: forall (U:Type) (m n:nat)
(add:Operation U) (default:U),
MatrixAdd_d (U:Type) 0 n add default
 (nil2D U n) (nil2D U n)=nil2D U n.

Lemma MatrixAdd_d_single: forall (U:Type) (m n:nat)
(add:Operation U) (default:U) (x y:array U n),
MatrixAdd_d U 1 n add default
(x::nil2D U n) (y::nil2D U n)=
(VectorAdd_d U n add default x y)::nil2D U n.

Definition MatrixAdd (U:Type) (m n:nat) (add:Operation U)
(A B:array2D U m n):array2D U m n:=
VectorAdd (VectorAdd add) A B.

Implicit Arguments MatrixAdd [U m n].

Lemma MatrixAdd_nil: forall (U:Type) (m n:nat) (add:Operation U),
MatrixAdd add (nil2D U n) (nil2D U n)=nil2D U n.

Lemma MatrixAdd_single: forall (U:Type) (m n:nat)
(add:Operation U) (x y:array U n),
MatrixAdd add (x::nil2D U n) (y::nil2D U n)=
(VectorAdd add x y)::nil2D U n.

Theorem MatrixAdd_ijth: forall (U:Type) (m n:nat)
(add:Operation U) (d:U) (A B:array2D U m n)
(i j:nat), i<m-> j<n->
ijth d i j (MatrixAdd add A B)=
add (ijth d i j A) (ijth d i j B).

Lemma MatrixAdd_commutativity: forall (U:Type) (m n:nat)
(add:Operation U),
Commutativity U add ->
Commutativity _ (@MatrixAdd U m n add).

Lemma MatrixAdd_associativity: forall (U:Type) (m n:nat)
(add:Operation U),
Associativity U add ->
Associativity _ (@MatrixAdd U m n add).

Definition MatrixProduct (U:Type) (p q r:nat)
(add prod:Operation U) (zero:U)
(A:array2D U p q) (B:array2D U q r):array2D U p r:=
matrix_from_funcrange p r (
fun (I:{i|i<p}) (J:{j|j<r})=>
ScalarProduct add prod zero
 (nth_range I A) (nthC_range J B)
).
Implicit Arguments MatrixProduct [U p q r].

Section Arith.

Variable U:Type.
Variable add prod:Operation U.
Variable zero one:U.

Infix "+" := add.
Infix "*" := prod.
Infix ":+" := add (at level 50, left associativity).
Infix ":*" := prod (at level 40, left associativity).
Hypothesis add_comm: Commutativity U add.
Hypothesis add_ass: Associativity U add.
Hypothesis prod_comm: Commutativity U prod.
Hypothesis prod_ass: Associativity U prod.
Hypothesis distributive_left: forall (a b c:U),
a * (b + c)=(a * b) +(a* c).
Hypothesis distributive_right: forall (a b c:U),
(a + b)*c=(a * c) +(b* c).

Hypothesis zeroL: forall (x:U), zero+x=x.
Hypothesis zeroR: forall (x:U), x+zero=x.
Hypothesis oneL: forall (x:U), one*x=x.
Hypothesis oneR: forall (x:U), x*one=x.

Hypothesis prod_zero_l: forall (x:U), zero*x=zero.
Hypothesis prod_zero_r: forall (x:U), x*zero=zero.

Notation "a + b" := (MatrixAdd add a b).
Notation "a * b" := (MatrixProduct add prod zero a b).
Notation " a ^T " := (Transpose a) (at level 25).

Let zerovector (n:nat):=array_homogeneous U n zero.

Let summatory (n:nat) (f:{k|k<n}->U):=
 fold_right add (array_from_funcrange n f) zero.
Implicit Arguments summatory [n].
Let summatoryv (m n:nat) (f:{k|k<m}->array U n):=
 fold_right (VectorAdd add) (array_from_funcrange m f)
 (zerovector n).
Implicit Arguments summatoryv [m n].

Let unitvector (n i:nat):=UnitVector n zero one i.
Let unitrow (n i:nat):=(unitvector n i)::nil2D U n.
Let unitcol (n i:nat):=Column (unitvector n i).

Lemma ScalarProduct_comm: forall (n:nat)
(a b:array U n),
ScalarProduct add prod zero a b=
ScalarProduct add prod zero b a.

Lemma TransposeZeroMatrix: forall (m n:nat),
(ZeroMatrix U m n zero)^T=(ZeroMatrix U n m zero).

Lemma Product_nil_l: forall (p q:nat)
(A:array2D U p q), nil2D U p * A =nil2D U q.

Lemma Product_nil_r: forall (p q:nat)
(A:array2D U p q), A * nilC U q=nilC U p.

Lemma Product_nil_c: forall (p q:nat),
nilC U p * nil2D U q=ZeroMatrix U p q zero.

Lemma TransposeProduct: forall (p q r:nat)
(A:array2D U p q) (B:array2D U q r),
(A*B)^T=B^T * A^T.

Theorem Product_unit_l: forall (m n i:nat) (D:array U n)
(A:array2D U m n), i<m->
unitrow m i * A =nth D i A :: nil2D U n.

Theorem Product_unit_r: forall (m n j:nat) (D:array U m)
(A:array2D U m n), j<n->
A * (unitcol n j) =Column (nthC D j A).

Theorem MatrixProduct_Zero_l: forall (p q r:nat)
(A:array2D U q r),
ZeroMatrix U p q zero * A=ZeroMatrix U p r zero.

Theorem MatrixProduct_Zero_r: forall (p q r:nat)
(A:array2D U p q),
A*ZeroMatrix U q r zero=ZeroMatrix U p r zero.

Lemma nth_range_summatoryv: forall (m n:nat)
(f:{k|k<m}->array U n) (J:{j|j<n}),
nth_range J (summatoryv f)
=summatory (fun K:{k|k<m}=>nth_range J (f K)).

Lemma Matrix_row_summatory: forall (m n:nat)
(A:array2D U m n) (I:{i|i<m}),
nth_range I A=
summatoryv (fun J:{j|j<n}=>
let (j,Hj):=J in
ScalarProdVector prod (unitvector n j) (ijth_range I J A) ).

Lemma Matrix_col_summatory: forall (m n:nat)
(A:array2D U m n) (J:{j|j<n}),
nthC_range J A=
summatoryv (fun I:{i|i<m}=>
let (i,Hi):=I in
ScalarProdVector prod (unitvector m i) (ijth_range I J A) ).

Lemma _Matrix_arith_summatory_swap:
forall (m n:nat) (f:{i|i<m}->{j|j<n}->U),
summatory (fun I:{i|i<m}=>summatory (fun J:{j|j<n}=>f I J))=
summatory (fun J:{j|j<n}=>summatory (fun I:{i|i<m}=>f I J)).

Lemma ScalarProduct_summatory_l: forall (m n:nat)
(f:{i|i<m}->array U n) (a:array U n),
ScalarProduct add prod zero (summatoryv f) a=
summatory (fun I:{i|i<m}=>
ScalarProduct add prod zero (f I) a).

Lemma ScalarProduct_summatory_r: forall (m n:nat)
(f:{i|i<m}->array U n) (a:array U n),
ScalarProduct add prod zero a (summatoryv f)=
summatory (fun I:{i|i<m}=>
ScalarProduct add prod zero a (f I)).

Theorem MatrixProduct_summatory: forall (p q r:nat)
(A:array2D U p q) (B:array2D U q r)
(I:{i|i<p}) (J:{j|j<r}),
ijth_range I J (A*B)=
summatory (fun K:{k|k<q}=>
 (ijth_range I K A):*(ijth_range K J B)).

Theorem MatrixProduct_associativity: forall (p q r s:nat)
(A:array2D U p q) (B:array2D U q r) (C:array2D U r s),
(A*B)*C=A*(B*C).


End Arith.