Advent of proof submissions.HEADmaster

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

1 files changed, 87 insertions, 0 deletions

diff --git a/src/Problem1.agda b/src/Problem1.agda
new file mode 100644
index 0000000..3aab789
--- /dev/null
+++ b/src/Problem1.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --safe #-}
+
+module Problem1 where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality
+
+open ≡-Reasoning
+
+data 𝔹 : Set where
+    T F : 𝔹
+
+iterate : (n : ℕ) (f : 𝔹 → 𝔹) (x : 𝔹) → 𝔹
+iterate zero f x = x
+iterate (suc n) f x = f (iterate n f x)
+
+twice = iterate (suc (suc zero))
+
+-- There are exactly four functions 𝔹 → 𝔹: the two constant functions, the
+-- identiy and the inversion.
+--
+-- We can decide (extensionally) which function we have.
+
+data OneOf (f : 𝔹 → 𝔹) : Set where
+  is-const : (∀ x y → f x ≡ f y) → OneOf f
+  is-id    : (∀ x → f x ≡ x) → OneOf f
+  is-not   : f T ≡ F → f F ≡ T → OneOf f
+
+which-one? : (f : 𝔹 → 𝔹) → OneOf f
+which-one? f with f T in prfT | f F in prfF
+... | T | T = is-const λ
+  { T T → refl
+  ; T F → begin
+    f T ≡⟨ prfT ⟩
+    T   ≡⟨ sym prfF ⟩
+    f F ∎
+  ; F T → begin
+    f F ≡⟨ prfF ⟩
+    T   ≡⟨ sym prfT ⟩
+    f T ∎
+  ; F F → refl
+  }
+... | T | F = is-id    λ { T → prfT ; F → prfF }
+... | F | T = is-not   prfT prfF
+... | F | F = is-const λ
+  { T T → refl
+  ; T F → begin
+    f T ≡⟨ prfT ⟩
+    F   ≡⟨ sym prfF ⟩
+    f F ∎
+  ; F T → begin
+    f F ≡⟨ prfF ⟩
+    F   ≡⟨ sym prfT ⟩
+    f T ∎
+  ; F F → refl
+  }
+
+-- First, we show that applying a function thrice is equal to a single
+-- application. We do this by splitting on the exact function.
+
+thrice-is-once : (f : 𝔹 → 𝔹) → iterate 3 f ≗ f
+thrice-is-once f with which-one? f
+... | is-const prf = λ b → prf (f (f b)) b
+... | is-id    prf = λ b →
+  begin
+    f (f (f b)) ≡⟨ prf (f (f b)) ⟩
+    f (f b)     ≡⟨ prf (f b) ⟩
+    f b         ∎
+... | is-not   prfT prfF = λ
+  { T → begin
+    f (f (f T)) ≡⟨ cong (twice f) prfT ⟩
+    f (f F)     ≡⟨ cong f prfF ⟩
+    f T         ∎
+  ; F → begin
+    f (f (f F)) ≡⟨ cong (twice f) prfF ⟩
+    f (f T)     ≡⟨ cong f prfT ⟩
+    f F         ∎
+  }
+
+-- We prove the theorem by induction on n.
+
+goal : ∀ (f : 𝔹 → 𝔹) (b : 𝔹) (n : ℕ) → iterate n (twice f) (f b) ≡ f b
+goal f b zero    = refl
+goal f b (suc n) = begin
+  f (f (iterate n (twice f) (f b))) ≡⟨ cong (twice f) (goal f b n) ⟩
+  f (f (f b))                       ≡⟨ thrice-is-once f b ⟩
+  f b                               ∎