πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Pigeonhole where

The finitary pigeonhole principle

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers
open import Padova2025.ProvingBasics.Connectives.More
open import Padova2025.ProvingBasics.Termination.Ordering

The primary goal of this module is to state and give a direct proof of the finitary pigeonhole principle in the following strong form: Every vector of length succ n, consisting of elements of a type with n elements, contains duplicates. Along the way, we will also formalize results which are useful in the section on the infinite box problem (TODO link).

TODO link to other formalizations

For every natural number n, the following definition sets up the prototypical finite type Fin n of size n. Its inhabitants can be pictured as those natural numbers which are strictly less than n.

data Fin : β„• β†’ Set where
  fzero : {n : β„•} β†’ Fin (succ n)
  fsucc : {n : β„•} β†’ Fin n β†’ Fin (succ n)

fsucc-inj : {n : β„•} β†’ {x y : Fin n} β†’ fsucc x ≑ fsucc y β†’ x ≑ y
fsucc-inj {x = x} {y = y} refl = refl

toβ„• : {n : β„•} β†’ Fin n β†’ β„•
toβ„• fzero     = zero
toβ„• (fsucc x) = succ (toβ„• x)

toβ„•-injective : {n : β„•} {x y : Fin n} β†’ toβ„• x ≑ toβ„• y β†’ x ≑ y
toβ„•-injective {x = fzero}   {y = fzero}   _ = refl
toβ„•-injective {x = fsucc x} {y = fsucc y} p = cong fsucc (toβ„•-injective (succ-injective p))

toβ„•-bounded : {n : β„•} (x : Fin n) β†’ toβ„• x < n
toβ„•-bounded fzero     = s≀s z≀n
toβ„•-bounded (fsucc x) = s≀s (toβ„•-bounded x)

_≑?_ : {n : β„•} β†’ (x y : Fin n) β†’ Dec (x ≑ y)
fzero ≑? fzero = yes refl
fzero ≑? fsucc y = no Ξ» ()
fsucc x ≑? fzero = no Ξ» ()
fsucc x ≑? fsucc y with x ≑? y
... | yes p = yes (cong fsucc p)
... | no  q = no Ξ» p β†’ q (fsucc-inj p)

We can collect the image of a function Fin n β†’ A into a list:

tabulate-Fin : {A : Set} {n : β„•} β†’ (Fin n β†’ A) β†’ List A
tabulate-Fin {n = zero}   f = []
tabulate-Fin {n = succ n} f = f fzero ∷ tabulate-Fin (Ξ» x β†’ f (fsucc x))

∈-tabulate-Fin : {A : Set} {n : β„•} (f : Fin n β†’ A) (x : Fin n) β†’ f x ∈ tabulate-Fin f
∈-tabulate-Fin f fzero     = here refl
∈-tabulate-Fin f (fsucc x) = there (∈-tabulate-Fin (Ξ» y β†’ f (fsucc y)) x)

TODO finish, incorporating the work of Jacopo Piccione