The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Tue, Apr 20, 2021 at 3:54 PM Jerome Hugues <jhugues AT andrew.cmu.edu> wrote:

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.

My rule of thumb is that every definition that is in Prop should be Qed and every definition that is in Type should be Defined.  Most of the time, there's enough of a phase distinction for this heuristic to work well.  See http://gallium.inria.fr/blog/coq-eval/ for more examples, including one that used to violate the phase distinction but was fixed since.

In this respect, NoDup_dec in the Coq standard library is a bug, and so is incl_decl in the same file, while In_dec correctly uses Defined.  Why don't you file a bug report at https://github.com/coq/coq/issues ?

Regards,

- Xavier Leroy

 

 

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