The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi Maxime,

I often end up with functions that don't compute because they use opaque definitions/lemmas (saved using Qed) at critical places, e.g. discriminees of match, guards of fixpoints.

Also, I vaguely remember instances when Coq's productivity check rejected my proofs because of the opacity of some subcomponents.

I am not the only one with such misfortune of not being able to use (e.g. for proof by computation) what has been paid for (by constructive proofs):

https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00033.html

https://sympa.inria.fr/sympa/arc/coq-club/2015-02/msg00075.html

https://sympa.inria.fr/sympa/arc/coq-club/2015-11/msg00173.html

On this list, there have been many discussions about workarounds for specific cases, particularly when the opaque lemmas/definitions are about decidable properties:

https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00081.html

Even in those cases, some manual work is needed : one needs to identify the critical opaque parts and redefine them.

I want something that effortlessly always restores canonicity.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Nov 15, 2016 at 12:09 PM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Abishek,

Can you share a bit of context about your use case?

Thanks!

Maxime.

On 11/15/16 18:03, Abhishek Anand wrote:
> My understanding is that once a definition is saved with Qed, there is
> no way to make it transparent.
> Is that true?
>
> If so, has someone written a plugin/tool to take a definition (say of X)
> with possibly opaque parts and recursively transparently duplicate those
> parts to create a new totally transparent definition (say X_t)?
>
> Perhaps no new Coq plugin is needed -- template-coq
> <https://github.com/gmalecha/template-coq>'s `Quote Recursively` already
> reifies opaque bodies. Also, it has "Make Definition" to reflect back
> encodings of definitions. It seems possible to write Ltac/Gallina
> functions that use template-coq commands to achieve the above-mentioned
> transparentification. Am I overlooking some difficulty?
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/~aa755/>