The Coq mailing list

[Venanzio Capretta <venanzio AT cs.kun.nl>]

I have some problem in the use of transparent and opaque constants.
I have this proof of decidability of gt:


Require Export Arith.
Require Export Compare_dec.

Lemma gt_decidable : (m : nat){(gt n m)}+{~(gt n m)}.

Intro m.
Case (le_gt_dec n m).
Intro H.
Right .
Apply (le_not_gt n m).
Assumption.

Intro.
Left ; Assumption.

Qed.


I need gt_decidable to be completely transparent, because I will use it 
to define types by cases on (gt_decidable n m), and to have that these 
types are equal to the types that I expect the actual computation of 
which of the two disjucts holds is necessary.
Since the proof uses also le_not_gt, whose proof in turn uses le_lt_dec, 
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?

Thank you,
  Venanzio


----------------------
Venanzio Capretta
University of Nijmegen
Faculty of Mathematics
       and Informatics
the Nederlands
tel.: +31-24-3652647
----------------------