Skip to content

Instantly share code, notes, and snippets.

@esurdam
Forked from gergoerdi/MIU.agda
Created August 3, 2016 02:05
Show Gist options
  • Save esurdam/02676cd05d13595fc40b9759e80d2372 to your computer and use it in GitHub Desktop.
Save esurdam/02676cd05d13595fc40b9759e80d2372 to your computer and use it in GitHub Desktop.
The "MI to MU" puzzle from GEB
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment