根据我的理解,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做的。我的问题归结为:
有没有更简单的方法来实现这种一次性函数应用,达到相同的效果?
Qed
而不是Defined
)。 - Vinz