From e1feb0b9d4ef955934a508232f5abff8c3597cbd Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 1 Jun 2024 23:54:58 +0200 Subject: [PATCH 1/8] centrosymmetric matrices Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 166 ++++++++++++++++++++++++++++++++ 1 file changed, 166 insertions(+) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 47865e93b45..922dff1ce20 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1018,6 +1018,172 @@ Defined. (** Skew-symmetric matrices degenerate to symmetric matrices in rings with characteristic 2. In odd characteristic the module of matrices can be decomposed into the direct sum of symmetric and skew-symmetric matrices. *) +(** ** Exchange matrix *) + +(** The exchange matrix is the matrix with ones on the anti-diagonal and zeros elsewhere. It will play an important role in defining classes of matrices with certain symmetric properties. *) +Definition exchange_matrix (R : Ring) n : Matrix R n n + := Build_Matrix R n n (fun i j Hi Hj + => kronecker_delta (R:=R) (i + j) (pred n))%nat. + +(** Multiplying a matrix by the exchange matrix on the left is equivalent to exchanging the rows. Similarly multiplying on the right exchanges the columns. *) + +(** The exchange matrix is invariant under transpose. *) +Definition exchange_matrix_transpose {R n} + : matrix_transpose (exchange_matrix R n) = exchange_matrix R n. +Proof. + apply path_matrix. + intros i j Hi Hj. + rewrite 3 entry_Build_Matrix. + by rewrite nat_add_comm. +Defined. + +(** The exchange matrix is symmetric. *) +Global Instance issymmetric_exchange {R : Ring} {n : nat} + : IsSymmetric (exchange_matrix R n) + := exchange_matrix_transpose. + +(** The exchange matrix has order 2. This proof is only long because of arithmetic. *) +Definition exchange_matrix_square {R : Ring} {n : nat} + : matrix_mult (exchange_matrix R n) (exchange_matrix R n) = identity_matrix R n. +Proof. + apply path_matrix. + intros i j Hi Hj. + assert (r : (i <= pred n)%nat) by auto with nat. + rewrite 2 entry_Build_Matrix. + lhs nrapply path_ab_sum. + { intros k Hk. + rewrite entry_Build_Matrix. + rewrite <- (nat_add_sub_eq _ r). + unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => i + x)). + 2: reflexivity. + intros x y H; exact (isinj_nat_add_l i x y H). } + unshelve erewrite rng_sum_kronecker_delta_l'. + { unfold Core.lt. + destruct n. + 1: by apply not_lt_n_0 in Hi. + auto with nat. } + rewrite entry_Build_Matrix. + set (t := (pred n - i + j)%nat). + rewrite <- (natminuspluseq _ _ r). + unfold t; clear t. + unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat). + 2: apply kronecker_delta_symm. + intros x y H. + exact (isinj_nat_add_l _ _ _ H). +Defined. + +(** ** Centrosymmetric matrices *) + +(** A centrosymmetric matrix is symmetric about its center. *) +Class IsCentrosymmetric {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Type@{i} + := exchange_matrix_iscentrosymmetric + : matrix_mult (exchange_matrix R n) M = matrix_mult M (exchange_matrix R n). + +Global Instance ishprop_iscentrosymmetric {R : Ring@{i}} {n : nat} (M : Matrix R n n) + : IsHProp (IsCentrosymmetric M). +Proof. + unfold IsCentrosymmetric; exact _. +Defined. + +(** The zero matrix is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_zero {R : Ring@{i}} {n : nat} + : IsCentrosymmetric (matrix_zero R n n) + := rng_mult_zero_r (A:=matrix_ring R n) _ @ (rng_mult_zero_l _)^. + +(** The identity matrix is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_identity {R : Ring@{i}} {n : nat} + : IsCentrosymmetric (identity_matrix R n) + := rng_mult_one_r (A:=matrix_ring R n) _ @ (rng_mult_one_l _)^. + +(** The sum of two centrosymmetric matrices is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_plus {R : Ring@{i}} {n : nat} + (M N : Matrix R n n) {H1 : IsCentrosymmetric M} {H2 : IsCentrosymmetric N} + : IsCentrosymmetric (matrix_plus M N). +Proof. + unfold IsCentrosymmetric. + lhs nrapply (rng_dist_l (A:=matrix_ring R n)). + rhs nrapply (rng_dist_r (A:=matrix_ring R n)). + cbn; by rewrite H1, H2. +Defined. + +(** The negation of a centrosymmetric matrix is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_negate {R : Ring@{i}} {n : nat} + (M : Matrix R n n) {H : IsCentrosymmetric M} + : IsCentrosymmetric (matrix_negate M). +Proof. + unfold IsCentrosymmetric. + lhs nrapply (rng_mult_negate_r (A:=matrix_ring R n) _). + rhs nrapply (rng_mult_negate_l (A:=matrix_ring R n) _). + f_ap. +Defined. + +(** A scalar multiple of a centrosymmetric matrix is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_scale {R : Ring@{i}} {n : nat} + (r : R) (M : Matrix R n n) {H : IsCentrosymmetric M} + : IsCentrosymmetric (matrix_lact r M). +Proof. + unfold IsCentrosymmetric. + (** TODO: Need associative algebra structure. *) +Abort. + +(** A centrosymmetric matrix is also centrosymmetric when considered over the opposite ring. *) +Global Instance iscentrosymmetric_rng_op {R : Ring@{i}} {n : nat} (M : Matrix R n n) + `{!IsCentrosymmetric M} + : IsCentrosymmetric (R := rng_op R) M. +Proof. + hnf. + apply path_matrix. + intros i j Hi Hj. + rewrite 2 entry_Build_Matrix. + pose (p := exchange_matrix_iscentrosymmetric). + apply (ap (fun x => entry x i j)) in p. + rewrite 2 entry_Build_Matrix in p. + refine (_ @ p @ _). + - apply path_ab_sum. + intros k Hk. + rewrite 2 entry_Build_Matrix. + rapply kronecker_delta_comm. + - apply path_ab_sum. + intros k Hk. + rewrite 2 entry_Build_Matrix. + rapply kronecker_delta_comm. +Defined. + +(** The transpose of a centrosymmetric matrix is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_transpose {R : Ring@{i}} {n : nat} + (M : Matrix R n n) {H : IsCentrosymmetric M} + : IsCentrosymmetric (matrix_transpose M). +Proof. + unfold IsCentrosymmetric. + rewrite <- exchange_matrix_transpose. + lhs_V nrapply (matrix_transpose_mult (R:=rng_op R) M (exchange_matrix R n)). + rhs_V nrapply (matrix_transpose_mult (R:=rng_op R) (exchange_matrix R n) M). + pose (iscentrosymmetric_rng_op M). + f_ap. + symmetry. + rapply (exchange_matrix_iscentrosymmetric (R:=rng_op R)). +Defined. + +(** The product of two centrosymmetric matrices is centrosymmetric. *) +Global Instance iscentrosymmetric_matrix_mult {R : Ring@{i}} {n : nat} + (M N : Matrix R n n) {H1 : IsCentrosymmetric M} {H2 : IsCentrosymmetric N} + : IsCentrosymmetric (matrix_mult M N). +Proof. + lhs nrapply (rng_mult_assoc (A:=matrix_ring R n)). + rhs_V nrapply (rng_mult_assoc (A:=matrix_ring R n)). + hnf in H1, H2; cbn. + rewrite H1. + lhs_V nrapply (rng_mult_assoc (A:=matrix_ring R n)); f_ap. +Defined. + +(** Centrosymmetric rings form a subring of the matrix ring. *) +Definition centrosymmetric_matrix_ring (R : Ring@{i}) (n : nat) + : Subring (matrix_ring R n). +Proof. + nrapply (Build_Subring' (fun M : matrix_ring R n => IsCentrosymmetric M)); + cbn beta; exact _. +Defined. + Section MatrixCat. (** The wild category [MatrixCat R] of [R]-valued matrices. This category has natural numbers as objects and m x n matrices as the arrows between [m] and [n]. *) From c2d194f41916ef2d63502f1361b6b1ecde950c1c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 1 Jul 2024 15:29:46 +0200 Subject: [PATCH 2/8] review suggestions Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 57 ++++++++++++++++++++------------- 1 file changed, 34 insertions(+), 23 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 922dff1ce20..3dfe145894a 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1042,14 +1042,16 @@ Global Instance issymmetric_exchange {R : Ring} {n : nat} : IsSymmetric (exchange_matrix R n) := exchange_matrix_transpose. -(** The exchange matrix has order 2. This proof is only long because of arithmetic. *) -Definition exchange_matrix_square {R : Ring} {n : nat} - : matrix_mult (exchange_matrix R n) (exchange_matrix R n) = identity_matrix R n. -Proof. - apply path_matrix. - intros i j Hi Hj. +Definition entry_matrix_mult_exchange {R : Ring} {n : nat} (M : Matrix R n n) + (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) + : let Hi' := natpmswap1 _ _ _ (lt_implies_pred_geq _ _ _) + (leq_implies_pred_lt _ _ _ Hi (n_leq_add_n_k' n i)) in + entry (matrix_mult (exchange_matrix R n) M) i j + = entry M (pred n - i) j. +Proof. + cbn. assert (r : (i <= pred n)%nat) by auto with nat. - rewrite 2 entry_Build_Matrix. + lhs nrapply entry_Build_Matrix. lhs nrapply path_ab_sum. { intros k Hk. rewrite entry_Build_Matrix. @@ -1057,19 +1059,25 @@ Proof. unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => i + x)). 2: reflexivity. intros x y H; exact (isinj_nat_add_l i x y H). } - unshelve erewrite rng_sum_kronecker_delta_l'. - { unfold Core.lt. - destruct n. - 1: by apply not_lt_n_0 in Hi. - auto with nat. } - rewrite entry_Build_Matrix. - set (t := (pred n - i + j)%nat). - rewrite <- (natminuspluseq _ _ r). - unfold t; clear t. - unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat). - 2: apply kronecker_delta_symm. - intros x y H. - exact (isinj_nat_add_l _ _ _ H). + nrapply rng_sum_kronecker_delta_l'. +Defined. + +(** The exchange matrix has order 2. This proof is only long because of arithmetic. *) +Definition exchange_matrix_square {R : Ring} {n : nat} + : matrix_mult (exchange_matrix R n) (exchange_matrix R n) = identity_matrix R n. +Proof. + apply path_matrix. + intros i j Hi Hj. + lhs nrapply entry_matrix_mult_exchange. + rewrite 2 entry_Build_Matrix. + set (t := (pred n - i + j)%nat). + assert (r : (i <= pred n)%nat) by auto with nat. + rewrite <- (natminuspluseq _ _ r). + unfold t; clear t. + unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat). + 2: apply kronecker_delta_symm. + intros x y H. + exact (isinj_nat_add_l _ _ _ H). Defined. (** ** Centrosymmetric matrices *) @@ -1176,12 +1184,15 @@ Proof. lhs_V nrapply (rng_mult_assoc (A:=matrix_ring R n)); f_ap. Defined. -(** Centrosymmetric rings form a subring of the matrix ring. *) +(** Centrosymmetric matrices form a subring of the matrix ring. *) Definition centrosymmetric_matrix_ring (R : Ring@{i}) (n : nat) : Subring (matrix_ring R n). Proof. - nrapply (Build_Subring' (fun M : matrix_ring R n => IsCentrosymmetric M)); - cbn beta; exact _. + nrapply (Build_Subring' (fun M : matrix_ring R n => IsCentrosymmetric M)). + - exact _. + - intros x y ? ?; exact (iscentrosymmetric_matrix_plus x (-y)). + - exact iscentrosymmetric_matrix_mult. + - exact iscentrosymmetric_matrix_identity. Defined. Section MatrixCat. From fe99a17e1995357f141633a672740cc72ac62718 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 1 Jul 2024 15:31:53 +0200 Subject: [PATCH 3/8] Update theories/Algebra/Rings/Matrix.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/Matrix.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 3dfe145894a..4be4e86c894 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1025,7 +1025,7 @@ Definition exchange_matrix (R : Ring) n : Matrix R n n := Build_Matrix R n n (fun i j Hi Hj => kronecker_delta (R:=R) (i + j) (pred n))%nat. -(** Multiplying a matrix by the exchange matrix on the left is equivalent to exchanging the rows. Similarly multiplying on the right exchanges the columns. *) +(** Multiplying a matrix by the exchange matrix on the left reverses the order of the rows. Similarly multiplying on the right reverses the order of the columns. *) (** The exchange matrix is invariant under transpose. *) Definition exchange_matrix_transpose {R n} From c6ebcdd9b1eea0c7e46acc9fc7e257d273021059 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 3 Jul 2024 15:57:23 -0400 Subject: [PATCH 4/8] Matrix.v: minor changes --- theories/Algebra/Rings/Matrix.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 4be4e86c894..b900c545e3d 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1050,12 +1050,12 @@ Definition entry_matrix_mult_exchange {R : Ring} {n : nat} (M : Matrix R n n) = entry M (pred n - i) j. Proof. cbn. - assert (r : (i <= pred n)%nat) by auto with nat. lhs nrapply entry_Build_Matrix. lhs nrapply path_ab_sum. { intros k Hk. rewrite entry_Build_Matrix. - rewrite <- (nat_add_sub_eq _ r). + unshelve erewrite <- (nat_add_sub_eq (pred n) (k:=i) _). + 1: auto with nat. unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => i + x)). 2: reflexivity. intros x y H; exact (isinj_nat_add_l i x y H). } @@ -1070,9 +1070,10 @@ Proof. intros i j Hi Hj. lhs nrapply entry_matrix_mult_exchange. rewrite 2 entry_Build_Matrix. + (* We hide this [pred n] in [t] so that the rewrite below changes the other [pred n]. *) set (t := (pred n - i + j)%nat). - assert (r : (i <= pred n)%nat) by auto with nat. - rewrite <- (natminuspluseq _ _ r). + unshelve erewrite <- (natminuspluseq i (pred n) _). + 1: auto with nat. unfold t; clear t. unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat). 2: apply kronecker_delta_symm. From c786f026f4b8be01fbf01f88d4a1307bbb9c8fa9 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 4 Jul 2024 08:55:21 -0400 Subject: [PATCH 5/8] Matrix.v: add a local Hint to simplify proofs --- theories/Algebra/Rings/Matrix.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index b900c545e3d..fd0c46a7d7a 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1042,6 +1042,9 @@ Global Instance issymmetric_exchange {R : Ring} {n : nat} : IsSymmetric (exchange_matrix R n) := exchange_matrix_transpose. +(** This gets used in a couple of places below, so we add it to [typeclass_instances] to simplify the proofs. It says that [i < j -> i <= pred j]. *) +#[local] Hint Immediate lt_implies_pred_geq : typeclass_instances. + Definition entry_matrix_mult_exchange {R : Ring} {n : nat} (M : Matrix R n n) (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) : let Hi' := natpmswap1 _ _ _ (lt_implies_pred_geq _ _ _) @@ -1054,8 +1057,7 @@ Proof. lhs nrapply path_ab_sum. { intros k Hk. rewrite entry_Build_Matrix. - unshelve erewrite <- (nat_add_sub_eq (pred n) (k:=i) _). - 1: auto with nat. + rewrite <- (nat_add_sub_eq (pred n) (k:=i) _). unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => i + x)). 2: reflexivity. intros x y H; exact (isinj_nat_add_l i x y H). } @@ -1072,8 +1074,7 @@ Proof. rewrite 2 entry_Build_Matrix. (* We hide this [pred n] in [t] so that the rewrite below changes the other [pred n]. *) set (t := (pred n - i + j)%nat). - unshelve erewrite <- (natminuspluseq i (pred n) _). - 1: auto with nat. + rewrite <- (natminuspluseq i (pred n) _). unfold t; clear t. unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat). 2: apply kronecker_delta_symm. From 19f11c78b9b115b0c3935adeb3d6ec74543c0459 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Thu, 4 Jul 2024 10:34:02 -0400 Subject: [PATCH 6/8] Matrix: a few more simplifications of exchange matrices --- theories/Algebra/Rings/Matrix.v | 68 +++++++++++++++++++++++---------- 1 file changed, 48 insertions(+), 20 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index fd0c46a7d7a..66bba30501c 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1025,8 +1025,6 @@ Definition exchange_matrix (R : Ring) n : Matrix R n n := Build_Matrix R n n (fun i j Hi Hj => kronecker_delta (R:=R) (i + j) (pred n))%nat. -(** Multiplying a matrix by the exchange matrix on the left reverses the order of the rows. Similarly multiplying on the right reverses the order of the columns. *) - (** The exchange matrix is invariant under transpose. *) Definition exchange_matrix_transpose {R n} : matrix_transpose (exchange_matrix R n) = exchange_matrix R n. @@ -1045,24 +1043,54 @@ Global Instance issymmetric_exchange {R : Ring} {n : nat} (** This gets used in a couple of places below, so we add it to [typeclass_instances] to simplify the proofs. It says that [i < j -> i <= pred j]. *) #[local] Hint Immediate lt_implies_pred_geq : typeclass_instances. +(** An alternate way to write the exchange matrix. *) +Definition exchange_matrix_sub {R n} + (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) + : entry (exchange_matrix R n) i j = kronecker_delta (R:=R) i (pred n - j)%nat. +Proof. + lhs nrapply entry_Build_Matrix. + rhs_V nrapply (kronecker_delta_map_inj _ _ (fun m => m + j)). + 2: nrapply isinj_nat_add_r. + apply ap. + symmetry; rapply natminuspluseq. +Defined. + +(** And another way to write the exchange matrix. *) +Definition exchange_matrix_sub' {R n} + (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) + : entry (exchange_matrix R n) i j = kronecker_delta (R:=R) (pred n - i)%nat j. +Proof. + rewrite <- exchange_matrix_transpose. + lhs nrapply entry_Build_Matrix. + lhs nrapply exchange_matrix_sub. + apply kronecker_delta_symm. +Defined. + +(** A lemma that is needed to ensure that [pred n - i] is a valid matrix index. The hypothesis [i < n] is only used to force that [0 < n], and matches what we have when we use this. *) +Local Definition nat_pred_sub_lt (n i : nat) (Hi : (i < n)%nat) : (pred n - i < n)%nat. +Proof. + (* We prove this using mixed transitivity: [pred n - i <= pred n < n]. *) + apply (mixed_trans1 _ (pred n) _). + 1: apply sub_less. + by apply leq_implies_pred_lt with (i:=i). +Defined. + +#[local] Hint Immediate nat_pred_sub_lt : typeclass_instances. + +(** Multiplying a matrix by the exchange matrix on the left reverses the order of the rows. Similarly multiplying on the right reverses the order of the columns, but we don't prove this. *) Definition entry_matrix_mult_exchange {R : Ring} {n : nat} (M : Matrix R n n) (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) - : let Hi' := natpmswap1 _ _ _ (lt_implies_pred_geq _ _ _) - (leq_implies_pred_lt _ _ _ Hi (n_leq_add_n_k' n i)) in - entry (matrix_mult (exchange_matrix R n) M) i j + : entry (matrix_mult (exchange_matrix R n) M) i j = entry M (pred n - i) j. Proof. cbn. lhs nrapply entry_Build_Matrix. - lhs nrapply path_ab_sum. - { intros k Hk. - rewrite entry_Build_Matrix. - rewrite <- (nat_add_sub_eq (pred n) (k:=i) _). - unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => i + x)). - 2: reflexivity. - intros x y H; exact (isinj_nat_add_l i x y H). } - nrapply rng_sum_kronecker_delta_l'. -Defined. + lhs rapply (path_ab_sum (g:=fun k Hk => kronecker_delta (pred n - i)%nat k * entry M k j)). + 2: nrapply rng_sum_kronecker_delta_l. + intros k Hk. + apply (ap (.* _)). + apply exchange_matrix_sub'. +Defined. (** The exchange matrix has order 2. This proof is only long because of arithmetic. *) Definition exchange_matrix_square {R : Ring} {n : nat} @@ -1071,15 +1099,15 @@ Proof. apply path_matrix. intros i j Hi Hj. lhs nrapply entry_matrix_mult_exchange. - rewrite 2 entry_Build_Matrix. + lhs nrapply entry_Build_Matrix. + rhs nrapply entry_Build_Matrix. (* We hide this [pred n] in [t] so that the rewrite below changes the other [pred n]. *) - set (t := (pred n - i + j)%nat). - rewrite <- (natminuspluseq i (pred n) _). - unfold t; clear t. + set (t := (pred n - i + j)%nat); + rewrite <- (natminuspluseq i (pred n) _); + unfold t; clear t. unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat). 2: apply kronecker_delta_symm. - intros x y H. - exact (isinj_nat_add_l _ _ _ H). + nrapply isinj_nat_add_l. Defined. (** ** Centrosymmetric matrices *) From 64d2b1b725e6d5ca96d2daee1809de0ee82c3827 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 5 Jul 2024 18:22:01 +0200 Subject: [PATCH 7/8] [WIP REVERT] show difficulties with index definition Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Matrix.v | 122 ++++++++++++++++++++++++++++---- theories/Algebra/Rings/Vector.v | 8 +-- 2 files changed, 112 insertions(+), 18 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 66bba30501c..7aea26b7558 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -89,6 +89,16 @@ Proof. exact (H i j Hi Hj). Defined. +Definition path_entry_matrix {R : Type} {m n} {M M' : Matrix R m n} + (p : M = M') {i i' j j' : nat} (q : i = i') (r : j = j') + (Hi : (i < m)%nat) (Hj : (j < n)%nat) + (Hi' : (i' < m)%nat) (Hj' : (j' < n)%nat) + : entry M i j = entry M' i' j'. +Proof. + snrapply path_entry_vector; trivial. + by snrapply path_entry_vector. +Defined. + (** ** Addition and module structure *) (** Here we define the abelian group of (n x m)-matrices over a ring. This follows from the abelian group structure of the underlying vectors. We are also able to derive a left module strucutre when the entries come from a left module. *) @@ -102,6 +112,14 @@ Definition matrix_plus {A : AbGroup} {m n} Definition matrix_zero (A : AbGroup) m n : Matrix A m n := @mon_unit (abgroup_matrix A m n) _. + +Definition entry_matrix_zero {A : AbGroup} {m n} (i j : nat) + (Hi : (i < m)%nat) (Hj : (j < n)%nat) + : entry (matrix_zero A m n) i j = 0. +Proof. + unfold entry, matrix_zero. + by rewrite 2 entry_Build_Vector. +Defined. Definition matrix_negate {A : AbGroup} {m n} : Matrix A m n -> Matrix A m n @@ -1078,12 +1096,11 @@ Defined. #[local] Hint Immediate nat_pred_sub_lt : typeclass_instances. (** Multiplying a matrix by the exchange matrix on the left reverses the order of the rows. Similarly multiplying on the right reverses the order of the columns, but we don't prove this. *) -Definition entry_matrix_mult_exchange {R : Ring} {n : nat} (M : Matrix R n n) +Definition entry_matrix_mult_exchange_l {R : Ring} {n : nat} (M : Matrix R n n) (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) : entry (matrix_mult (exchange_matrix R n) M) i j = entry M (pred n - i) j. Proof. - cbn. lhs nrapply entry_Build_Matrix. lhs rapply (path_ab_sum (g:=fun k Hk => kronecker_delta (pred n - i)%nat k * entry M k j)). 2: nrapply rng_sum_kronecker_delta_l. @@ -1092,13 +1109,33 @@ Proof. apply exchange_matrix_sub'. Defined. +Definition entry_matrix_mult_exchange_r {A : Ring} {n : nat} (M : Matrix A n n) + (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) + : let Hj' := natpmswap1 _ _ _ (lt_implies_pred_geq _ _ _) + (leq_implies_pred_lt _ _ _ Hj (n_leq_add_n_k' n j)) in + entry (matrix_mult M (exchange_matrix A n)) i j + = entry M i (pred n - j). +Proof. + assert (r : (j <= pred n)%nat) by auto with nat. + lhs nrapply entry_Build_Matrix. + lhs nrapply path_ab_sum. + { intros k Hk. + rewrite entry_Build_Matrix. + rewrite <- (nat_add_sub_eq _ r). + rewrite <- nat_add_comm. + unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => j + x)). + 2: reflexivity. + intros x y H; exact (isinj_nat_add_l j x y H). } + nrapply rng_sum_kronecker_delta_r'. +Defined. + (** The exchange matrix has order 2. This proof is only long because of arithmetic. *) Definition exchange_matrix_square {R : Ring} {n : nat} : matrix_mult (exchange_matrix R n) (exchange_matrix R n) = identity_matrix R n. Proof. apply path_matrix. intros i j Hi Hj. - lhs nrapply entry_matrix_mult_exchange. + lhs nrapply entry_matrix_mult_exchange_l. lhs nrapply entry_Build_Matrix. rhs nrapply entry_Build_Matrix. (* We hide this [pred n] in [t] so that the rewrite below changes the other [pred n]. *) @@ -1112,26 +1149,75 @@ Defined. (** ** Centrosymmetric matrices *) -(** A centrosymmetric matrix is symmetric about its center. *) -Class IsCentrosymmetric {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Type@{i} - := exchange_matrix_iscentrosymmetric - : matrix_mult (exchange_matrix R n) M = matrix_mult M (exchange_matrix R n). +(** A centrosymmetric matrix is symmetric about its center. We propositionally truncate this statement as to avoid funext. *) +Class IsCentrosymmetric {A : Type@{i}} {n : nat} (M : Matrix@{i} A n n) : Type@{i} + := iscentrosymmetric + : merely ( + forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat), + entry M i j = entry M (pred n - i) (pred n - j)). -Global Instance ishprop_iscentrosymmetric {R : Ring@{i}} {n : nat} (M : Matrix R n n) +(** The characterizing property of centrosymmetric matrices is that they commute with the exchange matrix. *) +Definition exchange_matrix_iscentrosymmetric {R : Ring@{i}} {n : nat} + (M : Matrix@{i} R n n) `{!IsCentrosymmetric M} + (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) + : matrix_mult (exchange_matrix R n) M = matrix_mult M (exchange_matrix R n). +Proof. + apply path_matrix. + intros k l Hk Hl. + lhs nrapply entry_matrix_mult_exchange_l. + rhs nrapply entry_matrix_mult_exchange_r. + pose proof (p := iscentrosymmetric). + strip_truncations. + lhs nrapply p. + apply path_entry_matrix; trivial. + apply ineq_sub. + eauto with nat. +Defined. + +Global Instance ishprop_iscentrosymmetric {A : Type@{i}} {n : nat} + (M : Matrix A n n) : IsHProp (IsCentrosymmetric M). Proof. unfold IsCentrosymmetric; exact _. Defined. (** The zero matrix is centrosymmetric. *) -Global Instance iscentrosymmetric_matrix_zero {R : Ring@{i}} {n : nat} - : IsCentrosymmetric (matrix_zero R n n) - := rng_mult_zero_r (A:=matrix_ring R n) _ @ (rng_mult_zero_l _)^. +Global Instance iscentrosymmetric_matrix_zero {A : AbGroup@{i}} {n : nat} + : IsCentrosymmetric (matrix_zero A n n). +Proof. + apply tr; intros i j Hi Hj. + lhs nrapply entry_matrix_zero. + by rhs nrapply entry_matrix_zero. +Defined. +Local Open Scope nat_scope. +Definition isinj_nat_sub_leq@{}(n x y : nat) + : x <= n -> y <= n -> n - x = n - y + -> x = y. +Proof. + intros H1 H2 p. + rewrite <- (ineq_sub _ _ H1) in H1 |- *. + rewrite <- (ineq_sub _ _ H2) in H2 |- *. + set (x' := (n - x)%nat) in *. + set (y' := (n - y)%nat) in *. + clearbody x' y'; clear x y. + by destruct p. +Defined. +Local Close Scope nat_scope. + (** The identity matrix is centrosymmetric. *) Global Instance iscentrosymmetric_matrix_identity {R : Ring@{i}} {n : nat} - : IsCentrosymmetric (identity_matrix R n) - := rng_mult_one_r (A:=matrix_ring R n) _ @ (rng_mult_one_l _)^. + : IsCentrosymmetric (identity_matrix R n). +Proof. + apply tr; intros i j Hi Hj. + lhs nrapply entry_Build_Matrix. + rhs nrapply entry_Build_Matrix. + symmetry. + nrapply (kronecker_delta_map_inj _ _ (fun m => pred n - m)%nat). + intros x y p. + nrapply (isinj_nat_sub_leq (pred n) _ _ _ _ p). + (* Doesn't work because injectivity needed here is more general.... *) +Admitted. (** The sum of two centrosymmetric matrices is centrosymmetric. *) Global Instance iscentrosymmetric_matrix_plus {R : Ring@{i}} {n : nat} @@ -1143,7 +1229,7 @@ Proof. rhs nrapply (rng_dist_r (A:=matrix_ring R n)). cbn; by rewrite H1, H2. Defined. - +(* (** The negation of a centrosymmetric matrix is centrosymmetric. *) Global Instance iscentrosymmetric_matrix_negate {R : Ring@{i}} {n : nat} (M : Matrix R n n) {H : IsCentrosymmetric M} @@ -1192,6 +1278,14 @@ Global Instance iscentrosymmetric_matrix_transpose {R : Ring@{i}} {n : nat} (M : Matrix R n n) {H : IsCentrosymmetric M} : IsCentrosymmetric (matrix_transpose M). Proof. + hnf. + apply path_matrix. + intros i j Hi Hj. + lhs nrapply entry_matrix_mult_exchange_l. + rhs nrapply entry_matrix_mult_exchange_r. + rewrite 2 entry_Build_Matrix. + + unfold IsCentrosymmetric. rewrite <- exchange_matrix_transpose. lhs_V nrapply (matrix_transpose_mult (R:=rng_op R) M (exchange_matrix R n)). diff --git a/theories/Algebra/Rings/Vector.v b/theories/Algebra/Rings/Vector.v index f391540eb39..be7978cf98b 100644 --- a/theories/Algebra/Rings/Vector.v +++ b/theories/Algebra/Rings/Vector.v @@ -66,11 +66,11 @@ Proof. 1, 2: apply nth'_nth'. Defined. -Definition path_entry_vector {A : Type} {n : nat} (v : Vector A n) - (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) (p : i = j) - : entry v i = entry v j. +Definition path_entry_vector {A : Type} {n : nat} {v v' : Vector A n} (p : v = v') + {i j : nat} {Hi : (i < n)%nat} {Hj : (j < n)%nat} (q : i = j) + : entry v i = entry v' j. Proof. - destruct p. + destruct p, q. apply nth'_nth'. Defined. From 2349783e41c62ea0babe34324ba6a72d32bdf594 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Fri, 12 Jul 2024 15:43:50 -0400 Subject: [PATCH 8/8] Matrix: progress with index version of IsCentroSymmetric --- theories/Algebra/Rings/Matrix.v | 62 +++++++++++---------------------- 1 file changed, 20 insertions(+), 42 deletions(-) diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v index 7aea26b7558..d4e6aa705ac 100644 --- a/theories/Algebra/Rings/Matrix.v +++ b/theories/Algebra/Rings/Matrix.v @@ -1109,6 +1109,7 @@ Proof. apply exchange_matrix_sub'. Defined. +(* TODO: if we keep this, clean it up like the _l version. *) Definition entry_matrix_mult_exchange_r {A : Ring} {n : nat} (M : Matrix A n n) (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) : let Hj' := natpmswap1 _ _ _ (lt_implies_pred_geq _ _ _) @@ -1149,7 +1150,7 @@ Defined. (** ** Centrosymmetric matrices *) -(** A centrosymmetric matrix is symmetric about its center. We propositionally truncate this statement as to avoid funext. *) +(** A centrosymmetric matrix is symmetric about its center. We propositionally truncate this statement to avoid funext. *) Class IsCentrosymmetric {A : Type@{i}} {n : nat} (M : Matrix@{i} A n n) : Type@{i} := iscentrosymmetric : merely ( @@ -1225,20 +1226,22 @@ Global Instance iscentrosymmetric_matrix_plus {R : Ring@{i}} {n : nat} : IsCentrosymmetric (matrix_plus M N). Proof. unfold IsCentrosymmetric. - lhs nrapply (rng_dist_l (A:=matrix_ring R n)). - rhs nrapply (rng_dist_r (A:=matrix_ring R n)). - cbn; by rewrite H1, H2. + strip_truncations; apply tr; intros i j Hi Hj. + rewrite 2 entry_Build_Matrix. + apply ap011. + - apply H1. + - apply H2. Defined. -(* + (** The negation of a centrosymmetric matrix is centrosymmetric. *) Global Instance iscentrosymmetric_matrix_negate {R : Ring@{i}} {n : nat} (M : Matrix R n n) {H : IsCentrosymmetric M} : IsCentrosymmetric (matrix_negate M). Proof. unfold IsCentrosymmetric. - lhs nrapply (rng_mult_negate_r (A:=matrix_ring R n) _). - rhs nrapply (rng_mult_negate_l (A:=matrix_ring R n) _). - f_ap. + strip_truncations; apply tr; intros i j Hi Hj. + rewrite 2 entry_Build_Matrix. + apply ap, H. Defined. (** A scalar multiple of a centrosymmetric matrix is centrosymmetric. *) @@ -1247,30 +1250,17 @@ Global Instance iscentrosymmetric_matrix_scale {R : Ring@{i}} {n : nat} : IsCentrosymmetric (matrix_lact r M). Proof. unfold IsCentrosymmetric. - (** TODO: Need associative algebra structure. *) -Abort. + strip_truncations; apply tr; intros i j Hi Hj. + rewrite 2 entry_Build_Matrix. + apply ap, H. +Defined. (** A centrosymmetric matrix is also centrosymmetric when considered over the opposite ring. *) Global Instance iscentrosymmetric_rng_op {R : Ring@{i}} {n : nat} (M : Matrix R n n) `{!IsCentrosymmetric M} - : IsCentrosymmetric (R := rng_op R) M. + : IsCentrosymmetric (A := rng_op R) M. Proof. - hnf. - apply path_matrix. - intros i j Hi Hj. - rewrite 2 entry_Build_Matrix. - pose (p := exchange_matrix_iscentrosymmetric). - apply (ap (fun x => entry x i j)) in p. - rewrite 2 entry_Build_Matrix in p. - refine (_ @ p @ _). - - apply path_ab_sum. - intros k Hk. - rewrite 2 entry_Build_Matrix. - rapply kronecker_delta_comm. - - apply path_ab_sum. - intros k Hk. - rewrite 2 entry_Build_Matrix. - rapply kronecker_delta_comm. + assumption. Defined. (** The transpose of a centrosymmetric matrix is centrosymmetric. *) @@ -1278,22 +1268,10 @@ Global Instance iscentrosymmetric_matrix_transpose {R : Ring@{i}} {n : nat} (M : Matrix R n n) {H : IsCentrosymmetric M} : IsCentrosymmetric (matrix_transpose M). Proof. - hnf. - apply path_matrix. - intros i j Hi Hj. - lhs nrapply entry_matrix_mult_exchange_l. - rhs nrapply entry_matrix_mult_exchange_r. - rewrite 2 entry_Build_Matrix. - - unfold IsCentrosymmetric. - rewrite <- exchange_matrix_transpose. - lhs_V nrapply (matrix_transpose_mult (R:=rng_op R) M (exchange_matrix R n)). - rhs_V nrapply (matrix_transpose_mult (R:=rng_op R) (exchange_matrix R n) M). - pose (iscentrosymmetric_rng_op M). - f_ap. - symmetry. - rapply (exchange_matrix_iscentrosymmetric (R:=rng_op R)). + strip_truncations; apply tr; intros i j Hi Hj. + rewrite 2 entry_Build_Matrix. + apply H. Defined. (** The product of two centrosymmetric matrices is centrosymmetric. *)