centrosymmetric matrices #2003
centrosymmetric matrices #2003
Conversation
Alizter
force-pushed
the
ps/rr/centrosymmetric_matrices
branch
from
fe208ee
to
c57fa3c
Compare
Signed-off-by: Ali Caglayan <[email protected]>
Alizter
force-pushed
the
ps/rr/centrosymmetric_matrices
branch
from
c57fa3c
to
e1feb0b
Compare
theories/Algebra/Rings/Matrix.v
Outdated
| Definition exchange_matrix_square {R : Ring} {n : nat} | ||
| : matrix_mult (exchange_matrix R n) (exchange_matrix R n) = identity_matrix R n. |
There was a problem hiding this comment.
This also follows from the claim above that (exchange_matrix R n) * M reverses the order of the rows of M. I wonder if this claim is a bit easier to prove?
There was a problem hiding this comment.
I've factored out that part of the proof, but it is still a little tricky. I might be missing something but I'll have to take another look when I have more time.
theories/Algebra/Rings/Matrix.v
Outdated
| Global Instance iscentrosymmetric_rng_op {R : Ring@{i}} {n : nat} (M : Matrix R n n) | ||
| `{!IsCentrosymmetric M} | ||
| : IsCentrosymmetric (R := rng_op R) M. |
There was a problem hiding this comment.
This is trivial if you know that being centrosymmetric is equivalent to the (i,j) entry being equal to the (n-1-i, n-1-j) entry, since this condition doesn't involve the ring structure at all. And if the claim about how the exchange matrix multiple other matrices is proven, this characterization would be easy. Just a thought.
There was a problem hiding this comment.
This may work out, however I found it quite awkward to write the condition as we need Coq to infer that n - 1 - i < n and I couldn't find a way to do this easily.
There was a problem hiding this comment.
It doesn't work to define a (possibly Local) instance stating this inequality?
There was a problem hiding this comment.
Or maybe it helps to write it as n - (i.+1) < n?
There was a problem hiding this comment.
I made a couple of minor changes. If i <= pred n can be inferred from i < n with some kind of hint, then with the new style we should be able to simply remove the auto with nat lines. (I also added a comment explaining the set t, which confused me at first.)
There was a problem hiding this comment.
I figured out how to add hints for i <= pred n and pred n - i < n, which makes some things smoother. I also factored out a different characterization of the entries of the exchange matrix. Maybe with these ideas you can further simplify a few things, e.g. giving the equivalent characterization of centrosymmetric matrices?
| Global Instance iscentrosymmetric_matrix_transpose {R : Ring@{i}} {n : nat} | ||
| (M : Matrix R n n) {H : IsCentrosymmetric M} | ||
| : IsCentrosymmetric (matrix_transpose M). |
There was a problem hiding this comment.
This might also be easier with the equivalent characterization?
Signed-off-by: Ali Caglayan <[email protected]>
Co-authored-by: Dan Christensen <[email protected]>
|
@jdchristensen I've tried to make progress on this but haven't been able to. I tried to characterize centrosymmetric matrices using the equivalent definition however getting Coq to find |
|
@jdchristensen Thanks a lot for the improvements. I would like to spend some more time thinking about this and see if I can improve things further. I will have another go at defining centrosymmetric matrices using the alternative characterisation. |
Signed-off-by: Ali Caglayan <[email protected]>
|
@jdchristensen I got further than before but I run into issues with showing the identity matrix is centrosymmetric. Overall it seems the index approach might be more general, but it greatly complicates even basic things like this. Would you like to have a look at the WIP commit to see the difficulty I am running into. |
|
I'm busy for a few days, but I'll try to take a look at this when I'm free. |
|
Alright, no rush. This is a relatively low priority PR anyway and should be the last of my matrix backlog. I'm going to be focusing on abelian groups and modules some more. |
I tried a few more things in the file, and many got easier (including some that were much easier). (See my last commit.) So I definitely think we want to have the index version around.
I don't think that particular goal looks that tricky. But I'm also ok with using the exchange matrix approach when it is more convenient, as in cases like this. So I suggest one of two approaches:
|
|
I'm converting this to a draft for now as we can come back to it when we have the time. |
In this PR we define centrosymmetric matrices which are matrices which are symmetric about their center. Unlike symmetric and skew-symmetric matrices, these form a subring of the ring of matrices.