I have read the documenation on rewriting in Coq and I have used the generalize rewriting with typeclass resolution. I have not used rewrite_strat but I think I get the idea there. I am wondering like, is there any tooling available to Coq users to help them generate rewrite rules for an equational theory based on Knuth-Bendix completion or something similar? A lot of the problems that come up in category theory are really easy equational reasoning problems and it should be easy to write a rewriting system but the problem is that the context is always changing, you need to set up new rewrite systems quickly. So I'm wondering what kind of tooling is available to help the user get up and running with a set of equational rewrite rules to solve their particular problem.

BTW the more general question here is that I want to prove a bunch of stuff about fibrations of bicategories and this is really easy stuff except that because it's category theory everything is dependently typed.

ironically, Huet proved Knuth-Bendix correct before he and Coquand developed Coq: https://core.ac.uk/download/pdf/82290465.pdf

Probably, there are formalizations of Knuth-Bendix in Coq floating around that one could use, e.g., via MetaCoq

Last updated: Jun 23 2024 at 05:02 UTC