The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Dmitry,

I'm sympathetic. With respect to (1) figuring out which proofs are opaque and thus need some action, "Print Opaque Dependencies" does the trick (thank you Adam). With respect to having to reprove, I believe that if you don't care about computation efficiency, you can just inline the existing proof and change "Qed" to "Defined." So there's no absolute need to reprove. In cases where the proof is fatally inefficient, naturally a new proof will be needed. 

My rationale for wanting to be able to "run" my program/proofs is only that I want to show students that we've succeeded (in Coq). However, I can imagine that, to the extent that proofs *often* involve/require computations, we'd like to be able to "run" programs, more generally. 

To the extent that the opacity of most of the fundamental proofs in Coq are opaque, doesn't this become a major problem, even for people who have more than mere pedagogical reasons for wanting to compute (within Coq)?

Kevin

On Tue, Nov 26, 2013 at 1:50 AM, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

> Arnaud, Thank you. The notion that it's reasonable to force one who wishes
> to program to "reprove" theorems with opaque proof terms makes sense, given
> that proofs are in general produced without regard for efficiency.

  But it's not efficient in sense of "time spent by programmer to 1.
determine which proofs are opaque, 2. prove it transparently".  For
example, I needed to compute with nat, plus and le, so I spent more
than an hour of my time to prove some facts about it.
  Imagine how much time I could spend if I had real numbers or
something non-trivial (even Z!).
  So I think it's completely not reasonable to force programmer to
"reprove" already proved things, if he's sure that execution time of
"Eval compute" doesn't matter compared to "reprove" time.