您如何在每次调用函数时有选择地简化参数，而不评估函数本身？ [英] How do you selectively simplify arguments to each time a function is called, without evaluating the function itself?

问题描述

我使用的是Coq 8.5pl1。

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

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

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

这将外部（2 + ...）转换为（S（S ...）），并且展开了两倍。

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

推荐答案

不透明/透明方法

结合此答案和此，我们得到以下解决方案：

Opaque/Transparent approach

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

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

我们使用 simpl 的模式功能缩小其操作范围，并不透明 / 透明以禁止（允许）展开 double 。

We use the pattern capability of simpl to narrow down its "action domain", and Opaque/Transparent to forbid (allow resp.) unfolding of double.

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

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.

那个 let A'：= ... 需要构造以防止嵌套函数被简化。这是一个简单的测试：

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.

以上结果为

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

我们曾经使用过类似 context [function？A] =>的东西。 simpl A 在 simpl_arg_of 的定义中，我们会得到

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)

相反。

正如@eponier在评论中建议的那样，可以利用 simpl - simpl< qualid> 的另一种形式，该手册（第8.7.4节）定义为：

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:

这仅将 simpl 应用于头部出现为不可折叠常数 qualid 的应用子项（如果存在这种符号，则常量可以使用字符串的符号来表示）。

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 / 透明方法不起作用，但是我们可以阻止 double 的展开使用 Ar guments 指令：

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.

这篇关于您如何在每次调用函数时有选择地简化参数，而不评估函数本身？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！