The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Dan Grayson and I hacked into the destruct a couple of years ago to make it more powerful and it used

the _rect .

V.

On Oct 23, 2014, at 11:00 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:

Perhaps I'm not understanding fully your question, but match *is* the eliminator.  Empty_set_rect is the inductive principle, build in terms of that eliminator.  If you want to use the later, you should use [induction] instead of destruct.  [destruct] is not unfolding anything, it is just a tactic for building a [match] interactively.

Best,

Beta

On Thu, Oct 23, 2014 at 11:34 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

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.