4

我正在使用 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).

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

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

2 回答 2

5

不透明/透明方法

结合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>，手册将其定义为：

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

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

Arguments double : simpl never.
simpl double.
于 2016-12-31T11:04:06.653 回答
2

您可能会发现 ssreflect 模式选择语言和重写机制在这里很有用。例如，您可以使用模式 + simpl 运算符进行更细粒度的控制/=：

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.
于 2016-12-31T14:43:19.197 回答