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

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).

现在，我只想将参数简化为双倍，
而不是它之外的任何部分。 (例如，因为
rest 已经被仔细地放入正确的形式。)

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 设置单独的模式。

我可以简化除了 double 本身

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

Answer 1

不透明/透明方法

结合this answer的结果和 this one ，我们得到以下解决方案:

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> ，手册( sect. 8.7.4 )定​​义为:

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).

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

Arguments double : simpl never.
simpl double.