如何在每次调用函数时有选择地简化参数，而不评估函数本身？

Question

我正在使用 Coq 8.5pl1。

举一个人为但具有说明性的例子，

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

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

现在，我只想将参数简化为 double，而不是其之外的任何部分。（例如，因为其余部分已经被仔细地放入正确的形式中。）

simpl.
   S (S (n + S (S (n + 0)))) = S (S (S (n + S (n + 0))))

这将外部 (2 + ...) 转换为 (S (S ...)) 以及展开双精度。

我可以通过执行以下操作来匹配其中之一：

match goal with | |- (double ?A) = _ => simpl A end.
   double (S (S n)) = 2 + double (1 + n)

我怎么说我想简化所有这些呢？也就是说，我想得到

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

无需为每次调用 double 放置单独的模式。

我可以简化除了双重本身

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

Answer 1

不透明/透明方法

结合这个答案和这个答案的结果，我们得到以下解决方案：

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

我们使用 的模式能力simpl来缩小其“动作域”，并Opaque/Transparent禁止（允许）展开double。

定制战术方法

我们还可以定义一个自定义策略来简化参数：

(* 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.

let A' := ...需要这种构造来保护嵌套函数不被简化。这是一个简单的测试：

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

上面的结果是

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

如果我们context [function ?A] => simpl A在 的定义中使用类似的东西simpl_arg_of，我们就会得到

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

反而。

参数指令方法

正如 @eponier 在评论中所建议的，我们可以利用另一种形式的simpl-- simpl <qualid>，手册将其定义为：

这仅适用于其头部出现是可展开常量限定simpl的应用子项（如果存在这样的表示法，则可以使用字符串通过其表示法来引用常量）。

Opaque/方法Transparent不适用于它，但是我们可以阻止double使用该Arguments指令的展开：

Arguments double : simpl never.
simpl double.