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 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}