如何在Coq中简化过程中只应用一次函数？

Question

如何在Coq中简化过程中只应用一次函数？

5

根据我的理解，Coq中的函数调用是不透明的。有时候我需要使用unfold来应用它，然后使用fold将函数定义/主体转换回其名称。这常常很繁琐。我的问题是，有没有更简单的方法来应用函数调用的特定实例？

作为一个最简示例，对于一个列表l，要证明右侧追加[]不会改变l：

Theorem nil_right_app: forall {Y} (l: list Y), l ++ [] = l.
Proof.
  induction l. 
    reflexivity.

这将得到以下内容：

1 subgoals
Y : Type
x : Y
l : list Y
IHl : l ++ [] = l
______________________________________(1/1)
(x :: l) ++ [] = x :: l

现在，我需要对++（即app）的定义应用一次（假装目标中还有其他我不想应用/展开的++）。目前，我知道实现这种一次性应用的唯一方法是先展开++，然后再折叠它。

    unfold app at 1. fold (app l []).

提供：

______________________________________(1/1)
x :: l ++ [] = x :: l

但这种方法很不方便，因为我必须弄清楚术语在fold中的形式。计算是我做的，而不是Coq做的。我的问题归结为：

有没有更简单的方法来实现这种一次性函数应用，达到相同的效果？

- thor

1

Coq的所有定义都不是不透明的，但有方法可以防止Coq自动展开定义（例如，在使用策略定义函数时使用Qed而不是Defined）。 - Vinz

什么是不透明？ - Charlie Parker

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Vinz · Accepted Answer

如果你想让Coq执行一些计算，可以使用simpl、compute或vm_compute。如果函数的定义是Opaque，上述解决方案将失败，但你可以先证明一个重写引理，例如：

forall (A:Type) (a:A) (l1 l2: list A), (a :: l1) ++ l2 = a :: (l1 ++ l2).

当需要时，使用您的技巧进行重写。

以下是使用 simpl 的示例：

Theorem nil_right_app: forall {Y} (l: list Y), l ++ nil = l.
Proof.
(* solve the first case directly *)
intros Y; induction l as [ | hd tl hi]; [reflexivity | ]. 
simpl app. (* or simply "simpl." *)
rewrite hi.
reflexivity.
Qed.

为了回答您的评论，我不知道如何告诉cbv或compute只计算某个符号。请注意，在您的情况下，它们似乎过于急切地进行计算，而simpl效果更好。