Was wondering where I would be able to find information or the implementation of how the rewrite tactic works when rewriting under setoid equivalences specifically. I imagine all if not most of the work is done in justifying the relation is proper with respect to the context, but what does this fully entail and where can I find the source?

For example, in one instance defining integers as pairs of naturals with the equivalence relation (x, y) ∼ (u, v) if and only if x + v = y + u, when rewriting (x, y) with (S x, S y), the corresponding proof term has functions called like trans_sym_co_inv_impl_morphism, which I assume has to do with justifying that the relation is an equivalence relation. I want to know where I may be able to find documentation for such functions invoked by the proof terms and what they do, and what the underlying logic is for rewrite in what ends up being called in the corresponding proof terms (when dealing with setoids specifically).

Furthermore, are there any customizations already enabled for rewrite in order to optimize it when certain properties (such as transitivity and symmetry) are already justified to prevent needing calls to separate functions which do that (in the event that is what's happening here)?

https://coq.inria.fr/doc/master/refman/addendum/generalized-rewriting.html

it builds the Proper proofs by using typeclass search

Last updated: Oct 13 2024 at 01:02 UTC