Jake Zweifler (Mar 08 2022 at 19:26): Jake Zweifler (Mar 08 2022 at 19:26):I am currently working on a project that uses many different types of addition. In an attempt to simplify things, I have added typeclasses for many of the basic algebraic structures (monoid, group, ring, etc...). I then want to prove many of the basic lemmas involving these structures. Instead of rewriting a bunch of times using the axioms of the structures, it would be much easier to use Coq's ring and field tactics which already exist. Since all the axioms of my type classes are the expected rules, it is quite easy to show that an arbitrary `{Field F} is a field in terms of Coq's notion of field. However, I am unsure of how to tell Coq that this is the case, since usually we just show that a specific type is a field, rather than a type class.
The code where this occurs is located at https://github.com/inQWIRE/QuantumLib/blob/main/Summation.v
You can see that I show compatibility with Coq's ring and field tactics in lines 78-99 and that I have commented out my attempt at adding this as a field in line 102. Finally, I would theoretically like to call the 'field' tactic in line 176 to solve a simple equation that basically only required a bunch of commutativity rewrites.
Any help will be greatly appreciated!
Gaëtan Gilbert (Mar 08 2022 at 21:42):best you can do is Add Ring / Add Field in a section AFAIK
Gaëtan Gilbert (Mar 08 2022 at 21:43): Kazuhiko Sakaguchi (Mar 09 2022 at 04:45):Proving Equalities in a Commutative Ring Done Right in Coq explains how the ring tactic is implemented. As in Section 6.1, you have to construct a syntax tree from a ring expression and apply the correctness lemma.
My recent preprint explains how to make this kind of reflexive tactics cooperate with an overloading/inheritance mechanism for algebraic structures, although it is based on canonical structures rather than type classes. Since your type classes bundle operators, I think some of the discussions in the paper apply to your case. If you are fine with switching to MathComp, Algebra Tactics do this for you.
Last updated: Oct 04 2023 at 23:01 UTC