Stream: Coq users

Topic: ✔ Tips on debugging rewriting with custom relations?


view this post on Zulip Yao Li (Oct 12 2021 at 19:55):

I wonder if anyone has any tips on debugging a rewriting does not work with my custom equivalence relation? I have proved the required Proper instance and the instance is in the hint database. When I rewrite Coq says no matching subterms; but an apply would work in the same situation.
Sorry that my question is vague and I don't have a minimal example at the moment. I need to figure out where the problem could be to cut my example to a smaller size...

view this post on Zulip Paolo Giarrusso (Oct 12 2021 at 20:05):

unless you’re trying to rewrite f in f a, I fear the starting point is Set Typeclasses Debug. You could also post a non-minimized example and/or a link to sources, in case somebody can spot something off

view this post on Zulip Yao Li (Oct 12 2021 at 20:48):

Thanks @Paolo Giarrusso! After spending some time eposeing and deciphering the debug info from Set Typeclasses Debug, I find that there is one other relation that I forgot to prove it's an instance of Equivalence. This combined with some issues with implicit arguments led to the issue I had.

view this post on Zulip Notification Bot (Oct 12 2021 at 21:32):

Yao Li has marked this topic as resolved.


Last updated: Jan 29 2023 at 06:02 UTC