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
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
lia). One idea would be to make
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
Arguments Z.mul : simpl never.
Since this invocation only matters for
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
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.