使用fun的Coq中的Curry-Howard同构定义

Question

我在Coq中定义时遇到了一些问题，更具体地说是在使用CHI定义时。我已经设法获得了对基本原则的理解，但当我试图定义这一点时，

((A -> (A -> C)) * ((A -> C) -> A)) -> C :=

我一无所获，因为它一直在告诉我：

"Error: The type of this term is a product while it is expected to be "C"。

我已经尝试了我之前在脚本中使用的常用策略，我确信必须使用相同的方法(有趣)来解决这个问题，但是我似乎尝试的一切都以该错误消息结束。有什么建议吗？

Answer 1

看起来您正在定义一个接受作为输入的函数：

• 一个A -> (A -> C)类型的函数:给定一个A类型的对象，它返回一个(A -> C) -> A类型的A -> C.
• a函数:给定一个A -> C类型的函数，它返回一个A.

类型的对象

您正在尝试构建一个C类型的对象，我不知道您将如何做到这一点。但是，您可以通过组合作为输入的两个函数来构建A类型的对象。

希望能有所帮助，

V。