How do you selectively simplify arguments to each

问题:

I'm using Coq 8.5pl1.

To make a contrived but illustrative example,

(* fix so simpl will automatically unfold. *)
Definition double := fix f n := 2*n.

Theorem contrived n : double (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.)

simpl.
   S (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:

match goal with | |- (double ?A) = _ => simpl A end.
   double (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

   double (S (S n)) = 2 + double (S n)

without having to put a separate pattern for each call to double.

I can simplify except for double itself with

remember double as x; simpl; subst x.
   double (S (S n)) = S (S (double (S n)))

回答1:

Opaque/Transparent approach

Combining the results of this answer and this one, we get the following solution:

Opaque double.
simpl (double _).
Transparent double.

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:

Fact test n :
    82 + double (2 + n)
  =
    double (1 + double (1 + 20)) + double (1 * n).
Proof.
  simpl_arg_of double.

The above results in

82 + double (S (S n)) = double (S (double 21)) + double (n + 0)

Had we used something like context [function ?A] => simpl A in the definition of simpl_arg_of, we would've gotten

82 + double (S (S n)) = double 43 + double (n + 0)

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 (sect. 8.7.4) 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:

Arguments double : simpl never.
simpl double.

回答2:

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.
Theorem contrived n : double (2 + n) = 2 + double (1 + n).
rewrite ![_+n]/=.

Will display:

n : nat
============================
double (S (S n)) = 2 + double (S n)

You can also use anonymous rewrite rules:

rewrite (_ : double (2+n) = 2 + double (1+n)) //.

I would personally factor the rewrite in smaller lemmas:

Lemma doubleE n : double n = n + n.
Proof. by elim: n => //= n ihn; rewrite -!plus_n_Sm -plus_n_O. Qed.

Lemma doubleS n : double (1 + n) = 2 + double n.
Proof. by rewrite !doubleE /= -plus_n_Sm. Qed.

Theorem contrived n : double (1+n) = 2 + double n.
rewrite doubleS.