## simpl is less annoying than you think

- May 22, 2018

In this blogpost we find out that it is possible to tweak the behavior of the Coq `simpl`

tactic. We find it particularly useful when dealing with arithmetic goals on Z.

We just discovered an answer to a longstanding annoyance we faced when dealing with arithmetic Coq goals. Consider the following Coq goal, using integers on `Z`

:

```
Require Import ZArith.
Open Scope Z_scope.
Goal forall a, 2 * a = 0 * a + a * 2.
intros. simpl.
```

We call the `simpl`

tactic to simplify `0 * a + ...`

into `...`

. Unfortunately, since `*`

is defined by pattern matching on its first argument, `simpl`

also unfolds `2 * a`

:

```
a : Z
============================
match a with
| 0 => 0
| Z.pos y' => Z.pos y'~0
| Z.neg y' => Z.neg y'~0
end = a * 2
```

This is both unconvenient and unsupported by automated tactics (such as `omega`

or `lia`

). One idea would be to make `Z.mul`

opaque:

```
Opaque Z.mul.
```

This prevents both `2 * a`

and `0 * a`

from being simplified. This can be seen as a reasonable trade-off (`omega`

will still be able to solve the goal).

However it also prevents reduction using `eval compute`

, which breaks the PolTac library for example (interestingly, `eval vm_compute`

ignores Opaque).

```
let x := (eval compute in (2*3)) in pose x.
(* x := 2*3 *)
let x := (eval vm_compute in (2*3)) in pose x.
(* x := 6 *)
```

A better solution can be found by reading the manual section for `simpl`

(!). It is possible to customize for each definition the amount of unfolding performed by `simpl`

. For example, the following instructs `simpl`

to never unfold `Z.mul`

:

```
Arguments Z.mul : simpl never.
```

Since this invocation only matters for `simpl`

, `eval compute`

and PolTac both continue to work.

```
let x := (eval compute in (2*3)) in pose x.
(* x := 6 *)
Goal forall a, 2 * a = 0 * a + a * 2.
intros. simpl.
(* 2 * a = 0 * a + a * 2 *)
```

And even better, we can achieve what we initially intended (which is to simplify away `0 * a`

), by instructing `simpl`

to only unfold a definition if doing so does not introduce a `match`

:

```
Arguments Z.mul : simpl nomatch.
```

```
Goal forall a, 2 * a = 0 * a + a * 2.
intros. simpl.
(* 2 * a = a * 2 *)
```

More configuration options are possible, and are thoroughly detailed in the manual page.