The Coq mailing list

[Benjamin Werner <werner>]

        Hello Venanzio,

> I have some problem in the use of transparent and opaque constants.
> I have this proof of decidability of gt:
[....]
> I need to declare all of them as transparent:
> 
> 
> Transparent le_lt_dec.
> Transparent le_gt_dec.
> Transparent gt_decidable.
> 
> 
> But I would like le_lt_dec and le_gt_dec to remain opaque. And maybe also 
> to have two version of the decidability of gt, one transparent and one 
> opaque.
> In other words I don't want to declare le_lt_dec, le_gt_dec, gt_decidable 
> as transparent, but rather to define a new constant
> 
> gt_dec = gt_decidable with le_lt_dec and gt_decidable unfolded
> 
> The only way I found to do this is manually: first I found the needed 
> term by giving the transparency commands and
> 
> Eval Compute in gt_decidable
> 
> and so getting an orrible expression, and then defining
> 
> Definition gt_dec := orrible expression.
> 
> Is there some nicer way to do this?


My first, quick, answer would be: redefine a second version of the
constants  le_lt_dec and gt_decidable (say you call them le_lt_dec'
and gt_decidable'), have these transparent and use 
them for your gt_dec. Keep the original ones opaque for other uses.

This is not very elegant, but seems coherent to me, in the end.

Of course, it will not work if you need the fact that 
le_lt_dec = le_lt_dec' this soultion does not work. In this case I
would understand that your problem is the way the system deals with
transparent constants (when does it unfold them, etc).


Hope this helps,


best wishes,


Benjamin Werner
----------------------------------------------------------------------------
Projet Coq
INRIA-Rocquencourt, BP 105, F-78 153 LE CHESNAY cedex, FRANCE
E-mail: 
Benjamin.Werner AT inria.fr
Phone:  +33 (1) 39 63 52 31
Mobile: +33 (6) 11 82 55 02
Fax:    +33 (1) 39 63 56 84
http://pauillac.inria.fr/~werner
-----------------------------------------------------------------------------