Martin Escardo and Paulo Oliva 2011

\begin{code}

{-# OPTIONS --without-K #-}

module InfinitePigeon.PigeonProgram where

open import InfinitePigeon.Cantor
open import InfinitePigeon.DataStructures
open import InfinitePigeon.FinitePigeon
open import InfinitePigeon.Logic
open import InfinitePigeon.Naturals
open import InfinitePigeon.Two

\end{code}

Given an infinite boolean sequence α and a natural number m, find a
boolean b and a finite list of length n with the indices of a
finite constant subsequence of α with value b at all
positions.

This is usually how such programs are specified in functional programming (if
they are at all). Here Theorem (defined in the module
InfinitePigeon.FinitePigeon) is the program with the formal specification, also
formally checked. Once this is done we can erase the specification.

\begin{code}

pigeon-program : ₂ℕ →  ℕ  →  ₂  ×  List ℕ
pigeon-program α m = f(Theorem α m)
 where
  f : Finite-Pigeonhole α m → ₂ × List ℕ
  f (∃-intro b (∃-intro s proof)) = (b , list s)

\end{code}