search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

centrosymmetric matrices #2003

Open Alizter opened 5 days ago

Alizter commented 5 days ago

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.

Alizter commented 2 days ago

@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 pred n - i <= n automatically hasn't been easy. I've tried to use lets to do this, but it complicated the proofs later on. I think I would prefer to keep it this way for now. Have you got any other suggestions for improvement?

Alizter commented 9 hours ago

@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.

Alizter commented 5 hours ago

@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.