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

2019年7月22日 224次阅读

据我所知,Coq中的函数调用是不透明的.

有时,我需要使用展开来应用它,然后折叠以将函数定义/正文转回其名称.这通常很乏味.我的问题是,是否有更简单的方法来应用函数调用的特定实例？

作为一个最小的例子,对于列表l,证明right-appending []不会改变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

但这很不方便,因为我必须弄清楚在折叠中使用的术语的形式.我做了计算,而不是Coq.我的问题归结为：

是否有更简单的方法来实现此一次性函数应用程序以达到同样的效果？

最佳答案 如果要让Coq为您执行某些计算,可以使用simpl,compute或vm_compute.如果函数的定义是不透明的,则上述解决方案将失败,但您可以首先证明重写引理,例如：

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只计算某个符号.请注意,在您的情况下,它们似乎过于急切地计算并且简化工作更好.

点赞