The Coq mailing list

["Cuihtlauac ALVARADO" <cuihtlauac.alvarado AT francetelecom.com>]

Title: Re: [Coq-Club] Opaque in the library

Hi all,

> > This function "shift" doesn't compute as I expected, because
> > "le_lt_dec" is Opaque in the library.  Of course, this is just one
> > lemma; I simply proved it again for myself, making it Transparent.
>
>   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.
>
>   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.
>
>   For which (other) theorems do you expect transparency?

It is not very easy to know in advance which theorems should be
transparent or not (at least for me). Suppose you are dealing with
vectors :

  Inductive vect [A:Set] : nat -> Set :=
  | nil : (vect A O)
  | cons : (x:A)(n:nat)(vect A n)->(vect A (S n)).

Then you want to build the linear-time reversal function (the one
which use a buffer not concatenation) :

  rev_app : (A:Set)(n:nat)(vect A n)->(m:nat)(vect A m)->(vect A (plus n m)).

I like to build it Lemma + Defined way. I found it easier than
guessing <...>Cases types. Anyway you'll end up needing something
like:

  plus_S : (n,m:nat)(plus n (S m))=(plus (S n) m).

Which is available in the library but *opaque* and which is not a
clear candidate for transparency (same remark: at least for me at
proof-time). In this case plus_S transparency is sufficient, but it
might not always be the case. If plus_S used others theorems and if
plus_S was *reduced* during reduction of, say (rev_app A n u m v),
then all those theorems would have to be transparent to.

Sometimes I end up in proof mode, I try Compute my value and then I
try to find the lemmas occurring in the (long & horrible) output just
to make them transparent.

Transparency & opacity should be something *local*: sometimes there
are type checks, then there are things which should not be reduced,
here opacity makes sense, but some others times user computations
happen, then reduction should not stop on opacity.

--
Cuihtlauac ALVARADO - France Telecom R&D - DTL/TAL
2, avenue Pierre Marzin - 22307 Lannion - France
Tel: +33 2 96 05 32 73 - Fax: +33 2 96 05 39 45