The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 26 Nov 2013 13:29:29 -0500,
Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>
 a écrit :

> 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)

That is separate from the transparent vs opaque problem. You can still
do your term in proof mode and separate proofs part from computational
parts with use of the "abstract" tactic, and end the script with
"Defined".

For my concern, still, I am not in the same category as
yours. Writing programs using tactics might be easier, but reading
them, maintaining them and understanding them is also harder.
For me, tactics should be considered for "write-only" stuff. All
relevant part is inside the type. For the term it self it is just
"trust me, the type is inhabited".

> 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.

There is Peano_dec.eq_nat_dec … (and it is even a transparent term).

And I am not against mixing proofs and computation in terms. Not even
against doing proofs inside of terms without tactics. Just that in that
case, the term should be a skeleton with all computational content
exposed and holes for proofs (so use the refine tactic once at the
beginning, and then prove each of your holes). Well, I forgot a
drawback when using "abstract": you should always clean the hypothesis
before using it (it is even mandatory if you are doing some recursive
function with the 'fix' keyword). I must recognize that for now there
is a lack of tools to do that things nicely.

> 
> 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.

It is not yet the case (especially with 'inversion'…), but for me the
main problems are readability, maintainance and full understanding of
what will produce some high-level tactics (like auto, intuition,
firstorder …). Plus when the system finds a proof, knowing if there
exist a shorter proof is not something easy, so designing efficient
high level tactics is not something I expect to see soon. 

> 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.

I also avoid this kind of tactics, which often takes quite a lot of
time to be executed (and also because the arithmetic part I need in
the proofs I usually do is rather trivial).

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

That would mean rely on a more complex kernel.

> 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.

Was it to define equality/order between two structures of about 60
constructors?

I do not think there are trivial ways to implement more efficient
pattern matching representation without loss of trust in the kernel.

If you have a type with many constructors, it is better either to
replace it with a more structured type (for instance: Inductive a := A
| B | C | D | E | F. with be turned into Inductive x := A | B | C.
Inductive y := D | E | F. Inductive a := AC : x -> a | DF : y -> a.
This will reduce 36 cases for equality definition to 20, which is quite
an improvement), or to define functions from your big type to smaller
ones and use them for pattern matching. Remember that you can also
"bind" two values with dependant types (for instance, "Definition
matchable (x y:a) : bool := match x, y with A,D => true | B,F=>true |
C,E=> true | _, _ => false end." can be replaced by "Inductive
matchable : a -> a -> Type := AD : matchable A D | BF : matchable B F |
CE : matchable C E." then a pattern matching against "matchable x y"
will produce only three branches in contrast to the 36 ones you would
require by performing full pattern matching).

> 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)

Well, that could be worth. Although I guess, it would weaken trustness
of the kernell (which would have to compile terms it receives instead
of simply type check them). It would also slower the system by
recompiling often the same pattern match (althugh I guess it is
negligible).

> 
> 
> 
> 
> -- 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\...
> >