{-# 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                               ∎