在Coq简化期间如何一次应用功能？

Question

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

举一个最小的例子，对于list 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。我的问题归结为：

有没有更简单的方法来实现此一次性功能应用程序以达到相同的效果？

Answer 1

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

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

使用你的技术，然后rewrite在必要时使用它。

这是一个使用的示例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效果更好。