Library Matrix_base

Require Import EnsembleFacts.
Require Import types.
Require Import Array.
Require Import Vector.
Require Import Recdef.
Require Import Omega.

Open Scope array_scope.


Definition array2D (A:Type) (m n:nat):=array (array A n) m.
Definition nil2D (A:Type) (n:nat):=nil (array A n).
Definition cons2D (A:Type) (n:nat):=@cons (array A n).
Implicit Arguments cons2D [A n].

Axiom array2D_typeequality_down_H: forall (U:Type) (m n1 n2:nat),
array2D U m n1=array2D U m n2->n1=n2.

Lemma array2D_typeequality_down_V: forall (U:Type) (m1 m2 n:nat),
array2D U m1 n=array2D U m2 n->m1=m2.

Lemma array2D_rewrite_dependent_H: forall (U D:Type) (m n1 n2:nat)
(A:array2D U m n1) (B:array2D U m n2)
(f:forall n:nat,array2D U m n->D), A==B-> f n1 A=f n2 B.

Lemma array2D_rewrite_dependent_H_Prop: forall (U:Type) (m n1 n2:nat)
(A:array2D U m n1) (B:array2D U m n2)
(P:forall n:nat,array2D U m n->Prop), A==B-> P n1 A->P n2 B.

Definition ijth (U:Type) (m n:nat) (default:U)
(i j:nat) (M:array2D U m n):U:=
match nth_error i M with
|error => default
|value row=> nth default j row
end.
Implicit Arguments ijth [U m n].

Definition ijth_error (U:Type) (m n i j:nat) (M:array2D U m n)
:Exc U:=
match nth_error i M with
|error => error
|value row=> nth_error j row
end.
Implicit Arguments ijth_error [U m n].

Definition ijth_range (U:Type) (m n:nat)
(I:{k|k<m}) (J:{k|k<n}) (M:array2D U m n):U:=
nth_range J (nth_range I M).
Implicit Arguments ijth_range [U m n].

Theorem ijth_out: forall (U:Type) (m n:nat) (d:U)
(i j:nat) (M:array2D U m n), i>=m\/j>=n->
ijth d i j M=d.

Theorem ijth_nth: forall (U:Type) (m n i j:nat) (M:array2D U m n)
(d:U) (D:array U n), i<m->j<n->
(ijth d i j M)=(nth d j (nth D i M)).

Corollary ijth_nth_d: forall (U:Type) (m n i j:nat) (M:array2D U m n)
(d:U), i<m->j<n->
(ijth d i j M)=(nth d j (nth ((array_homogeneous U n d)) i M)).

Theorem ijth_error_nth_error_D: forall (U:Type)
(m n i j:nat) (D:array U n) (M:array2D U m n), i<m->j<n->
(ijth_error i j M)=(nth_error j (nth D i M)).

Corollary ijth_error_nth_error_d: forall (U:Type)
(m n i j:nat) (d:U) (M:array2D U m n), i<m->j<n->
(ijth_error i j M)=(nth_error j (nth
 (array_homogeneous U n d) i M)).

Theorem ijth_error_eq: forall (U:Type) (m n:nat) (d:U)
(i j:nat) (M:array2D U m n), i<m->j<n->
ijth_error i j M = value (ijth d i j M).

Theorem ijth_range_eq: forall (U:Type) (m n:nat) (d:U)
(i j:nat) (M:array2D U m n) (Hi:i<m) (Hj:j<n),
ijth_range (exist _ i Hi) (exist _ j Hj) M=
ijth d i j M.

Theorem ijth_range_error_eq: forall (U:Type) (m n:nat) (d:U)
(i j:nat) (M:array2D U m n) (Hi:i<m) (Hj:j<n),
value(ijth_range (exist _ i Hi) (exist _ j Hj) M)=
ijth_error i j M.

Theorem ijth_equality: forall (U:Type) (m n:nat) (d:U)
(A B:array2D U m n),
(forall i j:nat, ijth d i j A=ijth d i j B)->A=B.

Theorem ijth_range_equality: forall (U:Type) (m n:nat)
(A B:array2D U m n),
(forall (I:{i|i<m}) (J:{j|j<n}),
 ijth_range I J A=ijth_range I J B)->A=B.

Theorem ijth_headS: forall (U:Type) (m n:nat) (M:array2D U (S m) n)
(d:U) (j:nat),
ijth d 0 j M=nth d j (headS M).

Theorem ijth_tailS: forall (U:Type) (m n:nat) (M:array2D U (S m) n)
(d:U) (i j:nat),
ijth d (S i) j M=ijth d i j (tailS M).

Theorem ijth_error_headS: forall (U:Type) (m n:nat) (M:array2D U (S m) n)
(j:nat),
ijth_error 0 j M=nth_error j (headS M).

Theorem ijth_error_tailS: forall (U:Type) (m n:nat) (M:array2D U (S m) n)
(i j:nat),
ijth_error (S i) j M=ijth_error i j (tailS M).

Definition matrix_from_func (A:Type) (m n:nat)
(f:nat->nat->A):array2D A m n:=
array_from_func m
(fun i:nat=>array_from_func n (f i)).
Implicit Arguments matrix_from_func [A].

Definition matrix_from_funcrange (A:Type) (m n:nat)
(f:{i|i<m}->{j|j<n}->A):array2D A m n:=
array_from_funcrange m
(fun I:{i|i<m}=>array_from_funcrange n (f I)).
Implicit Arguments matrix_from_funcrange [A].

Theorem matrix_from_func_ijth: forall (A:Type) (m n:nat)
(default:A) (f:nat->nat->A) (i j:nat),
i<m->j<n->
ijth default i j (matrix_from_func m n f)=f i j.

Theorem matrix_from_func_ijth_error:
forall (A:Type) (m n:nat) (f:nat->nat->A) (i j:nat),
i<m->j<n->
ijth_error i j (matrix_from_func m n f)=value(f i j).

Theorem matrix_from_funcrange_ijth_range: forall (U:Type)
(m n:nat) (f:{i|i<m}->{j|j<n}->U) (I:{i|i<m}) (J:{j|j<n}),
ijth_range I J (matrix_from_funcrange m n f)=f I J.

Theorem matrix_from_func_extensionality: forall (U:Type)
(m n:nat) (f g:nat->nat->U)
(EXT:forall m n:nat, f m n= g m n),
matrix_from_func m n f=matrix_from_func m n g.

Theorem matrix_from_funcrange_extensionalityR: forall (U:Type)
(m n:nat) (f g:{i|i<m}->{j|j<n}->U)
(EXT:forall (I:{i|i<m}) (J:{j|j<n}), f I J= g I J),
matrix_from_funcrange m n f=matrix_from_funcrange m n g.

Lemma nth_range_matrix_from_funcrange: forall (U:Type)
(m n:nat) (f:{i|i<m}->{j|j<n}->U) (I:{i|i<m}),
nth_range I (matrix_from_funcrange m n f)=
array_from_funcrange n (f I).

Defined.
Print Column.
Implicit Arguments Column [x x0].
Theorem Column_cons: forall (U:Type) (n:nat)
(C:array U n) (h:U), Column(h::C)=(h::nil U)::Column C.

Theorem Column_tailS: forall (U:Type) (n:nat)
(C:array U (S n)), tailS (Column C)=Column (tailS C).

Theorem Column_headS: forall (U:Type) (n:nat)
(C:array U (S n)), headS (Column C)=headS C::nil U.

Theorem Column_nth: forall (U:Type) (n:nat)
(C:array U n) (d:U) (i:nat), i<n->
nth (d::nil U) i (Column C)=nth d i C::nil U.

Theorem Column_ijth_error: forall (U:Type) (n:nat)
(C:array U n) (i:nat),
ijth_error i 0 (Column C)=nth_error i C.

Theorem Column_ijth: forall (U:Type) (n:nat)
(C:array U n) (d:U) (i:nat), i<n->
ijth d i 0 (Column C)=nth d i C.

Definition VerticalAppend (U:Type) (mA mB n:nat)
(A:array2D U mA n) (B:array2D U mB n):array2D U (mA+mB) n:=A++B.
Implicit Arguments VerticalAppend [U mA mB n].
Infix "+V+" := VerticalAppend (right associativity, at level 60) : matrix_scope.
Open Scope matrix_scope.

Qed.
Implicit Arguments HorizontalAppend [x x0 x1 x2]. Infix "+H+" := HorizontalAppend (right associativity, at level 60) : matrix_scope.

Definition nilC (U:Type) (m:nat):=
array_homogeneous (array U 0) m (nil U).

Lemma array2D_0_nilC: forall (U:Type) (m:nat) (M:array2D U m 0),
M=nilC U m.

Lemma HorizontalAppend_nil2D: forall (U:Type) (m n:nat),
nil2D U m+H+nil2D U n=nil2D U (m+n).

Lemma HorizontalAppend_nil_l: forall (U:Type) (m n:nat)
(B:array2D U m n), nilC U m +H+ B = B.

Lemma HorizontalAppend_nil_r: forall (U:Type) (m n:nat)
(B:array2D U m n), B+H+nilC U m == B.

Theorem HorizontalAppend_ijth_left: forall (U:Type) (m nA nB:nat)
(A:array2D U m nA) (B:array2D U m nB) (d:U) (i j:nat)
(Hi:i<m) (Hj:j<nA),
ijth d i j (A+H+B)=ijth d i j A.

Theorem HorizontalAppend_ijth_right: forall (U:Type) (m nA nB:nat)
(A:array2D U m nA) (B:array2D U m nB) (d:U) (i j:nat)
(Hi:i<m) (Hjl:j>=nA) (Hjr:j<nA+nB),
ijth d i j (A+H+B)=ijth d i (j-nA) B.

Theorem HorizontalAppend_commute_headS: forall (U:Type) (m nA nB:nat)
(A:array2D U (S m) nA) (B:array2D U (S m) nB),
headS (A +H+ B)=(headS A)++(headS B).

Theorem HorizontalAppend_commute_tailS: forall (U:Type) (m nA nB:nat)
(A:array2D U (S m) nA) (B:array2D U (S m) nB),
tailS (A +H+ B)=(tailS A)+H+(tailS B).

Defined.

Defined.
Implicit Arguments ColumnHeadS [x x0 x1]. Implicit Arguments ColumnTailS [x x0 x1].
Lemma ColumnHeadS_nil: forall (U:Type) (n:nat),
ColumnHeadS (nil (array U (S n)))=nil U.

Lemma ColumnTailS_nil: forall (U:Type) (n:nat),
ColumnTailS (nil (array U (S n)))=nil2D U n.

Lemma ColumnCons_HeadS_TailS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)),
Column (ColumnHeadS M)+H+(ColumnTailS M)=M.

Theorem ColumnDestructS: forall (U:Type) (m n:nat) (M:array2D U m (S n)),
{M_body:array2D U m n & {M_head:array U m & M=(Column M_head)+H+M_body}}.
Ltac ColumnDestructS a:=
 let a_body:=fresh a "_body"
 with a_head:=fresh a "_head"
 with aH:=fresh a "H"
 with X:=fresh
 in
assert(X:=ColumnDestructS _ _ _ a);
destruct X as [a_body X];
destruct X as [a_head aH].

Lemma HorizontalAppend_associativeC: forall (U:Type)
(m nA nB:nat) (H:array U m) (A:array2D U m nA) (B:array2D U m nB),
(Column H +H+ A)+H+ B=Column H +H+ (A+H+ B).

Lemma HorizontalAppend_type: forall (U U':Type) (m m' nA nA' nB nB':nat),
U=U'->m=m'->nA=nA'->nB=nB'->
@HorizontalAppend U m nA nB==@HorizontalAppend U' m' nA' nB'.


Theorem HorizontalAppend_associative: forall (U:Type)
(m nA nB nC:nat)
(A:array2D U m nA) (B:array2D U m nB) (C:array2D U m nC),
(A+H+B)+H+C==A+H+(B+H+C).

Theorem HorizontalAppend_commuteC: forall (U:Type) (m n:nat)
(C:array U m) (M:array2D U m n) (d:U) (i:nat),
nth (array_homogeneous U (S n) d) i (Column C +H+ M)=
(nth (array_homogeneous U 1 d) i (Column C))++
(nth (array_homogeneous U n d) i M).

Theorem HorizontalAppend_commute: forall (U:Type) (m nA nB:nat)
(A:array2D U m nA) (B:array2D U m nB) (d:U) (i:nat),
nth (array_homogeneous U (nA+nB) d) i (A +H+ B)=
(nth (array_homogeneous U nA d) i A)++
(nth (array_homogeneous U nB d) i B).

Theorem ColumnHeadS_Column: forall (U:Type)
(m:nat) (C:array U m),
ColumnHeadS (Column C)=C.

Theorem ColumnTailS_Column: forall (U:Type)
(m:nat) (C:array U m),
ColumnTailS (Column C)=nilC U m.

Theorem VerticalAppend_Column: forall (U:Type)
(mA mB:nat) (A:array U mA) (B:array U mB),
Column (A++B) = Column A ++ Column B.

Lemma array2D_1_Column: forall (U:Type) (m:nat) (M:array2D U m 1),
{C|Column C=M}.

Theorem HorizontalAppend_ColumnHeadS_C: forall (U:Type) (m n:nat)
(C:array U m) (M:array2D U m n),
ColumnHeadS (Column C +H+ M) = C.

Theorem HorizontalAppend_ColumnHeadS: forall (U:Type) (m nA nB:nat)
(A:array2D U m (S nA)) (B:array2D U m nB),
ColumnHeadS (A +H+ B) = ColumnHeadS A.

Theorem HorizontalAppend_ColumnTailS_C: forall (U:Type) (m n:nat)
(C:array U m) (M:array2D U m n),
ColumnTailS (Column C +H+ M) = M.

Theorem HorizontalAppend_ColumnTailS: forall (U:Type) (m nA nB:nat)
(A:array2D U m (S nA)) (B:array2D U m nB),
ColumnTailS (A+H+B) = ColumnTailS A +H+ B.

Lemma AppendCommuteDimensions_RC: forall (U:Type)
(m n:nat)
(UL:U) (UR:array U n)
(DL:array U m) (DR:array2D U m n),
(UL::UR)::(Column DL +H+ DR)=Column (UL::DL)+H+(UR::DR).

Lemma AppendCommuteDimensions_R: forall (U:Type)
(m nL nR:nat)
(UL:array U nL) (UR:array U nR)
(DL:array2D U m nL) (DR:array2D U m nR),
(UL ++ UR)::(DL +H+ DR)=(UL::DL)+H+(UR::DR).

Theorem AppendCommuteDimensions: forall (U:Type)
(mU mD nL nR:nat)
(UL:array2D U mU nL) (UR:array2D U mU nR)
(DL:array2D U mD nL) (DR:array2D U mD nR),
(UL +H+ UR)++(DL +H+ DR)=(UL++DL)+H+(UR++DR).

Theorem VerticalAppend_commute_ColumnHeadS_C: forall (U:Type)
(mA mB:nat) (A:array U mA) (B:array U mB),
ColumnHeadS (Column A ++ Column B) = A ++ B.

Theorem VerticalAppend_commute_ColumnHeadS: forall (U:Type)
(mA mB n:nat) (A:array2D U mA (S n)) (B:array2D U mB (S n)),
ColumnHeadS (A++B)=ColumnHeadS A++ ColumnHeadS B.

Theorem VerticalAppend_commute_ColumnTailS: forall (U:Type)
(mA mB n:nat) (A:array2D U mA (S n)) (B:array2D U mB (S n)),
ColumnTailS (A++B)=ColumnTailS A++ ColumnTailS B.

Definition Transpose_type (U:Type) (m m' n:nat) (E:m=S m')
:array2D U n (1 + m')=array2D U n m.
Defined.
Definition Transpose_Ctype (U:Type) (m n:nat) (E:m=0)
:array (array U 0) n=array2D U n m.
Defined.
Defined.
Implicit Arguments Transpose [x x0 x1].
Theorem Transpose_nil: forall (U:Type) (n:nat),
Transpose (nil (array U n))=nilC U n.

Theorem Column_eq_Transpose: forall (U:Type) (n:nat)
(C:array U n), Column C=Transpose (C::nil2D U n).

Definition nthC_type (U:Type) (m n n':nat) (E:n=S n'):
array2D U m n=array2D U m (S n').
Defined.
Fixpoint nthC (U:Type) (m n:nat) (D:array U m) (i:nat) (M:array2D U m n)
:array U m:=
match i,nat_destruct n with
|O,inleft Dn =>
 let (n',E):=Dn in
 ColumnHeadS (maptype (nthC_type U m n n' E) M)
|S i',inleft Dn =>
 let (n',E):=Dn in
 nthC U m n' D i' (ColumnTailS (maptype (nthC_type U m n n' E) M))
|_,_=>D
end.
Implicit Arguments nthC [U m n].

Fixpoint nthC_error (U:Type) (m n:nat) (i:nat) (M:array2D U m n)
:Exc (array U m):=
match i,nat_destruct n with
|O,inleft Dn =>
 let (n',E):=Dn in
 value (ColumnHeadS (maptype (nthC_type U m n n' E) M))
|S i',inleft Dn =>
 let (n',E):=Dn in
 nthC_error U m n' i' (ColumnTailS (maptype (nthC_type U m n n' E) M))
|_,_=>error
end.
Implicit Arguments nthC_error [U m n].

Definition nthC_range (U:Type) (m n:nat) (J:{j|j<n})
(M:array2D U m n):array U m.
Defined.
Implicit Arguments nthC_range [U m n].

Theorem nthC_out: forall (U:Type) (m n:nat)
(M:array2D U m n) (D:array U m) (i:nat),
i>=n -> nthC D i M=D.

Theorem nthC_error_out: forall (U:Type) (m n:nat)
(M:array2D U m n) (i:nat), i>=n -> nthC_error i M=error.

Theorem nthC_error_eq: forall (U:Type) (m n:nat) (D:array U m)
(i:nat) (M:array2D U m n), i<n ->
nthC_error i M = value (nthC D i M).

Lemma nthC_anydefault: forall (U:Type) (m n:nat)
(D1 D2:array U m)
(j:nat) (M:array2D U m n), j<n ->
nthC D1 j M = nthC D2 j M.

Lemma nthC_range_eq: forall (U:Type) (m n:nat) (D:array U m)
(j:nat) (M:array2D U m n) (Hj:j<n),
nthC_range (exist _ j Hj) M=nthC D j M.

Theorem nthC_ColumnHeadS: forall (U:Type) (m n:nat)
(M:array2D U m (S n))
(D:array U m), nthC D 0 M=ColumnHeadS M.

Theorem nthC_ColumnTailS: forall (U:Type) (m n:nat)
(M:array2D U m (S n))
(D:array U m) (j:nat), nthC D (S j) M=nthC D j (ColumnTailS M).

Theorem nthC_error_ColumnHeadS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)), nthC_error 0 M=value (ColumnHeadS M).

Theorem nthC_error_ColumnTailS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)) (j:nat),
nthC_error (S j) M=nthC_error j (ColumnTailS M).

Theorem nthC_range_ColumnHeadS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)) (H:0<S n),
nthC_range (exist _ 0 H) M=ColumnHeadS M.

Theorem nthC_range_ColumnTailS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)) (j:nat) (Hj:S j<S n),
nthC_range (exist _ (S j) Hj) M=
nthC_range (exist _ j (lt_S_n j n Hj)) (ColumnTailS M).

Theorem VerticalAppend_commuteR: forall (U:Type) (m n:nat)
(R:array U n) (M:array2D U m n) (d:U) (j:nat),
nthC (array_homogeneous U (S m) d) j (R::M)=
(nthC (array_homogeneous U 1 d) j (R::nil2D U n))++
(nthC (array_homogeneous U m d) j M).

Theorem VerticalAppend_commute: forall (U:Type) (mA mB n:nat)
(A:array2D U mA n) (B:array2D U mB n) (d:U) (j:nat),
nthC (array_homogeneous U (mA+mB) d) j (A ++ B)=
(nthC (array_homogeneous U mA d) j A)++
(nthC (array_homogeneous U mB d) j B).

Theorem HorizontalAppend_nthC_left: forall (U:Type) (m nA nB:nat)
(A:array2D U m nA) (B:array2D U m nB) (d:U) (j:nat),j<nA->
nthC (array_homogeneous U m d) j (A+H+B)=
nthC (array_homogeneous U m d) j A.

Theorem HorizontalAppend_nthC_right: forall (U:Type) (m nA nB:nat)
(A:array2D U m nA) (B:array2D U m nB) (d:U) (j:nat)
(Hl:j>=nA) (Hr:j<nA+nB),
nthC (array_homogeneous U m d) j (A+H+B)=
nthC (array_homogeneous U m d) (j-nA) B.

Theorem headS_ColumnHeadS: forall (U:Type) (m n:nat)
(M:array2D U (S m) (S n)),
headS (ColumnHeadS M) = headS (headS M).

Theorem headS_ColumnTailS: forall (U:Type) (m n:nat)
(M:array2D U (S m) (S n)),
headS (ColumnTailS M) = tailS (headS M).

Theorem tailS_ColumnHeadS: forall (U:Type) (m n:nat)
(M:array2D U (S m) (S n)),
tailS (ColumnHeadS M) = ColumnHeadS (tailS M).

Theorem tailS_ColumnTailS: forall (U:Type) (m n:nat)
(M:array2D U (S m) (S n)),
tailS (ColumnTailS M) = ColumnTailS (tailS M).

Theorem nthC_headS: forall (U:Type) (m n:nat)
(M:array2D U (S m) n) (d:U) (j:nat),
headS (nthC (array_homogeneous U (S m) d) j M)=
nth d j (headS M).

Theorem nthC_tailS: forall (U:Type) (m n:nat)
(M:array2D U (S m) n) (d:U) (j:nat),
tailS (nthC (array_homogeneous U (S m) d) j M)=
nthC (array_homogeneous U m d) j (tailS M).

Theorem nth_ColumnHeadS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)) (d:U) (i:nat),
nth d i (ColumnHeadS M)=
headS (nth (array_homogeneous U (S n) d) i M).

Theorem nth_ColumnTailS: forall (U:Type) (m n:nat)
(M:array2D U m (S n)) (d:U) (i:nat),
nth (array_homogeneous U n d) i (ColumnTailS M)=
tailS (nth (array_homogeneous U (S n) d) i M).

Lemma nthC_nth_R: forall (U:Type) (m n:nat) (M:array2D U (S m) n)
(d:U) (D:array U (S m)) (j:nat), j<n->
nth d 0 (nthC D j M)=ijth d 0 j M.

Theorem nthC_nth: forall (U:Type) (m n:nat) (M:array2D U m n)
(d:U) (D:array U m) (i j:nat), i<m->j<n->
nth d i (nthC D j M)=ijth d i j M.

Theorem headS_Transpose: forall (U:Type) (m n:nat)
(M:array2D U m (S n)),
headS (Transpose M)=ColumnHeadS M.

Theorem tailS_Transpose: forall (U:Type) (m n:nat)
(M:array2D U m (S n)),
tailS (Transpose M)=Transpose (ColumnTailS M).

Theorem ColumnHeadS_Transpose: forall (U:Type) (m n:nat)
(M:array2D U (S m) n),
ColumnHeadS (Transpose M)=headS M.

Theorem ColumnTailS_Transpose: forall (U:Type) (m n:nat)
(M:array2D U (S m) n),
ColumnTailS (Transpose M)=Transpose (tailS M).

Theorem TransposeTranspose: forall (U:Type) (m n:nat)
(M:array2D U m n),
Transpose (Transpose M)=M.

Theorem Transpose_nth: forall (U:Type) (m n:nat) (M:array2D U m n)
(D:array U m) (d:U) (j:nat), j<n->
nth D j (Transpose M)=nthC D j M.

Theorem Transpose_nthC: forall (U:Type) (m n:nat) (M:array2D U m n)
(D:array U n) (d:U) (i:nat), i<m->
nthC D i (Transpose M)=nth D i M.

Theorem Transpose_nth_range: forall (U:Type) (m n:nat) (M:array2D U m n)
(J:{j|j<n}),
nth_range J (Transpose M)=nthC_range J M.

Theorem Transpose_nthC_range: forall (U:Type) (m n:nat) (M:array2D U m n)
(I:{i|i<m}),
nthC_range I (Transpose M)=nth_range I M.

Theorem Transpose_ijth: forall (U:Type) (m n:nat) (M:array2D U m n)
(d:U) (i j:nat), i<m->j<n->
ijth d j i (Transpose M)=ijth d i j M.

Theorem Transpose_ijth_range: forall (U:Type) (m n:nat) (M:array2D U m n)
(I:{i|i<m}) (J:{j|j<n}),
ijth_range J I (Transpose M)=ijth_range I J M.

Lemma nthC_matrix_from_func: forall (U:Type)
(m n:nat) (f:nat->nat->U) (j:nat) (d:U) (Hj:j<n),
nthC (array_homogeneous U _ d) j (matrix_from_func m n f)=
array_from_func m (fun i=>f i j).

Lemma nthC_range_nth_range: forall (U:Type)
(m n:nat) (M:array2D U m n)
(I:{i|i<m}) (J:{j|j<n}),
nth_range I (nthC_range J M)=ijth_range I J M.

Lemma nthC_range_matrix_from_funcrange: forall (U:Type)
(m n:nat) (f:{i|i<m}->{j|j<n}->U) (J:{j|j<n}),
nthC_range J (matrix_from_funcrange m n f)=
array_from_funcrange m (fun I=>f I J).

Definition ZeroMatrix (U:Type) (m n:nat) (z:U):=
array_homogeneous (array U n) m
(array_homogeneous U n z).

Theorem ZeroMatrix_ijth: forall (U:Type) (m n:nat) (z d:U) (i j:nat),
i<m->j<n->ijth d i j (ZeroMatrix U m n z)=z.

Theorem ZeroMatrix_ijth_range: forall (U:Type) (m n:nat) (z:U)
(I:{i|i<m}) (J:{j|j<n}),
ijth_range I J (ZeroMatrix U m n z)=z.

Definition IdentityMatrix (U:Type) (m n:nat) (z v:U):=
array_from_func m (UnitVector n z v).

Theorem IdentityMatrix_ijth: forall (U:Type) (m n:nat)
(z v d:U) (i j:nat), i<m->j<n->
ijth d i j (IdentityMatrix U m n z v)=
Kronecker_delta z v i j.

Theorem IdentityMatrix_ijth_range: forall (U:Type) (m n:nat)
(z v:U) (i j:nat) (Hi:i<m) (Hj:j<n),
ijth_range (exist _ i Hi) (exist _ j Hj) (IdentityMatrix U m n z v)=
Kronecker_delta z v i j.

Definition MatrixSymmetric (U:Type) (n:nat) (M:array2D U n n):=
Transpose M=M.
Implicit Arguments MatrixSymmetric [U n].

Theorem MatrixSymmetric_ijth: forall (U:Type) (n:nat)
(M:array2D U n n) (i j:nat) (d:U), MatrixSymmetric M->
ijth d i j M=ijth d j i M.

Theorem MatrixSymmetric_ijth_range: forall (U:Type) (n:nat)
(M:array2D U n n) (I J:{i|i<n}), MatrixSymmetric M->
ijth_range I J M=ijth_range J I M.

Lemma ZeroMatrix_Transpose: forall (U:Type) (m n:nat) (z:U),
Transpose (ZeroMatrix U m n z)=ZeroMatrix U n m z.

Lemma ZeroMatrix_Symmetric: forall (U:Type) (n:nat) (z:U),
MatrixSymmetric (ZeroMatrix U n n z).

Lemma IdentityMatrix_Transpose: forall (U:Type) (m n:nat) (z v:U),
Transpose (IdentityMatrix U m n z v)=IdentityMatrix U n m z v.

Lemma IdentityMatrix_Symmetric: forall (U:Type) (n:nat) (z v:U),
MatrixSymmetric (IdentityMatrix U n n z v).