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.好的,这是一个属性"重复l1".

另一个说:给我一个"排除中间",假设2和假设3.好的,这是一个属性"重复l1".

像Coq这样的证明助手的用户和实施者也是功能性程序员,而且curried版本对于他们来说就像未经证实的那样一样自然.