Conjunction vs. Implication in Coq

Question

I am currently working through the book Software Foundations. When theorems are defined, I often see chains of implications where I believe conjunctions would make more sense. For example, in defining the pigeonhole principle, the authors write:

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.

This definition would make more sense to me if it looked more like this:

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.

Why is the first version correct? Why wouldn't conjunctions be more appropriate?

That is just an example. More generally, I am asking why conjunctions seem to be shunned in favor of chains of implications in coq.

Pascal Cuoq Pascal Cuoq · Accepted Answer · 2012-11-29T00:58:10

This is the theorem-prover version of function currying.

To summarise, the two expressions are both correct (they are equivalent).

One says: Give me an “excluded middle”. Now give me hypothesis 2. Now give me hypothesis 3. Okay, here is a property “repeats l1”.

The other says: Give me an “excluded middle”, and hypothesis 2, and hypothesis 3. Okay, here is a property “repeats l1”.

Users and implementers of proof assistants such as Coq are also functional programmers and the curried version is as natural for them as the uncurried one.

Conjunction vs. Implication in Coq

1 Answers