Laurent Théry (Oct 20 2021 at 13:26): 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?
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.
Laurent Théry (Oct 20 2021 at 13:36):thanks, is there an example somewhere of this kind of use of Hint Extern
Enrico Tassi (Oct 20 2021 at 13:44):random grep:
Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
I think assumptions were always used, even for non-typeclasses, so this might be a different bug, such as simple apply being too weak?
Enrico Tassi (Oct 21 2021 at 07:02):maybe the context item is not syntactically identical to the goal (typical situation in mathcompland)
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.
Enrico Tassi (Oct 21 2021 at 09:18):did you manage to call assumption in the hint extern?
Last updated: Oct 03 2023 at 02:34 UTC