-
Notifications
You must be signed in to change notification settings - Fork 193
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Adapt ring
tactic to HoTT
#2093
Comments
It is not, mathclasses uses the Coq stdlib ring tactic. |
Ok great, then the most sensible thing to do would be to investigate how to get it to interact nicely with the Algebra library. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 thering
tactic in a custom way, here is their code: https://github.com/math-comp/algebra-tactics/blob/master/theories/common.vOriginally posted by @Alizter in #2089 (comment)
The text was updated successfully, but these errors were encountered: