Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 46 insertions, 0 deletions

diff --git a/src/Problem16.agda b/src/Problem16.agda
new file mode 100644
index 0000000..d327602
--- /dev/null
+++ b/src/Problem16.agda
@@ -0,0 +1,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