Stream: Coq users

Topic: Typeclass and side condition


view this post on Zulip Laurent Théry (Oct 20 2021 at 13:26):

I have an instance of a typeclass C where one instance looks like S -> C x f1 -> C y f2 -> C (x * y) f3 (here S is a side-condition, typically x <> 0). Even if S is one of the assumption of my goal, the instance fails to be applied by resolution. What is the standard way to deal with this kind of situation?

view this post on Zulip Enrico Tassi (Oct 20 2021 at 13:34):

I don't know if it is usual, but you could declare the instance using the Hint Extern machinery on the TC instance database, apply you instance by hand (with apply) and call, say, assumption on the first goal.

view this post on Zulip Laurent Théry (Oct 20 2021 at 13:36):

thanks, is there an example somewhere of this kind of use of Hint Extern

view this post on Zulip Enrico Tassi (Oct 20 2021 at 13:44):

random grep:

Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 01:21):

I think assumptions were always used, even for non-typeclasses, so this might be a different bug, such as simple apply being too weak?

view this post on Zulip Enrico Tassi (Oct 21 2021 at 07:02):

maybe the context item is not syntactically identical to the goal (typical situation in mathcompland)

view this post on Zulip Laurent Théry (Oct 21 2021 at 07:52):

Enrico may be right, when tracing the resolution I see the step of my side condition but at the end it says failed.

view this post on Zulip Enrico Tassi (Oct 21 2021 at 09:18):

did you manage to call assumption in the hint extern?


Last updated: Jan 29 2023 at 05:03 UTC