我目前正在阅读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。好的,这是一个属性“repeat l1”。
另一个说:给我一个“排除中间”,假设2和假设3。好吧,这是一个属性“重复l1”。
证明助手的用户和实现者(例如Coq)也是功能性程序员,对于他们来说, curry 版本与未经 curry 的版本一样自然。
关于coq - Coq的连词与含义,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/13617065/