coq - 在 Coq 证明中展开匿名函数

Question

我一直试图在 Coq 中证明涉及使用类型类的东西。

具体的类型类几乎与这个 Functor 类型类相同:https://gist.github.com/aztek/2911378

我的实例如下所示:

Instance ListFunctor : Functor list := { fmap := map }.
  (* Proof stuff here *)
Defined.

map 是标准库中列表的映射。

我做的“证明”基本上只是一个单元测试:

Example list_map_test : fmap (fun x => x + 1) (1::2::3::nil) = (2::3::4::nil).

我的目标看起来像这样，但我被卡住了:

(let (fmap0, _, _) := ListFunctor in fmap0) nat nat
 (fun x : nat => x + 1) (1 :: 2 :: 3 :: nil) = 2 :: 3 :: 4 :: nil

Coq 解构实例以获取 fmap0，然后使用参数 nat nat (fun x : nat => x + 1) (1::2::3::无)。

作为证明的下一步，我想展开 fmap0 或匿名函数。

我该怎么做？我无法执行 unfold fmap0。

我的期望是 fmap0 是标准库 map，因为这是我给实例的内容。

我能够自己销毁实例，但这显示了 fmap0 的抽象版本，而不是在实例化类型类时给出的实现。

我做错了什么？

Answer 1

如果 f 是一个匿名函数(即 fun x => expr 形式的东西)，那么 simpl 就足够了.如果它是一个标识符并且您不能展开它，那么 (1) 它是一个在您的上下文中绑定(bind)的局部变量，或者 (2) 它是一个通过 Qed 定义的全局定义。在后一种情况下，只需从您的定义中删除 Qed，将其替换为 Defined。在前一种情况下，我猜想您应该尝试展开或简化 expr1 以便 Coq 可以访问 f 的实际定义(反过来，可能需要从其他全局定义中删除 Qed。