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

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 ...)) 以及展开的 double。

我可以匹配其中之一：

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

Opaque/Transparent接近

结合 and 的结果，我们得到以下解决方案：

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

我们使用simpl的模式能力来缩小其“作用域”，Opaque/Transparent禁止（允许resp.）展开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)

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

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

相反。

参数指令方法

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

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 方法不适用于它，但是我们可以使用 Arguments 指令阻止 double 的展开：

Arguments double : simpl never.
simpl double.

Answer 2

您可能会发现 ssreflect 模式选择语言和重写机制在这里很有用。例如，您可以使用模式 + 简单运算符 /=:

进行更细粒度的控制

From mathcomp Require Import ssreflect.
Definition double := fix f n := 2*n.
Theorem contrived n : double (2 + n) = 2 + double (1 + n).
rewrite ![_+n]/=.

将显示：

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

您也可以使用匿名重写规则：

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

我个人会在更小的引理中考虑重写：

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.

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

How do you selectively simplify arguments to each time a function is called, without evaluating the function itself?

coq

coq-tactic

Opaque/Transparent接近

自定义策略方法

参数指令方法