The "MI to MU" puzzle from GEB

MIU.agda

module MIU where

data Symbol : Set where
  I : Symbol
  U : Symbol

open import Data.List

Word : Set
Word = List Symbol

data M : Word → Set where
  MI : M [ I ]
  MxI→MxIU : ∀ {w} → (MxI : M (w ++ [ I ])) → M (w ++ I ∷ U ∷ [])
  Mx→Mxx : ∀ {w} → (Mw : M w) → M (w ++ w)
  III→U : ∀ {w w′} → (MwIIIw′ : M (w ++ (I ∷ I ∷ I ∷ w′))) → M (w ++ (U ∷ w′))
  UU→ε : ∀ {w w′} → (MwUUw : M (w ++ (U ∷ U ∷ w′))) → M (w ++ w′)

open import Data.Nat
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

countI : Word → ℕ
countI [] = 0
countI (I ∷ w) = suc (countI w)
countI (U ∷ w) = countI w

countI-++ : ∀ w w′ → countI (w ++ w′) ≡ countI w + countI w′
countI-++ [] w′ = P.refl
countI-++ (I ∷ w) w′ = P.cong suc (countI-++ w w′)
countI-++ (U ∷ w) w′ = countI-++ w w′

countI-wU : ∀ w → countI (w ++ I ∷ U ∷ []) ≡ countI (w ++ [ I ])
countI-wU [] = P.refl
countI-wU (I ∷ w) = P.cong suc (countI-wU w)
countI-wU (U ∷ w) = countI-wU w

countI-wUw′ : ∀ w w′ → countI (w ++ w′) ≡ countI (w ++ U ∷ w′)
countI-wUw′ [] w′ = P.refl
countI-wUw′ (I ∷ w) w′ = P.cong suc (countI-wUw′ w w′)
countI-wUw′ (U ∷ w) w′ = countI-wUw′ w w′

countI-wIw′ : ∀ w w′ → countI (w ++ I ∷ w′) ≡ suc (countI (w ++ w′))
countI-wIw′ [] w′ = P.refl
countI-wIw′ (I ∷ w) w′ = P.cong suc (countI-wIw′ w w′)
countI-wIw′ (U ∷ w) w′ = countI-wIw′ w w′

open import Data.Nat.Divisibility
open import Function

lem : ∀ x → 3 ∣ x + x → 3 ∣ x
lem x = coprime-divisor 3-coprime-2 ∘ P.subst (_∣_ 3) x+x≡2*x
  where
  open import Data.Nat.Properties as Nat
  open import Algebra
  open import Data.Product
  module CS = CommutativeSemiring Nat.commutativeSemiring

  x+x≡2*x : x + x ≡ 2 * x
  x+x≡2*x = P.cong (_+_ x) (P.sym (proj₂ CS.+-identity x))

  open import Data.Nat.Coprimality

  3-coprime-2 : Coprime 3 2
  3-coprime-2 = prime⇒coprime _ 3-prime 2 (s≤s z≤n) (s≤s (s≤s (s≤s z≤n)))
    where
    open import Data.Nat.Primality
    open import Relation.Nullary.Decidable

    3-prime : Prime 3
    3-prime = from-yes (prime? 3)

inv : ∀ {w} → M w → ¬ 3 ∣ countI w
inv MI = 3∤1
  where
  3∤1 : ¬ 3 ∣ 1
  3∤1 (divides zero ())
  3∤1 (divides (suc q) ())
inv (MxI→MxIU {w} MxI) = inv MxI ∘ P.subst (_∣_ 3) (countI-wU w)
inv (Mx→Mxx {w} Mw) = inv Mw ∘ lem (countI w) ∘ P.subst (_∣_ 3) (countI-++ w w)
inv (III→U {w} {w′} MwIIIw) = inv MwIIIw ∘ 3∣wIIIw′ ∘ 3∣ww′
  where
  3∣ww′ : 3 ∣ countI (w ++ U ∷ w′) → 3 ∣ countI (w ++ w′)
  3∣ww′ = P.subst (_∣_ 3) (P.sym (countI-wUw′ w w′))

  3∣wIIIw′ : 3 ∣ countI (w ++ w′) → 3 ∣ countI (w ++ I ∷ I ∷ I ∷ w′)
  3∣wIIIw′ (divides q eq) = divides (suc q) $
    begin
      countI (w ++ I ∷ I ∷ I ∷ w′)
    ≡⟨ countI-wIw′ w (I ∷ I ∷ w′) ⟩
      suc (countI (w ++ I ∷ I ∷ w′))
    ≡⟨ P.cong (_+_ 1) (countI-wIw′ w (I ∷ w′)) ⟩
      suc (suc (countI (w ++ I ∷ w′)))
    ≡⟨ P.cong (_+_ 2) (countI-wIw′ w w′) ⟩
      suc (suc (suc (countI (w ++ w′))))
    ≡⟨ P.cong (_+_ 3) eq ⟩
      suc (suc (suc (q * 3)))
    ∎
    where
    open P.≡-Reasoning
inv (UU→ε {w} {w′} MwUUw′) = inv MwUUw′ ∘ 3∣wUUw′
  where
  3∣wUUw′ : 3 ∣ countI (w ++ w′) → 3 ∣ countI (w ++ U ∷ U ∷ w′)
  3∣wUUw′ = P.subst (_∣_ 3) (countI-wUw′ w w′ ⟨ P.trans ⟩ countI-wUw′ w (U ∷ w′))

¬MU : ¬ M [ U ]
¬MU = λ mu → inv mu (3 ∣0)