coq - Coq 中的连词与蕴涵

Question

我目前正在阅读《软件基础》一书。当定理被定义时，我经常看到我认为连词更有意义的含义链。例如，在定义鸽巢原则时，作者写道：

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 中似乎回避连词以支持含义链。

Answer 1

这是函数 currying的定理证明者版本。

总而言之，这两个表达式都是正确的（它们是等价的）。

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

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

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