The Coq mailing list

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

Pragmatically, I'm being blocked by things like nat_eq_sym and S_O. Inlining their definitions doesn't help because Coq's picking up the versions in the library namespaces. I guess I could go edit the libraries. What, practically, is the easiest way to inline these low-level theorems. Reproving is no problem. It's mostly just "auto", but getting tactics to pick up on transparent versions is (at least for me) presenting some hassles. --Kevin

On Tue, Nov 26, 2013 at 1:29 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I agree with Dmitry.

I like the "Proofs as Programs" paradigm and have often preferred to define my functions in proof mode, rather than learning the  syntax of match .. in.. with.. return. (I know that many people like the opposite approach : programs as proofs)

Also, I often prefer putting the data and correctness parts together (intrinsic verification).

Making all my definitions transparent helps me go a long way in my coq proofs by just computation.

Trying to separate computation from proofs is often annoying.

For example, I would have preferred to have a sumbool version of beq_nat in

http://coq.inria.fr/library/Coq.Arith.EqNat.html

It is often a pain to apply the lemmas connecting the boolean value of beq_nat to the equality proposition.

I agree that it makes things slow because the "proof-part" of the inhabitant is often orders of magnitude larger that the "computation-part". I probably even had out of memory errors because of this issue.

But I also think that we can write tactics which try to come up with shorter and simpler extracts.

I had to sometimes avoid using heavy-weight tactics like omega which often comes up a huge inhabitants for types which just require an application of a constructor.

In general, I feel that Coq could represent things internally in a more compact manner.

For example generalized patters are internally compiled into primitive pattern matches.

https://www.lri.fr/~paulin/TypesSummerSchool/lab.pdf (page 6 end)

In my case, this blew up the size of my coq function from 70 lines to ~4000 lines internally.

And there were many recursive calls in that function. I kept running out of memory on a computer with 8GB RAM.

http://t63129.science-mathematics-logic-coq-club.mathematicstalk.info/unfold-causes-out-of-memory-t63129.html

I had to manually write a primitive pattern match (was around ~80 lines) to get around that problem.

I don't see why coq can't keep the generalized patterns internally (once they are typechecked by possibly by compiling to primitive patterns)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Nov 26, 2013 at 4:37 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

For me there is no real problem. For transparent/opaque, a simple rule to have is the following one:
Keep the computational part transparent, and put the proof part opaque.

In practice, a term of type "∀ x, ∃ y, P x y" will be opaque, while a term of type "∀ x, {y | P x y}" will be partly transparent: the part providing 'y' is transparent, while the one proving 'P x y' will be opaque.
To do so, I often combine "refine+abstract", that is for instance: "refine (fun x => let y := <put some term which depends on x> in let proof := (*hole to fill*) _ : P x y in exist y proof). abstract(<put your proof>)."
This mostly provides the best of the two worlds:
– terms are readable and transparent for their relevant part
– proofs remain black magic managed with tactics

Of course there is some annoying points:
– abstract is a 'one shot' tactic, that means that often I do the proof script without it, and at the end I change '.' into ';,[,|,]' and put abstract in front of it.
– you need some good understanding of what parts must be considered computational and what parts must be proofs (in my example, it is obvious, but with Acc recursion things are trickier)

(You can also do it by hand rather than relying on abstract with a "Definition y_term x := <put some term which depends on x>. Lemma y_proof x : P x (y_term x). Proof. <put your proof> Qed. Definition term x := exist (x_term x) (y_proof x)."  This is nicer and more readable, but often not convenient at all.)

A tool which reads a term and make an equivalent one with proofs opaque and computational part transparent would be a nice addition to Coq though (for instance terminating a proof with "Autoed" instead of "Qed" or "Defined" would insert would produce the "y_term", "y_proof" and "term" definitions with "y_term" and "term" transparent, while "y_proof" would be opaque).

In general Coq library is well designed. There is not so much computational parts defined opaque, and proofs are almost always opaque. I find strange to feel the need to make all transparent. Maybe you defined some "Type" terms opaque (like {x|P x}), or use some "Prop" terms (like nat_ind) to produce "Type"s (instead of using "nat_rect") [well, for the last point, I am not sure it is possible due to type conflicts].

2013/11/26 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.

--
.../Sedrikov\...