Running the classical pigeonhole principle in Agda

Martin Escardo & Paulo Oliva, May 2011. In collaboration with Ulrich Berger & Monika Seisenberger. Transcribed to Agda 29 April - 3 May 2011 by Martin Escardo, based on other Agda modules produced in previous years (for the selection monad J and continuation monad K, double-negation shift, classical choice etc., which are also included below).
This version 27th May 2011, 19:27 BST.
You can download all the agda files as a zip file.
The main Agda files (html-formated with hyperlinks to the other files, which allow navigation by clicking at any word) are
  1. Slides of talk given at MFPS.

  2. InfinitePigeon

    3. (See also InfinitePigeonLessEfficient.)

  3. FinitePigeon

  4. Examples

The classical axiom of countable choice (that is, choice formulated with the classical existential quantifier) is realized in K-AC-N using any of
  1. K-Shift-BBC with Berardi, Bezem and Coquand's functional,

  2. K-Shift-MBR with Berger-Oliva modified bar recursion,

  3. K-Shift-Selection with Escardo and Oliva's countable product of selection functions (download pdf),

by performing a suitable choice in the wrapper module K-Shift.

The classical infinite pigeonhole principle says that any infinite sequence of booleans has an infinite constant subsequence (this is the program/proof "pigeonhole" in InfinitePigeon).

We work with the negative translation or more generally Friedman's A-translation, which amounts to prefixing "K R" (double negation monad) in front of existential quantifiers, disjunctions, and atomic formulas (equations of ground type), where R is an arbitrary proposition (as a first approximation, think of the parameter R as false).

Starting with a proof that uses both excluded middle and classical countable choice (i.e. choice formulated with the classical existential quantifier), we eventually get to a theorem that avoids K and considers a finite version of the pigeonhole principle. The point is to illustrate how one can extract witnesses from proofs that use classical logic and countable choice.

(We don't use the Agda libraries, and hence this set of Agda files is self-contained.)

Martin Escardo
m.escardo@cs.bham.ac.uk