How do you selectively simplify arguments to each time a function is called, without evaluating the function itself?
Question
To make a contrived but illustrative example,
(* fix so simpl will automatically unfold. *) Definition double := fix f n := 2*n.n: natdouble (2 + n) = 2 + double (1 + n)
Now, I only want to simplify the arguments to double, and not any part outside of it. (For example, because the rest has already carefully been put into the correct form.)
n: natS (S (n + S (S (n + 0)))) = S (S (S (n + S (n + 0))))
This converted the outside (2 + ...) to (S (S ...)) as well as unfolding double.
I can match one of them by doing:
n: natdouble (S (S n)) = 2 + double (1 + n)
How do I say that I want to simplify all of them? That is, I want to get
without having to put a separate pattern for each call to double.
I can simplify except for double itself with
n: nat
x: nat -> nat
Heqx: x = doublex (S (S n)) = 2 + x (1 + n)n: nat
x: nat -> nat
Heqx: x = doublex (S (S n)) = S (S (x (S n)))n: natdouble (S (S n)) = S (S (double (S n)))
Answer (Anton Trunov)
Opaque/Transparent approach
Combining the results of this answer and this one, we get the following solution:
n: natdouble (2 + n) = 2 + double (1 + n)n: natdouble (S (S n)) = 2 + double (S n)n: natdouble (S (S n)) = 2 + double (S n)
We use the pattern capability of simpl to narrow down its "action domain", and Opaque/Transparent to forbid (allow resp.) unfolding of double.
Custom tactic approach
We can also define a custom tactic for simplifying arguments:
(* simplifies the first argument of a function *) Ltac simpl_arg_of function := repeat multimatch goal with | |- context [function ?A] => let A' := eval cbn -[function] in A in change A with A' end.
That let A' := ... construction is needed to protect nested functions from simplification. Here is a simple test:
n: nat82 + double (2 + n) = double (1 + double (1 + 20)) + double (1 * n)n: nat82 + double (2 + n) = double (1 + double (1 + 20)) + double (1 * n)n: nat82 + double (S (S n)) = double (S (double 21)) + double (n + 0)
The above results in
Had we used something like context [function ?A] => simpl A in the definition of simpl_arg_of, we would've gotten
instead.
Arguments directive approach
As suggested by @eponier in comments, we can take advantage of yet another form of simpl -- simpl <qualid>, which the manual defines as:
This applies simpl only to the applicative subterms whose head occurrence is the unfoldable constant qualid (the constant can be referred to by its notation using string if such a notation exists).
The Opaque/Transparent approach doesn't work with it, however we can block unfolding of double using the Arguments directive:
n: natdouble (2 + n) = 2 + double (1 + n)n: natdouble (S (S n)) = 2 + double (S n)
Answer (ejgallego)
You may find the ssreflect pattern selection language and rewrite mechanism useful here. For instance, you can have a finer grained control with patterns + the simpl operator /=:
From mathcomp Require Import ssreflect. Definition double := fix f n := 2*n.n: natdouble (2 + n) = 2 + double (1 + n)n: natdouble (S (S n)) = 2 + double (S n)
Will display:
You can also use anonymous rewrite rules:
n: natdouble (2 + n) = 2 + double (1 + n)
I would personally factor the rewrite in smaller lemmas:
n: natdouble n = n + nby elim: n => //= n ihn; rewrite -!plus_n_Sm -plus_n_O. Qed.n: natdouble n = n + nn: natdouble (1 + n) = 2 + double nby rewrite !doubleE /= -plus_n_Sm. Qed.n: natdouble (1 + n) = 2 + double nnow rewrite doubleS. Qed.n: natdouble (1 + n) = 2 + double n