Jake Zweifler (Aug 31 2021 at 19:53): Jake Zweifler (Aug 31 2021 at 19:53):I am working on a project that uses Ccorn's complex numbers and I am having trouble finding lemmas\tactics. For example, I need to rewrite associativity, commutativity, etc... I also need a tactic for numerical like showing that 1*2 + 2 = 4, 1 <> 0, etc... I also need the same kinds of lemmas for polynomials. I have read much of the code, but can't seem to find what I am looking for. Any help is greatly appreciated.
Bas Spitters (Aug 31 2021 at 19:59):Hi Jake, can you say a bit more about the project you are working on?
Corn has both a ring and a field tactic, which should help in some of the problems you are working on.
@Vincent Semeria has been very active with corn recently. So he may also be able to give some pointers.
Jake Zweifler (Aug 31 2021 at 22:07):@Bas Spitters I am using my own set of complex numbers (denoted C) that is a pair (R * R) of coq_reals. I then use the type (nat -> nat -> C) to represent a matrix, sending the two indices to a complex number. For this reason, simply calling ring and field won't work since I may need to also use some of my own matrix rewrites. The main reason I need corn is that I need to use the fundamental theorem of algebra to show that every matrix has an eigenvector. My proof involves an annoying induction argument and I need to know that (f ! x) + (g ! x) = (f + g) ! x, etc... and also that these are true after translating to my complex numbers. To show the second part, it more than suffices to show that my complex numbers are 'isomorphic' to corn's complex numbers. I don't think this would be too difficult since I can mirror the way that corn shows coq_reals are isomorphic to corn reals. However, I don't really know the specifics of actually how to do this, and I also don't know how to then use this.
Another possibility is to use corns complex numbers for the entire project. Then, I will probably need to just know many of the necessary lemmas. Since this is still pretty vague, I can perhaps try to give examples if it would help. Thank you so much!
Bas Spitters (Sep 06 2021 at 15:05):@Jake Zweifler yes, I would go for the first route. You've already found the isomorphism for the reals. Based on that, it should not be too difficult, I expect.
Last updated: Apr 19 2024 at 15:02 UTC