The Coq mailing list

[Randy Pollack <rap AT dcs.ed.ac.uk>]

Hi Hugo,

Hugo Herbelin writes:
 >   As far as le_lt_dec is concerned (and other lemmas from Peano_dec
 > and Compare_dec), it is transparent in the current cvs version of Coq.
 > 

I'll be happy if new versions of Coq have these lemmas transparent for
computation, but in the version 7.3.1 library, that lemma is
permanently opaque.

BTW, the proofs in Peano_dec and Compare_dec use other lemmas.  Are
all of those lemmas also transparent in the CVS version?

 >   As far as I know, the question whether a lemma is Opaque or not
 > results of a compromise between the need for efficiency (transparency
 > may induces very strong time penalty on type checking) and convenience
 > for reduction.

Of course, but Coq implements a constructive type theory.  Who ever
heard of a constructive type theory where you can't compute.

So we probably need more flexibility than Transparent/Opaque.  Maybe
several levels of transparency, and tactics can specify which level
they will unfold.  Maybe "Exact" and "Change" should see every lemma
as transparent.  (If I say "Exact" and "Change" I mean it, why should
the tool not try to do what I say?).  The Coq community may think
about other possible solutions.

 >   For which (other) theorems do you expect transparency?

What about course-of-values recursion over nat, induction_ltof1.  This
is not usable for computation in 7.3.1.  There are many other theorems
that probably should be transparent.

Best,
Randy