The Coq mailing list

[Jerome Hugues <jhugues AT andrew.cmu.edu>]

Hi Jean-Christophe

Thanks for the pointers. I had read them already. Unfortunately this does not provide a definite solution (or I did not quite grasp the full idea behind those posts, which is also likely). I still end up with terms like

 

= False /\

       ([] = [] /\

        (Feature (Ident "a_feature") inF eventPort

           (Component (Ident "") null (Ident "") [] [] [] []) [] =

         Feature (Ident "a_feature") inF eventPort

           (Component (Ident "") null (Ident "") [] [] [] []) [] \/ False) \/

        False)

     : Prop

 

And I believe an evaluation strategy would reduce those basic terms to either True or False without intervention. But I fail to establish one. It works in some cases, but not on other and I am trying to understand the pattern behind those.

 

Generally speaking, all my definitions are based on equality of some inductive types based on nat or lists of other inductive types. So the use case is rather narrow.

 

Thanks,

 

From: <coq-club-request AT inria.fr> on behalf of Jean-Christophe Léchenet <jean-christophe.lechenet AT inria.fr>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, April 21, 2021 at 4:26 AM
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Qed opacity and Coq standard library

 

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