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!

best you can do is Add Ring / Add Field in a section AFAIK

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: Jun 24 2024 at 12:02 UTC