{-# OPTIONS --safe #-}

module Problem16 where

open import Data.Fin
open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Properties using (0≢1+n)
open import Data.Fin.Properties
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Function

variable n : ℕ

open ≡-Reasoning

Inj : (Fin n → Fin n) → Set
Inj f = ∀ i j → f i ≡ f j → i ≡ j

Sur : (Fin n → Fin n) → Set
Sur f = ∀ x → ∃[ y ] f y ≡ x

goal : ∀ n (f : Fin n → Fin n) → Inj f → Sur f
goal (suc n) f inj x with f zero ≟ x
... | yes prf = zero , prf
... | no f0≢x =
  let (z , prf) = goal n f′ f′-inj (punchOut f0≢x) in
  suc z ,
  (begin
    f (suc z)                                 ≡˘⟨ punchIn-punchOut (f0≢f[1+i] z) ⟩
    punchIn (f zero) (punchOut (f0≢f[1+i] z)) ≡⟨ cong (punchIn (f zero)) prf ⟩
    punchIn (f zero) (punchOut (f0≢x))        ≡⟨ punchIn-punchOut f0≢x ⟩
    x                                         ∎)
  where
  f0≢f[1+i] : ∀ i → f zero ≢ f (suc i)
  f0≢f[1+i] i prf = 0≢1+n (cong toℕ (inj zero (suc i) prf))

  f′ : Fin n → Fin n
  f′ = punchOut ∘ f0≢f[1+i]

  f′-inj : Inj f′
  f′-inj i j prf =
    suc-injective $′
    inj (suc i) (suc j) $′
    punchOut-injective (f0≢f[1+i] i) (f0≢f[1+i] j) prf