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.