search

HoTT / Coq-HoTT

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

Adapt `ring` tactic to HoTT #2093

Open Alizter opened 3 days ago

Alizter commented 3 days ago 
          > As an aside, it would be great to have some "reflection" tools in Coq-HoTT that let us quickly solve all of these goals involving group and ring laws. I heard that the Cubical Agda library has recently added such things, and of course there's lots of work of this nature done in Coq. I wonder if any of it can be easily imported into Coq-HoTT?

We have some ring reflection tactics already in the library. Though it is from mathclasses so I don't know how easy it would be to get working with the main algebra library. Coq also has its own ring tactics that can solve polynomial expressions in semirings. I don't know if it relies on the stdlib in anyway, but it would be interesting to see if we can adapt its usage here. I'll create an issue.

The key detail with adapting the ring tacitcs is to produce a normalization/reification procedure for semiring expressions together with proofs of correctness. mathcomp also adapts the ring tactic in a custom way, here is their code: https://github.com/math-comp/algebra-tactics/blob/master/theories/common.v

Originally posted by @Alizter in https://github.com/HoTT/Coq-HoTT/issues/2089#issuecomment-2363644360

SkySkimmer commented 3 days ago

Though it is from mathclasses

It is not, mathclasses uses the Coq stdlib ring tactic. https://github.com/HoTT/Coq-HoTT/blob/master/theories/Classes/tactics/ring_tac.v is a custom job for hott

Alizter commented 3 days ago

Ok great, then the most sensible thing to do would be to investigate how to get it to interact nicely with the Algebra library.