[ new ] Proof of the pigeonhole principle

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`:

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