blob: d327602845f44670625922a727dc384abbd714de (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
{-# 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
|
