The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/17/2016 05:39 AM, Enrico Tassi wrote:
> ...
> I think there are two "kind" of definitions in Coq.
> Definitions like "I define plus on nat" and definitions like in HoTT,
> ie "proofs I will later reason about".  For the first kind of definition,
> I think your request makes little sense, since one proves stuff on plus
> immediately after it is defined.  For the latter use case, I
> think the way to go is provide a Command to make these proofs
> transparent later on.  I mean, you use Qed and when you really need to
> open the proof you make it explicit in the document.  This makes things
> quite simpler, since synchronization points become statically
> detectable.
>
> Would that work for your?  Is your use case different?

I already use Qed for almost everything.  However, Pierre Letouzey once 
raised the objection to my usage of Extraction on Qed definitions.  If 
it happens that only transparent definitions are allowed for Extraction, 
then indeed making opaque proofs transparent later would work.  Although 
I view permanent opaqueness as a nice way to enforce modularity.

Briefly, my usage of Coq is on the high side of dependently typed-ness, 
such that type signatures eliminate the need to unfold all but a few 
trivial functions.  However, I do extraction on most functions.  But, I 
don't do extraction until the end of a script (except while debugging).

> > And don't have Extraction force
> > unextracted definitions.
> I don't understand that.  Could you elaborate?

Bug #4449.  Which also contains Pierre Letouzey's objection.

-- Jonathan