Running a classical proof with choice in Agda

• 10 May 2011
• Martin Escardo
• Computation, Constructive math, Guest post, Logic, Programming, Tutorial

As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I've developed in Agda some things we've been doing together.

Using

• Berardi-Bezem-Coquand functional, or alternatively,
• Berger-Oliva modified bar recursion, or alternatively,
• Escardo-Oliva countable product of selection functions,

for giving a proof term for classical countable choice, we prove the classical infinite pigeonhole principle in Agda: every infinite boolean sequence has a constant infinite subsequence, where the existential quantification is classical (double negated).

As a corollary, we get the finite pigeonhole principle, using Friedman's trick to make the existential quantifiers intuitionistic.

This we can run, and it runs fast enough. The point is to illustrate in Agda how we can get witnesses from classical proofs that use countable choice. The finite pigeonhole principle has a simple constructive proof, of course, and hence this is really for illustration only.

The main Agda files are

• InfinitePigeon
• FinitePigeon
• Examples

These are Agda files converted to html so that you can navigate them by clicking at words to go to their definitions. A zip file with all Agda files is available. Not much more information is available here.

The three little modules that implement the Berardi-Bezem-Coquand, Berger-Oliva and Escardo-Oliva functionals disable the termination checker, but no other module does. The type of these functionals in Agda is the J-shift principle, which generalizes the double-negation shift.

Comments

Martin Escardo

12 May 2011 at 15:31

We have added a proof term for countable choice using Berger’s modified bar recursion now, and I have edited the post accordingly.

Martin Escardo

27 May 2011 at 20:42

I have added the slides of the talk given at MFPS in the link given in the post.

Neel Krishnaswami

31 May 2011 at 18:01

This was a fantastic series of tutorials, btw.