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

Posted 2023-05-08

【中文标题】Coq 中使用 fun 的 Curry-Howard 同构定义

【英文标题】：Curry-Howard isomorphism definitions in Coq using fun

【发布时间】：2015-01-12 09:47:32

【问题描述】：

我在 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". 我已经尝试过我之前在脚本中使用的常用策略，并且我确信必须使用相同的方法（有趣）来解决这个问题，但是我似乎尝试的一切都以该错误消息结尾。有什么建议吗？

【问题讨论】：

很难说可能是什么问题；你能把你的脚本的其余部分放在这里，或者是一个简化的版本吗？

更多信息会很棒。这可能是符号范围的问题，* 被解释为自然数的乘法。

您是否正在寻找在产品类型上定义的选择器 fst 和 snd？

【参考方案1】：

您似乎正在定义一个作为输入的函数：

A -> (A -> C) 类型的函数：给定一个A 类型的对象，它返回一个A -> C 类型的函数。 (A -> C) -> A 类型的函数：给定一个A -> C 类型的函数，它返回一个A 类型的对象。

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

希望对你有帮助，

V.