[Agda] Running a classical proof with choice in Agda
Martin Escardo
m.escardo at cs.bham.ac.uk
Mon May 9 11:29:15 CEST 2011
Dear Agda- and type-theorists,
Using
* Berardi-Bezem-Coquand's functional, or alternatively
* Escardo-Oliva's 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
A-translation (by hand) 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.
This can be seen at
http://www.cs.bham.ac.uk/~mhe/pigeon/
with nice html formating of the Agda files produced by the Agda system.
The two little modules that implement the Berardi-Bezem-Coquand 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. More details in
the above web page.
Best wishes,
Martin
More information about the Agda
mailing list