The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

is there a way to make Coq print proof terms using eliminators when these 
proof terms are constructed using 
eliminators? 

For example “destruct” uses the eliminators but the proof terms constructed 
with destruct are printed in terms of “match” even
when I request the corresponding eliminator to be opaque. An example code is 
below.

This makes it very difficult for me to teach Coq to mathematicians. I can 
explain eliminators to them but I do not know how to explain
match to them and I am not even sure that a semantically adequate theory of 
dependent “match” exists. In any event even if it does 
exist it is still not right that when I request something to be opaque Coq 
unfolds it without asking. 

***

Opaque Empty_set_rect.
Opaque Empty_set_rec.
Opaque Empty_set_ind.

Definition test { X : UU } : Empty_set -> X .
Proof . intros X H . destruct H . Defined.

Print test.

Definition test' { X : UU } : Empty_set -> X := fun H => Empty_set_rect ( fun 
x => X ) H . 

Print test' . 

***

Vladimir.