在 Coq 证明中展开匿名函数

Question

我一直试图在 Coq 中证明涉及类型 class.

的东西

具体类型 class 几乎与此 Functor 类型相同 class: https://gist.github.com/aztek/2911378

我的实例如下所示：

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

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

我做的"proof"基本上只是一个单元测试：

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 :: nil).

应用生成的匿名函数

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

我该怎么做？我做不到 unfold fmap0.

我的期望是 fmap0 是标准库 map 因为那是我给实例的。

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

我做错了什么？

Answer 1

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

Answer 2

我不知道为什么，但如果你直接简化目标

1 subgoal
______________________________________(1/1)
fmap (λ x : nat, (x + 1)%nat) (1 :: 2 :: 3 :: [ ]) = 2 :: 3 :: 4 :: [ ]

例如，使用 simpl 或 cbv，您将获得 map 的实例（实际上，您将 map S 的结果应用于 1 :: 2 :: 3 :: []因此目标变得微不足道）。我不知道为什么展开 fmap 或破坏 ListFunctor 会产生通用的 fmap0.

在 Coq 证明中展开匿名函数

Unfold anonymous function in Coq proof

coq