COQ 定义 curry howard (A -> B -> C) -> (B -> A -> C) 使用集合

Question

我一直盯着这张脸看了好几个小时不明白:(

我需要使用 coq 解决一些定义，我应该通过 Curry Howard 同构来解决。我已经阅读了，但仍然不知道我在做什么。我查看了其他示例并尝试以这些方式进行操作，但我总是遇到错误。

例如，这里我需要定义这个：

Variables A B C : Set.

Definition c01 : (A -> B -> C) -> (B -> A -> C) :=

这是我的尝试：

fun g => fun p => g (snd p) (fst p).
end.

我也试过

fun f => fun b => fun a => f (b , a)
end.

最终它只是说它期待的类型与我给出的不同，有时它会说：“预期有类型“?9 * ?10”。”

在阅读了我能找到的所有内容后，我真的很难理解这一点。

请有人解释一下:(

Answer 1

我猜你不知道如何正确读取类型。

c01 的类型是 (A -> B -> C) -> (B -> A -> C)。这意味着它是一个函数，它接受一个函数作为参数并返回一个函数。

它采用“带有两个参数的函数”（我的意思是 Haskell 意义上的“带有两个参数的函数”，而不是 Scala 或 Java 意义上的） ，类型为A 和B，返回一个C 类型的值。

它必须返回一个带有两个参数的函数，类型为A 和B（但顺序相反），它返回一个类型为C 的值。

那么c01这个函数必须做什么？

它必须接受一个函数，并将其转换为相同的函数，但其​​参数的顺序颠倒。

所以：

fun f => fun b => fun a => f a b

或等效（只是添加一些括号使其更清晰）：

fun f => (fun b => fun a => f a b)