The Coq mailing list

[olivier pons <pons.olivier AT gmail.com>]

Hello,

One way to  avoid reduction of a specific functions by simpl is to make it opaque using the Opaque command.

Opaque functionName

to make it reducable again use the Transparent command

Transparent functionName

On you example 

Coq < Lemma redtest:5+3-1=9.

1 subgoal

============================

   5 + 3 - 1 = 9

redtest < Opaque minus.

redtest < simpl.

1 subgoal

============================

   8 - 1 = 9

redtest < Transparent minus.

redtest < simpl.

1 subgoal

============================

   7 = 9

...

O.

2014-04-11 18:41 GMT+02:00 Nuno Gaspar <nmpgaspar AT gmail.com>:

Hello.

Is there a way to make specific functions not be reduced by simpl (even when they could be I mean..)?

For instance,

Example redtest:

  5 + 3 - 1 = 9.

Proof.

  simpl.

simpl will fully reduce the _expression_. What if I didn't want the minus function to reduce?

Sure, in this particular example I could do simpl plus, but I would like to be able to set this kind of "guard" for some functions, and also be able to unset them on demand.

I believe ssreflect does something similar, but I can't remember exactly how..

Help please :)

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.