module PigeonProgram where open import Cantor open import Naturals open import Two open import Logic open import FinitePigeon open import DataStructures -- 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. pigeon-program : ₂ℕ → ℕ → ₂ × List ℕ pigeon-program α m = f(Theorem α m) where f : Finite-Pigeonhole α m → ₂ × List ℕ f(∃-intro b (∃-intro s proof)) = (b , list s)