The Coq mailing list

[Jean-Christophe Léchenet <jean-christophe.lechenet AT inria.fr>]

Hi Jerome,

Two blog posts that are relevant to this topic :
- http://gallium.inria.fr/blog/coq-eval/
- https://gmalecha.github.io/reflections/2017/qed-considered-harmful

Not sure if that will help in your case, though.

Best,

Jean-Christophe

Le 20/04/2021 à 15:48, Jerome Hugues a écrit :

Hi,

 

At some point in my project, I use Defined rather than Qed to have transparent proofs and use the Compute mechanisms to evaluate some statements. This works nicely for my own theorems, but I am stuck when this involves theorems provided by the Coq standard library, NoDup_dec in my case, but ultimately this might extend to more situations.

 

One quick and dirty work-around is to copy/paste the code, change Qed into Defined and voila! But this is not satisfactory.

 

I could find some blog posts like this one https://plv.csail.mit.edu/blog/computing-with-opaque-proofs.html by Clément Pit-Claudel on this topic, but again it seems this imposes some rework.

 

I understand Qed and Defined are different for a reason, I am just curious whether there is a systematic way to change Qed into Defined on a case by case basis, or if we are forced to this type of modifications.

 

Is there some suggested readings on this topic?

 

Thanks