The Typeclasses page in the coq docs says
By default, all constants and local variables are considered transparent.
I am wondering how, in the context of a proof, I can hide the value of certain variables from typeclass resolution and force the algorithm to treat them as opaque.
Also the command Typeclasses Filtered Unification
is deprecated as of 8.16, is there any suggested workaround to achieve the same functionality?
You can use Typeclasses Opaque X.
to make X
opaque for typeclass resolution and Typeclasses Transparent X
to make X
transparent again. Alternatively, you can use typeclass search (typeclasses eauto
) with a custom hint database. See https://gitlab.mpi-sws.org/iris/coq-tricks/-/blob/main/theories/custom_typeclass_db.v for an explanation of the technique.
My question is about local definitions in proof mode. something like
set ( j:= x * y)
Is there a way to avoid unfolding j?
That command isn't working for me, it says 'j
not found in the current environment.'
If you use the second technique, Global Hint Variables Opaque
should do what you want, see https://gitlab.mpi-sws.org/iris/coq-tricks/-/blob/main/theories/custom_typeclass_db.v#L80 . I am not sure if it is possible to control this in a more fine grained way.
for the local context there are also locking tactics — already using remember
will produce a propositional equality — e.g. Hfoo : j = x * y
— which TC search won't unfold, and the resulting prop. equality Hfoo
can then be wrapped
Last updated: Oct 13 2024 at 01:02 UTC