coqrewriting

Print existing setoids and morphisms in Coq


I am using the generalized rewriting features of Coq.

I would like to print the setoids and morphisms currently available to setoid_rewrite, to understand better which relation or function is missing when rewriting fails. Is there any way to do that?


Solution

  • Perhaps Print Instances ... can help.

    Require Import Setoid.
    Print Instances Equivalence.
    Print Instances Morphisms.Proper.
    

    From the man page link you provided.

    27.2.3 Printing relations and morphisms

    The Print Instances command can be used to show the list of currently registered Reflexive (using Print Instances Reflexive), Symmetric or Transitive relations, Equivalences, PreOrders, PERs, and Morphisms (implemented as Proper instances). When the rewriting tactics refuse to replace a term in a context because the latter is not a composition of morphisms, the Print Instances commands can be useful to understand what additional morphisms should be registered.