I have a goal mentioning some concrete definitions that were used to define an instance of a class, and would like to use lemmas referring to corresponding fields of the class. Is there any way to set things up so unification can succeed? The failed unification message looks something like
let (_, ... , foo , ...) := ?inst in foo), which reminds me of canonical projections. Can a typeclass field be declared a canonical projection?
never seen that in the wild. If I saw that, I’d fix the goal, and possibly stop
my_foo_impl from having a name.
I'm using the implementation function on purpose, because the class takes some extra parameters that are not used by that field, and not known or needed at the point where I'm using it.
Maybe our classes need to be split up, but it's not like an accident or some early reduction that's exposing the specific function used to implement that instance. It's the other way around - because the instance that includes the specific
my_foo_impl that I mentioned takes extra parameters that are not mentioned in the field, those parameters have to be supplied to manually fold it to a use of the class method.
fair enough! In that case, I suspect I’d pass enough type arguments that
?inst can be inferred.
If you really want to try canonical structures ... I might be pessimistic but I’d expect an exciting amount of bugs due to untested feature interactions.
One way to even try it is probably to turn the class into a canonical structure and use
Existing Class to make it a class as well.
if canonical structures with parameters trigger problems, the params can be bound in the surrounding section (I think I’ve seen this part in Iris).
for best unification results, probably you want to use ssreflect tactics, since their unification algorithm (evarconv, used e.g. by
apply:) works better with canonical structures AFAICT than tactic unification (used e.g. by
Last updated: Jan 27 2023 at 00:03 UTC