Stream: Coq users

Topic: Typeclasses


view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 02:55):

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?

view this post on Zulip MackieLoeffel (Oct 19 2022 at 03:31):

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.

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 03:43):

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.'

view this post on Zulip MackieLoeffel (Oct 19 2022 at 03:47):

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.

view this post on Zulip Paolo Giarrusso (Oct 19 2022 at 17:15):

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