在Coq简化期间如何一次应用功能？ [英] How to apply a function once during simplification in Coq?

问题描述

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

From what I understand, function calls in Coq are opaque. Sometimes, I need to use unfold to apply it and then fold to turn the function definition/body back to its name. This is often tedious. My question is, is there an easier way to let apply a specific instance of a function call?

作为最小示例，列表 l ，以证明正确添加 [] 不会更改 l ：

As a minimal example, for a list l, to prove right-appending [] does not change 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 ）的定义（假装还有其他 ++ 我不想应用/扩展的目标）。目前，我唯一知道实现此一次性应用程序的方法是先展开 ++ 然后将其折叠：

Now, I need to apply the definition of ++ (i.e. app) once (pretending there are other ++ in the goal which I don't want to apply/expand). Currently, the only way I know to implement this one time application is to first unfold ++ and then fold it:

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

给予：

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

但是这很不方便，因为我必须弄清楚折叠中使用的术语的形式。我进行了计算，而不是Coq。我的问题可以归结为：

But this is inconvenient as I have to figure out the form of the term to use in fold. I did the computation, not Coq. My question boils down to:

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

Is there a simpler way to implement this one-time function application to the same effect?

推荐答案

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

You can use simpl, compute or vm_compute if you want to ask Coq to perform some computation for you. If the definition of the function is Opaque, the above solution will fail, but you could first prove a rewriting lemma such as:

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 的效果更好。

To answer your comment, I don't know how to tell cbv or compute to only compute a certain symbol. Note that in your case, they seem to compute too eagerly and simpl works better.

这篇关于在Coq简化期间如何一次应用功能？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！