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 05 2023 at 02:01 UTC