gpt4 book ai didi

coq - 连词和。 Coq 中的含义

转载 作者:行者123 更新时间:2023-12-04 02:25:50 24 4
gpt4 key购买 nike

我目前正在阅读这本书 Software Foundations .当定理被定义时,我经常看到我认为连词更有意义的含义链。例如,在定义鸽巢原则时,作者写道:

Theorem pigeonhole_principle: ∀{X:Type} (l1 l2:list X),
excluded_middle →
(∀x, appears_in x l1 → appears_in x l2) →
length l2 < length l1 →
repeats l1.

如果它看起来更像这样,这个定义对我来说会更有意义:
Theorem pigeonhole_principle: ∀{X:Type} (l1 l2:list X),
(excluded_middle /\
(∀x, appears_in x l1 → appears_in x l2) /\
length l2 < length l1) →
repeats l1.

为什么第一个版本是正确的?为什么连词不更合适?

这只是一个例子。更一般地说,我在问为什么在 coq 中似乎回避连词以支持含义链。

最佳答案

这是 function currying 的定理证明器版本.

总而言之,这两个表达式都是正确的(它们是等价的)。

一个人说:给我一个“排斥的中间”。现在给我假设 2。现在给我假设 3。好的,这是一个属性“repeats l1”。

另一个说:给我一个“排除中间”,以及假设 2 和假设 3。好的,这里有一个属性“repeats l1”。

Coq 等证明助手的用户和实现者也是函数式程序员,对他们来说,curried 版本和 uncurried 版本一样自然。

关于coq - 连词和。 Coq 中的含义,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/13617065/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com