[ refactor ] application, and perhaps even proof, of `Data.Fin.Properties.pigeonhole`?

[jamesmckinna]

Currently, we have

agda-stdlib/src/Data/Fin/Properties.agda

Lines 1006 to 1023 in 9fca9dc

	pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j × f i ≡ f j
	pigeonhole z<s f = contradiction (f zero) λ()
	pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
	... | yes (j , f₀≡fⱼ) = zero , suc j , z<s , f₀≡fⱼ
	... | no f₀≢fₖ
	with i , j , i<j , fᵢ≡fⱼ ← pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
	= suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
	injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
	injective⇒≤ {zero} {_} {f} _ = z≤n
	injective⇒≤ {suc _} {zero} {f} _ = contradiction (f zero) ¬Fin0
	injective⇒≤ {suc _} {suc _} {f} inj = s≤s (injective⇒≤ (λ eq →
	suc-injective (inj (punchOut-injective
	(contraInjective inj 0≢1+n)
	(contraInjective inj 0≢1+n) eq))))
	<⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f)
	<⇒notInjective n<m inj = ℕ.≤⇒≯ (injective⇒≤ inj) n<m

Regarding the two lemmas which follow pigeonhole, we have:

• injective⇒≤ proved by a separate (and complicatedly contraPositive) argument from that of pigeonhole, despite (essentially) recapiltulating the same/similar call-pattern
• from which <⇒notInjective then follows by (another contrapositive heavy!) application of ℕ.≤⇒≯

By contrast, we could reorder the lemmas so that the second follows as an immediate corollary:

• <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f)
  <⇒notInjective {f = f} n<m inj = let i , j , i<j , fᵢ≡fⱼ = pigeonhole n<m f in <-irrefl (inj fᵢ≡fⱼ) i<j

• followed by the 'opposite' contrapositive argument for the first

  injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
  injective⇒≤ = ℕ.≮⇒≥ ∘ flip <⇒notInjective

Regarding the proof of pigeonhole itself (the present version is merely a cosmetic refactoring of @MatthewDaggitt 's original in #387 ), there is (still, to my mind) something strange about the argument: namely that the argument in the second no branch makes a recursive call on pigeonhole m<n, but now with a function which has no relation to the original f... (except perhaps indirectly via f₀≢fₖ). How is this possible? Can this be simplified further?

[JacquesCarette]

I agree that refactoring the two lemmas that follow is a good idea.

Note that the recursive call is, in a very hidden way, about f ! It 'punches out' a part of f's codomain. You have to delta-expand quite a lot to see this.

An old agda proof by Dan Doel is interesting because, if you unwind it enough, you see that punchOut is also key there too! (Different name, different set-up, same 'function').

[jamesmckinna]

Thanks @JacquesCarette , closing now, but may post refactoring PR for the first part.