From c7689a42d1c636ec6e0fe1e5d8611fcd70c21da9 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 1 Jun 2024 23:26:55 +0200 Subject: [PATCH 1/4] theory of diagonal matrices Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 172 +++++++++++++++++++++++++++++++- 1 file changed, 167 insertions(+), 5 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 9cff446b96d..e78ba24973f 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -310,16 +310,178 @@ Defined. (** ** Diagonal matrices *) -(** A diagonal matrix is a matrix with zeros everywhere except on the diagonal. *) -Definition diagonal_matrix {R : Ring@{i}} {n : nat} (v : list R) (p : length v = n) +(** A diagonal matrix is a matrix with zeros everywhere except on the diagonal. It's entries are given by a vector. *) +Definition matrix_diag {R : Ring@{i}} {n : nat} (v : Vector R n) : Matrix R n n. Proof. snrapply Build_Matrix. intros i j H1 H2. - destruct (dec (i = j)). + exact (kronecker_delta i j * Vector.entry v i). +Defined. + +(** Addition of matrices is the same as addition of the corresponding vectors. *) +Definition matrix_diag_plus {R : Ring@{i}} {n : nat} (v w : Vector R n) + : matrix_plus (matrix_diag v) (matrix_diag w) = matrix_diag (vector_plus v w). +Proof. + snrapply path_matrix. + intros i j Hi Hj. + rewrite 2 entry_Build_Matrix, 4 entry_Build_Vector. + cbv beta zeta; destruct (dec (i = j)) as [p | np]. - destruct p. - exact (nth' v i H1). - - exact 0. + rewrite kronecker_delta_refl. + rewrite <- rng_dist_l. + by rewrite entry_Build_Vector. + - rewrite (kronecker_delta_neq np). + by rewrite 3 rng_mult_zero_l, rng_plus_zero_l. +Defined. + +(** Matrix multiplication of diagonal matrices is the same as multiplying the corresponding vectors pointwise. *) +Definition matrix_diag_mult {R : Ring} {n : nat} (v w : Vector R n) + : matrix_mult (matrix_diag v) (matrix_diag w) + = matrix_diag (vector_map2 (.*.) v w). +Proof. + snrapply path_matrix. + intros i j Hi Hj. + rewrite 2 entry_Build_Matrix. + lhs snrapply path_ab_sum. + { intros k Hk. + rewrite 2 entry_Build_Matrix. + rewrite rng_mult_assoc. + rewrite <- (rng_mult_assoc (kronecker_delta _ _ )). + rewrite kronecker_delta_comm. + rewrite <- 2 rng_mult_assoc. + reflexivity. } + rewrite (rng_sum_kronecker_delta_l _ _ Hi). + by rewrite entry_Build_Vector. +Defined. + +(** The transpose of a diagonal matrix is the same diagonal matrix. *) +Definition matrix_transpose_diag {R : Ring} {n : nat} (v : Vector R n) + : matrix_transpose (matrix_diag v) = matrix_diag v. +Proof. + snrapply path_matrix. + intros i j Hi Hj. + rewrite 3 entry_Build_Matrix. + rewrite kronecker_delta_symm. + unfold kronecker_delta. + destruct (dec (i = j)) as [p|np]. + 1: destruct p; f_ap; f_ap; apply path_ishprop. + by rewrite !rng_mult_zero_l. +Defined. + +(** The diagonal matrix construction is injective. *) +Global Instance isinj_matrix_diag {R : Ring} {n : nat} + : IsInjective (@matrix_diag R n). +Proof. + intros v1 v2 p. + snrapply path_vector. + intros i Hi. + apply (ap (fun M => entry M i i)) in p. + rewrite 2 entry_Build_Matrix in p. + rewrite kronecker_delta_refl in p. + by rewrite 2 rng_mult_one_l in p. +Defined. + +(** A matrix is diagonal if it is equal to a diagonal matrix. *) +Class IsDiagonal {R : Ring@{i}} {n : nat} (M : Matrix R n n) : Type@{i} := { + isdiagonal_diag_vector : Vector R n; + isdiagonal_diag : M = matrix_diag isdiagonal_diag_vector; +}. + +Arguments isdiagonal_diag_vector {R n} M {_}. +Arguments isdiagonal_diag {R n} M {_}. + +Definition issig_IsDiagonal {R : Ring} {n : nat} {M : Matrix R n n} + : _ <~> IsDiagonal M + := ltac:(issig). + +(** A matrix is diagonal in a unique way. *) +Global Instance ishprop_isdiagonal {R : Ring} {n : nat} (M : Matrix R n n) + : IsHProp (IsDiagonal M). +Proof. + snrapply hprop_allpath. + intros x y. + snrapply ((equiv_ap' issig_IsDiagonal^-1%equiv _ _ )^-1%equiv). + rapply path_sigma_hprop; cbn. + apply isinj_matrix_diag. + exact ((isdiagonal_diag M)^ @ isdiagonal_diag M). +Defined. + +(** The zero matrix is diagonal. *) +Global Instance isdiagonal_matrix_zero {R : Ring} {n : nat} + : IsDiagonal (matrix_zero R n n). +Proof. + exists (vector_zero R n). + snrapply path_matrix. + intros i j Hi Hj. + rewrite 2 entry_Build_Matrix, entry_Build_Vector. + by rewrite rng_mult_zero_r. +Defined. + +(** The identity matrix is diagonal. *) +Global Instance isdiagonal_identity_matrix {R : Ring} {n : nat} + : IsDiagonal (identity_matrix R n). +Proof. + exists (Build_Vector R n (fun _ _ => 1)). + snrapply path_matrix. + intros i j Hi Hj. + rewrite 2 entry_Build_Matrix, entry_Build_Vector. + by rewrite rng_mult_one_r. +Defined. + +(** The sum of two diagonal matrices is diagonal. *) +Global Instance isdiagonal_matrix_plus {R : Ring} {n : nat} (M N : Matrix R n n) + `{IsDiagonal R n M} `{IsDiagonal R n N} + : IsDiagonal (matrix_plus M N). +Proof. + exists (vector_plus (isdiagonal_diag_vector M) (isdiagonal_diag_vector N)). + rewrite (isdiagonal_diag M), (isdiagonal_diag N). + apply matrix_diag_plus. +Defined. + +(** The negative of a diagonal matrix is diagonal. *) +Global Instance isdiagonal_matrix_negate {R : Ring} {n : nat} (M : Matrix R n n) + `{IsDiagonal R n M} + : IsDiagonal (matrix_negate M). +Proof. + exists (vector_neg _ _ (isdiagonal_diag_vector M)). + rewrite (isdiagonal_diag M). + snrapply path_matrix. + intros i j Hi Hj. + rewrite !entry_Build_Matrix, !entry_Build_Vector. + by rewrite rng_mult_negate_r. +Defined. + +(** The product of two diagonal matrices is diagonal. *) +Global Instance isdiagonal_matrix_mult {R : Ring} {n : nat} (M N : Matrix R n n) + `{IsDiagonal R n M} `{IsDiagonal R n N} + : IsDiagonal (matrix_mult M N). +Proof. + exists (vector_map2 (.*.) (isdiagonal_diag_vector M) (isdiagonal_diag_vector N)). + rewrite (isdiagonal_diag M), (isdiagonal_diag N). + apply matrix_diag_mult. +Defined. + +(** The transpose of a diagonal matrix is diagonal. *) +Global Instance isdiagonal_matrix_transpose {R : Ring} {n : nat} (M : Matrix R n n) + `{IsDiagonal R n M} + : IsDiagonal (matrix_transpose M). +Proof. + exists (isdiagonal_diag_vector M). + rewrite (isdiagonal_diag M). + apply matrix_transpose_diag. +Defined. + +(** Given a square matrix, we can extract the diagonal as a vector. *) +Definition matrix_diag_vector {R : Ring} {n : nat} (M : Matrix R n n) + : Vector R n + := Build_Vector R n (fun i _ => entry M i i). + +(** Diagonal matrices form a subring of the ring of square matrices. *) +Definition matrix_diag_ring (R : Ring) (n : nat) : Subring (matrix_ring R n). +Proof. + snrapply (Build_Subring' (fun M : matrix_ring R n => IsDiagonal M)); + cbn beta; exact _. Defined. (** ** Trace *) From 40e5962fba95401cfb4aeb3d54d038736acd8724 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 3 Jun 2024 13:21:30 +0200 Subject: [PATCH 2/4] speed up matrix_diag_ring Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index e78ba24973f..5382b048aa3 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -480,8 +480,13 @@ Definition matrix_diag_vector {R : Ring} {n : nat} (M : Matrix R n n) (** Diagonal matrices form a subring of the ring of square matrices. *) Definition matrix_diag_ring (R : Ring) (n : nat) : Subring (matrix_ring R n). Proof. - snrapply (Build_Subring' (fun M : matrix_ring R n => IsDiagonal M)); - cbn beta; exact _. + snrapply (Build_Subring' (fun M : matrix_ring R n => IsDiagonal M) _); hnf. + - intros; exact _. + - intros x y dx dy. + nrapply isdiagonal_matrix_plus; trivial. + by nrapply isdiagonal_matrix_negate. + - nrapply isdiagonal_matrix_mult. + - nrapply isdiagonal_identity_matrix. Defined. (** ** Trace *) From b312fba68f6e1e5e96f662a7ec491f2f4474f5be Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 3 Jun 2024 13:47:27 +0200 Subject: [PATCH 3/4] reivew suggestions Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 19 +++++++------------ theories/Algebra/Rings/Vector.v | 7 +++++++ 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 5382b048aa3..9a3e4f3fc29 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -310,7 +310,7 @@ Defined. (** ** Diagonal matrices *) -(** A diagonal matrix is a matrix with zeros everywhere except on the diagonal. It's entries are given by a vector. *) +(** A diagonal matrix is a matrix with zeros everywhere except on the diagonal. Its entries are given by a vector. *) Definition matrix_diag {R : Ring@{i}} {n : nat} (v : Vector R n) : Matrix R n n. Proof. @@ -319,20 +319,15 @@ Proof. exact (kronecker_delta i j * Vector.entry v i). Defined. -(** Addition of matrices is the same as addition of the corresponding vectors. *) +(** Addition of diagonal matrices is the same as addition of the corresponding vectors. *) Definition matrix_diag_plus {R : Ring@{i}} {n : nat} (v w : Vector R n) : matrix_plus (matrix_diag v) (matrix_diag w) = matrix_diag (vector_plus v w). Proof. + symmetry. snrapply path_matrix. intros i j Hi Hj. - rewrite 2 entry_Build_Matrix, 4 entry_Build_Vector. - cbv beta zeta; destruct (dec (i = j)) as [p | np]. - - destruct p. - rewrite kronecker_delta_refl. - rewrite <- rng_dist_l. - by rewrite entry_Build_Vector. - - rewrite (kronecker_delta_neq np). - by rewrite 3 rng_mult_zero_l, rng_plus_zero_l. + rewrite 2 entry_Build_Matrix, 5 entry_Build_Vector. + nrapply rng_dist_l. Defined. (** Matrix multiplication of diagonal matrices is the same as multiplying the corresponding vectors pointwise. *) @@ -347,7 +342,7 @@ Proof. { intros k Hk. rewrite 2 entry_Build_Matrix. rewrite rng_mult_assoc. - rewrite <- (rng_mult_assoc (kronecker_delta _ _ )). + rewrite <- (rng_mult_assoc (kronecker_delta _ _)). rewrite kronecker_delta_comm. rewrite <- 2 rng_mult_assoc. reflexivity. } @@ -365,7 +360,7 @@ Proof. rewrite kronecker_delta_symm. unfold kronecker_delta. destruct (dec (i = j)) as [p|np]. - 1: destruct p; f_ap; f_ap; apply path_ishprop. + 1: destruct p; f_ap; apply path_entry_vector. by rewrite !rng_mult_zero_l. Defined. diff --git a/theories/Algebra/Rings/Vector.v b/theories/Algebra/Rings/Vector.v index cee4c64c4ef..d52b3bd2a47 100644 --- a/theories/Algebra/Rings/Vector.v +++ b/theories/Algebra/Rings/Vector.v @@ -61,6 +61,13 @@ Proof. 1, 2: apply nth'_nth'. Defined. +Definition path_entry_vector {A : Type} {n : nat} (v : Vector A n) + (i : nat) (Hi Hi' : (i < n)%nat) + : @entry _ _ v i Hi = @entry _ _ v i Hi'. +Proof. + apply nth'_nth'. +Defined. + (** ** Operations *) Definition vector_map {A B : Type} {n} (f : A -> B) From fde5a49796419206e202413ebb954004a96230fd Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 3 Jun 2024 15:48:45 +0200 Subject: [PATCH 4/4] generalise path_entry_vector Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 2 +- theories/Algebra/Rings/Vector.v | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 9a3e4f3fc29..549c8f8e517 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -360,7 +360,7 @@ Proof. rewrite kronecker_delta_symm. unfold kronecker_delta. destruct (dec (i = j)) as [p|np]. - 1: destruct p; f_ap; apply path_entry_vector. + 1: f_ap; symmetry; by apply path_entry_vector. by rewrite !rng_mult_zero_l. Defined. diff --git a/theories/Algebra/Rings/Vector.v b/theories/Algebra/Rings/Vector.v index d52b3bd2a47..e258506ede2 100644 --- a/theories/Algebra/Rings/Vector.v +++ b/theories/Algebra/Rings/Vector.v @@ -62,9 +62,10 @@ Proof. Defined. Definition path_entry_vector {A : Type} {n : nat} (v : Vector A n) - (i : nat) (Hi Hi' : (i < n)%nat) - : @entry _ _ v i Hi = @entry _ _ v i Hi'. + (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) (p : i = j) + : entry v i = entry v j. Proof. + destruct p. apply nth'_nth'. Defined.