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.