The Coq mailing list

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

Hi

 

Thanks for the links,

 

I created issue https://github.com/coq/coq/issues/14149 about NoDup_dec being Qed instead of Defined.

 

About my own problem, I finally found a work-around that puzzles me as a Coq novice: I need to check that a list is empty as part of some more complex verifications on my data structures, nothing fancy but …

 

this definition allows me to do nice evaluation using Compute, you will note it matches an equivalent bool version. It is not that elegant but works

 

  Definition Is_Empty (q : queue) : Prop :=

   match q with

    | nil => True

    | _ => False

    end.

 

The more direct

 

                Definition Is_Empty (q : queue) : Prop := q = empty.  

 

where empty is defined as nil, returns an _expression_ of 400+ lines. Coding style definitely matters to help the evaluation process I presume, a topic for further readings on my end.

 

Regards,

 

 

From: <coq-club-request AT inria.fr> on behalf of Xavier Leroy <xavier.leroy AT college-de-france.fr>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, April 21, 2021 at 1:14 PM
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Qed opacity and Coq standard library

 

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