Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Dec 03, 2014 at 01:42:17PM -0600, John Wiegley wrote:
> I'm using the SSReflect library, and when I extract my program to Haskell, I
> get the following warning.  Perhaps there are some definitions in the 
> library
> which should be made transparent?
> 
>     Warning: The extraction is currently set to bypass opacity,
>     the following opaque constant bodies have been accessed :
>      andP eqP eqnP idP iffP inj_eqAxiom pair_eqP val_eqP.

Hello John, the reflect predicate is stated in Type, hence one
can use, say, eqnP to define data.  This is useful because by pattern
matching on eqnP one gets to know if the two nats are equal and
the same time he obtains a proof of their equality, that in turn can be
used to cast another term (to "help" the type checker).  This also means
that exracting a program may end up needing the body of eqnP.  (I guess
this is what is happening).

But given you are using extraction and math comp in the same sentence
I want to warn you, since you will probably encounter the following
oddities/problems.

The notion of opacity is an optimization: you tell Coq you are not going
to need the body of the opaque constant in order to type check the rest
of your statements and proofs.  If Coq had the freedom to unfold,
reduce and eventually duplicate everything it may end up getting lost
doing that.
Indeed, many programs in the math comp library are marked as opaque, or
locked by starting their code with a match over an opaque proof of unit,
to prevent Coq from computing too much, by mistake, with them.  So I'm
afraid we can't avoid warnings like the one you had.

Another thing you may want to know is that programs in the math
comp library are optimized for doing proofs with them or doing proofs
about them, not for runnig them.  The extracted code is not going to
be very efficient.  If you want to use math comp to produce certified
code I think you may be interested in the coqEAL project, where one
gets the best of both worlds: write efficient algorithms on optimized
data types and prove them correct in the comfort of the math comp
library.

I hope it helps,
-- 
Enrico Tassi