Martin Escardo, November-December 2019

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Fin.Pigeonhole where


open import Factorial.Swap
open import Fin.Bishop
open import Fin.Choice
open import Fin.Embeddings
open import Fin.Order
open import Fin.Topology
open import Fin.Type
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import Naturals.Order
open import Notation.Order
open import NotionsOfDecidability.Complemented
open import NotionsOfDecidability.Decidable
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.FunExt
open import UF.LeftCancellable
open import UF.PropTrunc

\end{code}

Recall that X ↣ Y is the type of left cancellable maps from X to Y,
which should not be confused with the type X β†ͺ Y of embeddings of X
into Y. However, for types that are sets, like Fin n, there is no
difference between the embedding property and left cancellability.

\begin{code}

+πŸ™-cancel-lemma : {X Y : 𝓀 Μ‡ }
                β†’ (𝒇 : X + πŸ™ ↣ Y + πŸ™)
                β†’ ⌈ 𝒇 βŒ‰ 𝟎 ＝ 𝟎
                β†’ X ↣ Y

+πŸ™-cancel-lemma {𝓀} {X} {Y} (f , l) p = g , m
 where
  g : X β†’ Y
  g x = pr₁ (inl-preservation {𝓀} {𝓀} {𝓀} {𝓀} f p l x)

  a : (x : X) β†’ f (suc x) ＝ suc (g x)
  a x = prβ‚‚ (inl-preservation f p l x)

  m : left-cancellable g
  m {x} {x'} p = q
   where
    r = f (suc x)  ＝⟨ a x ⟩
        suc (g x)  ＝⟨ ap suc p ⟩
        suc (g x') ＝⟨ (a x')⁻¹ ⟩
        f (suc x') ∎

    q : x ＝ x'
    q = inl-lc (l r)


+πŸ™-cancel : {X Y : 𝓀 Μ‡ }
          β†’ is-discrete Y
          β†’ X + πŸ™ ↣ Y + πŸ™
          β†’ X ↣ Y

+πŸ™-cancel {𝓀} {X} {Y} i (f , e) = a
 where
  h : Y + πŸ™ β†’ Y + πŸ™
  h = swap (f 𝟎) 𝟎 (+-is-discrete i πŸ™-is-discrete (f 𝟎)) new-point-is-isolated

  d : left-cancellable h
  d = equivs-are-lc h (swap-is-equiv (f 𝟎) 𝟎 (+-is-discrete i πŸ™-is-discrete (f 𝟎)) new-point-is-isolated)

  f' : X + πŸ™ β†’ Y + πŸ™
  f' = h ∘ f

  e' : left-cancellable f'
  e' = left-cancellable-closed-under-∘ f h e d

  p : f' 𝟎 ＝ 𝟎
  p = swap-equationβ‚€ (f 𝟎) 𝟎 (+-is-discrete i πŸ™-is-discrete (f 𝟎)) new-point-is-isolated

  a : X ↣ Y
  a = +πŸ™-cancel-lemma (f' , e') p

\end{code}

In set theory, natural numbers are defined as certain sets, and their
order relation is inherited from the ordering of sets defined by the
existence of injections, or left-cancellable maps. Here, in type
theory, we have defined m ≀ n by induction on m and n, in the style of
Peano Arithmetic, but we can prove that this relation is characterized
by this injection property:

\begin{code}

↣-gives-≀ : (m n : β„•) β†’ (Fin m ↣ Fin n) β†’ m ≀ n
↣-gives-≀ 0        n        e       = zero-least n
↣-gives-≀ (succ m) 0        (f , i) = 𝟘-elim (f 𝟎)
↣-gives-≀ (succ m) (succ n) e       = ↣-gives-≀ m n (+πŸ™-cancel Fin-is-discrete e)


canonical-Fin-inclusion : (m n : β„•) β†’ m ≀ n β†’ (Fin m β†’ Fin n)
canonical-Fin-inclusion 0        n        l = unique-from-𝟘
canonical-Fin-inclusion (succ m) 0        l = 𝟘-elim l
canonical-Fin-inclusion (succ m) (succ n) l = +functor IH unique-to-πŸ™
 where
  IH : Fin m β†’ Fin n
  IH = canonical-Fin-inclusion m n l


canonical-Fin-inclusion-lc : (m n : β„•) (l : m ≀ n)
                           β†’ left-cancellable (canonical-Fin-inclusion m n l)

canonical-Fin-inclusion-lc 0        n        l {x}     {y}     p = 𝟘-elim x
canonical-Fin-inclusion-lc (succ m) 0        l {x}     {y}     p = 𝟘-elim l
canonical-Fin-inclusion-lc (succ m) (succ n) l {suc x} {suc y} p = Ξ³
 where
  IH : canonical-Fin-inclusion m n l x ＝ canonical-Fin-inclusion m n l y β†’ x ＝ y
  IH = canonical-Fin-inclusion-lc m n l

  γ : suc x ＝ suc y
  Ξ³ = ap suc (IH (inl-lc p))

canonical-Fin-inclusion-lc (succ m) (succ n) l {𝟎} {𝟎} p = refl


≀-gives-↣ : (m n : β„•) β†’ m ≀ n β†’ (Fin m ↣ Fin n)
≀-gives-↣ m n l = canonical-Fin-inclusion m n l , canonical-Fin-inclusion-lc m n l

\end{code}

An equivalent, shorter construction:

\begin{code}
≀-gives-↣' : (m n : β„•) β†’ m ≀ n β†’ (Fin m ↣ Fin n)
≀-gives-↣' 0        n        l = unique-from-𝟘 , (Ξ» {x} {x'} p β†’ 𝟘-elim x)
≀-gives-↣' (succ m) 0        l = 𝟘-elim l
≀-gives-↣' (succ m) (succ n) l = g , j
 where
  IH : Fin m ↣ Fin n
  IH = ≀-gives-↣' m n l

  f : Fin m β†’ Fin n
  f = pr₁ IH

  i : left-cancellable f
  i = prβ‚‚ IH

  g : Fin (succ m) β†’ Fin (succ n)
  g = +functor f unique-to-πŸ™

  j : left-cancellable g
  j {suc x} {suc x'} p = ap suc (i (inl-lc p))
  j {suc x} {𝟎}      p = 𝟘-elim (+disjoint  p)
  j {𝟎}     {suc y}  p = 𝟘-elim (+disjoint' p)
  j {𝟎}     {𝟎}      p = refl

\end{code}

Added 9th December 2019. A version of the pigeonhole principle, which
uses (one direction of) the above characterization of the relation m ≀ n
as the existence of an injection Fin m β†’ Fin n:

\begin{code}

_has-a-repetition : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
f has-a-repetition = Ξ£ x κž‰ domain f , Ξ£ x' κž‰ domain f , (x β‰  x') Γ— (f x ＝ f x')

pigeonhole-principle : (m n : β„•) (f : Fin m β†’ Fin n)
                     β†’ m > n β†’ f has-a-repetition
pigeonhole-principle m n f g = Ξ³
 where
  a : Β¬ (Ξ£ f κž‰ (Fin m β†’ Fin n), left-cancellable f)
  a = contrapositive (↣-gives-≀ m n) (less-not-bigger-or-equal n m g)

  b : Β¬ left-cancellable f
  b l = a (f , l)

  c : Β¬ ((i j : Fin m) β†’ f i ＝ f j β†’ i ＝ j)
  c Ο† = b (Ξ» {i} {j} β†’ Ο† i j)

  d : ¬¬ (f has-a-repetition)
  d ψ = c δ
   where
    Ξ΅ : (i j : Fin m) β†’ f i ＝ f j β†’ Β¬ (i β‰  j)
    Ρ i j p ν = ψ (i , j , ν , p)

    Ξ΄ : (i j : Fin m) β†’ f i ＝ f j β†’ i ＝ j
    δ i j p = ¬¬-elim (Fin-is-discrete i j) (Ρ i j p)

\end{code}

A classical proof ends at this point. For a constructive proof, we
need more steps.

\begin{code}

  u : (i j : Fin m) β†’ is-decidable ((i β‰  j) Γ— (f i ＝ f j))
  u i j = Γ—-preserves-decidability
           (Β¬-preserves-decidability (Fin-is-discrete i j))
           (Fin-is-discrete (f i) (f j))

  v : (i : Fin m) β†’ is-decidable (Ξ£ j κž‰ Fin m , (i β‰  j) Γ— (f i ＝ f j))
  v i = Fin-Compact _ (u i)

  w : is-decidable (f has-a-repetition)
  w = Fin-Compact _ v

  Ξ³ : f has-a-repetition
  γ = ¬¬-elim w d

\end{code}

This, of course, doesn't give the most efficient algorithm, but it
does give an algorithm for computing an argument of the function whose
value is repeated.

Example. The pigeonhole principle holds for finite types in the
following form:

\begin{code}

module _ (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt
 open finiteness pt

 finite-pigeonhole-principle : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                               (Ο† : is-finite X) (ψ : is-finite Y)
                             β†’ cardinality X Ο† > cardinality Y ψ
                             β†’ βˆ₯ f has-a-repetition βˆ₯

 finite-pigeonhole-principle {𝓀} {π“₯} {X} {Y} f (m , s) (n , t) b = Ξ³
  where
   h : Fin m ≃ X β†’ Y ≃ Fin n β†’ f has-a-repetition
   h (g , d) (h , e) = r r'
    where
     f' : Fin m β†’ Fin n
     f' = h ∘ f ∘ g

     r' : f' has-a-repetition
     r' = pigeonhole-principle m n f' b

     r : f' has-a-repetition β†’ f has-a-repetition
     r (i , j , u , p) = g i , g j , u' , p'
      where
       u' : g i β‰  g j
       u' = contrapositive (equivs-are-lc g d) u

       p' : f (g i) ＝ f (g j)
       p' = equivs-are-lc h e p

   Ξ³ : βˆ₯ f has-a-repetition βˆ₯
   Ξ³ = βˆ₯βˆ₯-functorβ‚‚ h (βˆ₯βˆ₯-functor ≃-sym s) t

\end{code}

We now assume function extensionality for a while:

\begin{code}

 module _ (fe : FunExt) where

\end{code}

We now consider further variations of the finite pigeonhole principle.

\begin{code}

  repeated-values : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ X β†’ 𝓀 βŠ” π“₯ Μ‡
  repeated-values f = Ξ» x β†’ Ξ£ x' κž‰ domain f , (x β‰  x') Γ— (f x ＝ f x')

  repetitions-complemented : {m : β„•} {Y : π“₯ Μ‡ } (f : Fin m β†’ Y)
                         β†’ is-finite Y
                         β†’ is-complemented (repeated-values f)

  repetitions-complemented {π“₯} {m} {Y} f (n , t) i =
   Fin-Compact
    (Ξ» j β†’ (i β‰  j) Γ— (f i ＝ f j))
    (Ξ» j β†’ Γ—-preserves-decidability
            (Β¬-preserves-decidability (Fin-is-discrete i j))
            (finite-types-are-discrete pt fe (n , t) (f i) (f j)))

  finite-pigeonhole-principle' : {m : β„•} {Y : π“₯ Μ‡ } (f : Fin m β†’ Y)
                                 (ψ : is-finite Y)
                               β†’ m > cardinality Y ψ
                               β†’ f has-a-repetition

  finite-pigeonhole-principle' {π“₯} {m} {Y} f (n , t) b = Ξ³
   where
    h : Y ≃ Fin n β†’ f has-a-repetition
    h (h , e) = r r'
     where
      f' : Fin m β†’ Fin n
      f' = h ∘ f

      r' : f' has-a-repetition
      r' = pigeonhole-principle m n f' b

      r : f' has-a-repetition β†’ f has-a-repetition
      r (i , j , u , p) = i , j , u , equivs-are-lc h e p

    Ξ³' : βˆ₯ f has-a-repetition βˆ₯
    Ξ³' = βˆ₯βˆ₯-functor h t

    A : Fin m β†’ π“₯ Μ‡
    A i = Ξ£ j κž‰ Fin m , (i β‰  j) Γ— (f i ＝ f j)

    Ξ³ : f has-a-repetition
    Ξ³ = Fin-Ξ£-from-βˆƒ pt fe {m} A (repetitions-complemented f (n , t)) Ξ³'

\end{code}

We can easily derive the construction finite-pigeonhole-principle from
finite-pigeonhole-principle', but at the expense of function
extensionality, which was not needed in our original construction.

Further versions of the pigeonhole principle are the following.

\begin{code}

  finite-pigeonhole-principle'' : {m : β„•} {Y : π“₯ Μ‡ } (f : Fin m β†’ Y)
                                  (Ο† : is-finite Y)
                                β†’ m > cardinality Y Ο†
                                β†’ Ξ£-min Ξ»(i : Fin m) β†’ repeated-values f i

  finite-pigeonhole-principle'' {π“₯} {m} {Y} f Ο† g =
   Ξ£-gives-Ξ£-min
    (repeated-values f)
    (repetitions-complemented f Ο†)
    (finite-pigeonhole-principle' f Ο† g)

  β„•-finite-pigeonhole-principle : {Y : π“₯ Μ‡ } (f : β„• β†’ Y)
                                β†’ is-finite Y
                                β†’ f has-a-repetition

  β„•-finite-pigeonhole-principle {π“₯} {Y} f (m , t) = r r'
   where
    f' : Fin (succ m) β†’ Y
    f' i = f (⟦_⟧ i)

    r' : f' has-a-repetition
    r' = finite-pigeonhole-principle' f'(m , t) (<-succ m)

    r : f' has-a-repetition β†’ f has-a-repetition
    r (i , j , u , p) = ⟦_⟧ i , ⟦_⟧ j , contrapositive (⟦_⟧-lc (succ m)) u , p

\end{code}

Added 13th December 2019.

A well-known application of the pigeonhole principle is that every
element has a (least) finite order in a finite group. This holds
more generally for any finite type equipped with a left-cancellable
binary operation _Β·_ and a distinguished element e, with the same
construction.

\begin{code}

  module _ {X : 𝓀 Μ‡ }
           (Ο† : is-finite X)
           (_Β·_ : X β†’ X β†’ X)
           (lc : (x : X) β†’ left-cancellable (x Β·_))
           (e : X)
         where

    _↑_ : X β†’ β„• β†’ X
    x ↑ 0        = e
    x ↑ (succ n) = x Β· (x ↑ n)

    infixl 3 _↑_

    finite-order : (x : X) β†’ Ξ£ k κž‰ β„• , x ↑ (succ k) ＝ e
    finite-order x = c a
     where
      a : Ξ£ m κž‰ β„• , Ξ£ n κž‰ β„• , (m β‰  n) Γ— (x ↑ m ＝ x ↑ n)
      a = β„•-finite-pigeonhole-principle (x ↑_) Ο†

      b : (m : β„•) (n : β„•) β†’ m β‰  n β†’ x ↑ m ＝ x ↑ n β†’ Ξ£ k κž‰ β„• , x ↑ (succ k) ＝ e
      b 0        0        ν p = 𝟘-elim (ν refl)
      b 0        (succ n) ν p = n , (p ⁻¹)
      b (succ m) 0        Ξ½ p = m , p
      b (succ m) (succ n) Ξ½ p = b m n (Ξ» (q : m ＝ n) β†’ Ξ½ (ap succ q)) (lc x p)

      c : type-of a β†’ Ξ£ k κž‰ β„• , x ↑ (succ k) ＝ e
      c (m , n , Ξ½ , p) = b m n Ξ½ p

\end{code}

And of course then there is a least such k, by bounded minimization,
because finite types are discrete:

\begin{code}

    least-finite-order : (x : X) β†’ Σμ Ξ»(k : β„•) β†’ x ↑ (succ k) ＝ e
    least-finite-order x = least-from-given A Ξ³ (finite-order x)
     where
      A : β„• β†’ 𝓀 Μ‡
      A n = x ↑ (succ n) ＝ e

      Ξ³ : (n : β„•) β†’ is-decidable (x ↑ succ n ＝ e)
      Ξ³ n = finite-types-are-discrete pt fe Ο† (x ↑ succ n) e

\end{code}

Remark: the given construction finite-order already produces the
least order, but it seems slightly more difficult to prove this than
just compute the least order from any order. If we were interested
in the efficiency of our constructions (Agda constructions are
functional programs!), we would have to consider this.