How to prohibit simple tactics for deploying arithmetic expressions?

Question

simpl tactics simpl expressions like 2 + a to “match trees” that don't seem simple. For instance:

 Goal forall i:Z, ((fun x => x + i) 3 = i + 3). simpl. 

Leads to:

 forall i : Z, match i with | 0 => 3 | Z.pos y' => Z.pos match y' with | q~1 => match q with | q0~1 => (Pos.succ q0)~1 | q0~0 => (Pos.succ q0)~0 | 1 => 3 end~0 | q~0 => match q with | q0~1 => (Pos.succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1 | 1 => 4 end | Z.neg y' => Z.pos_sub 3 y' end = i + 3 

How to avoid such complications with simpl tactics?

This specific goal can be solved with omega , but if it is a little more complicated, omega fails, and I have to resort to something like: replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a) replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a) replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a) .

Answer 1

You can control the expansion of a definition using the Transparent and Opaque commands. In your example, you should be able to say something like

 Opaque Z.add. simpl. Transparent Z.add. 

Alternatively, Arguments command can be used to specify simpl tactics to avoid simplifying conditions in certain contexts. For instance.

 Arguments Z.add _ _ : simpl nomatch. 

does the trick for me in your case. What this particular option does is to avoid simplifying the deadline when after that a big ugly match appears after you have done it (as you saw in your example). However, there are other options.

Finally, for completeness only, the Ssreflect library provides a good framework for localizing certain definitions. So you can say something like

 rewrite (lock Z.add) /= -lock. 

means "lock Z.add so that it does not simplify, and then simplifies the remaining expression (switch /= ), then unlock the definition ( -lock ) again."

Answer 2

You can customize the behavior of tactical tactics to get fewer matches.

 Require Import Coq.ZArith.ZArith. Goal forall i:Z, ((fun x => (x + i)%Z) 3%Z = (i + 3)%Z). Arguments Z.add xy : simpl nomatch. simpl. 

Read more about it here .

Otherwise, you can use another tactic that allows you to choose how to reduce. cbn beta , for example.