From c5d13b732a2f71c93602f27caae58515060a519b Mon Sep 17 00:00:00 2001
From: = <matthewdaggitt@gmail.com>
Date: Sun, 15 Jul 2018 23:38:08 +0100
Subject: [PATCH] A proof of the pigeonhole principle

---
 CHANGELOG.md                 |  4 +++-
 src/Data/Fin/Properties.agda | 14 +++++++++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2f84fe2f34..9e99135450 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -196,6 +196,8 @@ Other minor additions
 * Added new proof to `Data.Fin.Properties`:
   ```agda
   toℕ-fromℕ≤″ : toℕ (fromℕ≤″ m m<n) ≡ m
+
+  pigeonhole  : m < n → (f : Fin n → Fin m) → ∃₂ λ i j → i ≢ j × f i ≡ f j
   ```
 
 * Added new proofs to `Data.List.Any.Properties`:
@@ -336,7 +338,7 @@ Other minor additions
 * Added new functions to `Level`:
   ```agda
   _ℕ+_ : Nat → Level → Level
-  #_   : Nat → Level  
+  #_   : Nat → Level
   ```
 
 * Added the following types in `Relation.Unary`:
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 4d1b4f6d85..772a42c143 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -20,7 +20,7 @@ open import Data.Nat as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_)
   )
 import Data.Nat.Properties as ℕₚ
 open import Data.Unit using (tt)
-open import Data.Product using (∃; ∄; _×_; _,_; map; proj₁)
+open import Data.Product using (∃; ∃₂; ∄; _×_; _,_; map; proj₁)
 open import Function using (_∘_; id)
 open import Function.Injection using (_↣_)
 open import Relation.Binary as B hiding (Decidable)
@@ -496,6 +496,18 @@ all? P? with decFinSubset U? (λ {f} _ → P? f)
           ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
 ¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)
 
+-- The pigeonhole principle.
+
+pigeonhole : ∀ {m n} → m ℕ.< n → (f : Fin n → Fin m) →
+             ∃₂ λ i j → i ≢ j × f i ≡ f j
+pigeonhole (s≤s z≤n)       f = contradiction (f zero) λ()
+pigeonhole (s≤s (s≤s m≤n)) f with any? (λ k → f zero ≟ f (suc k))
+... | yes (j , f₀≡fⱼ) = zero , suc j , (λ()) , f₀≡fⱼ
+... | no  f₀≢fₖ with pigeonhole (s≤s m≤n) (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
+...   | (i , j , i≢j , fᵢ≡fⱼ) =
+  suc i , suc j , i≢j ∘ suc-injective ,
+  punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
+
 ------------------------------------------------------------------------
 -- Categorical