An MIU Decision Procedure in Lean

The MIU formal system was introduced by Douglas Hofstadter in the first chapter of his 1979 book, Gödel, Escher, Bach. The system is defined by four rules of inference, one axiom, and an alphabet of three symbols: M, I, and U.

Hofstadter's central question is: can the string "MU" be derived?

It transpires that there is a simple decision procedure for this system. A string is derivable if and only if it starts with M, contains no other Ms, and the number of Is in the string is congruent to 1 or 2 modulo 3.

The principal aim of this project is to give a Lean proof that the derivability of a string is a decidable predicate.

The MIU System

In Hofstadter's description, an atom is any one of M, I or U. A string is a finite sequence of zero or more symbols. To simplify notation, we write a sequence [I,U,U,M], for example, as IUUM.

The four rules of inference are:

1. xI → xIU,
2. Mx → Mxx,
3. xIIIy → xUy,
4. xUUy → xy,

where the notation α → β is to be interpreted as 'if α is derivable, then β is derivable'.

Additionally, he has an axiom:

• MI is derivable.

In Lean, it is natural to treat the rules of inference and the axiom on an equal footing via an inductive data type Derivable designed so that Derivable x represents the notion that the string x can be derived from the axiom by the rules of inference. The axiom is represented as a nonrecursive constructor for Derivable. This mirrors the translation of Peano's axiom '0 is a natural number' into the nonrecursive constructor zero of the inductive type Nat.

References

• [Jeremy Avigad, Leonardo de Moura and Soonho Kong, Theorem Proving in Lean] [avigad_moura_kong-2017]
• [Douglas R Hofstadter, Gödel, Escher, Bach][Hofstadter-1979]

Tags

miu, derivable strings

Declarations and instance derivations for MiuAtom and Miustr

inductive Miu.MiuAtom : Type

The atoms of MIU can be represented as an enumerated type in Lean.

• M: Miu.MiuAtom
• I: Miu.MiuAtom
• U: Miu.MiuAtom

instance Miu.instDecidableEqMiuAtom : DecidableEq Miu.MiuAtom

Equations

• Miu.instDecidableEqMiuAtom x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

The annotation deriving DecidableEq above indicates that Lean will automatically derive that MiuAtom is an instance of DecidableEq. The use of deriving is crucial in this project and will lead to the automatic derivation of decidability.

instance Miu.miuAtomInhabited : Inhabited Miu.MiuAtom

We show that the type MiuAtom is inhabited, giving M (for no particular reason) as the default element.

Equations

• Miu.miuAtomInhabited = { default := Miu.MiuAtom.M }

def Miu.MiuAtom.repr : Miu.MiuAtom → String

MiuAtom.repr is the 'natural' function from MiuAtom to String.

Equations

• x.repr = match x with | Miu.MiuAtom.M => "M" | Miu.MiuAtom.I => "I" | Miu.MiuAtom.U => "U"

instance Miu.instReprMiuAtom : Repr Miu.MiuAtom

Using MiuAtom.repr, we prove that MiuAtom is an instance of Repr.

Equations

• Miu.instReprMiuAtom = { reprPrec := fun (u : Miu.MiuAtom) (x : ℕ) => Std.Format.text u.repr }

def Miu.Miustr : Type

For simplicity, an Miustr is just a list of elements of type MiuAtom.

Equations

• Miu.Miustr = List Miu.MiuAtom

instance Miu.instMembershipMiuAtomMiustr : Membership Miu.MiuAtom Miu.Miustr

Equations

• Miu.instMembershipMiuAtomMiustr = id inferInstance

def Miu.Miustr.mrepr : Miu.Miustr → String

For display purposes, an Miustr can be represented as a String.

Equations

• Miu.Miustr.mrepr [] = ""
• Miu.Miustr.mrepr (c :: cs) = c.repr ++ Miu.Miustr.mrepr cs

instance Miu.miurepr : Repr Miu.Miustr

Equations

• Miu.miurepr = { reprPrec := fun (u : Miu.Miustr) (x : ℕ) => Std.Format.text u.mrepr }

def Miu.lcharToMiustr : List Char → Miu.Miustr

In the other direction, we set up a coercion from String to Miustr.

Equations

• Miu.lcharToMiustr [] = []
• Miu.lcharToMiustr (c :: cs) = let ms := Miu.lcharToMiustr cs; match c with | 'M' => Miu.MiuAtom.M :: ms | 'I' => Miu.MiuAtom.I :: ms | 'U' => Miu.MiuAtom.U :: ms | x => []

instance Miu.stringCoeMiustr : Coe String Miu.Miustr

Equations

• Miu.stringCoeMiustr = { coe := fun (st : String) => Miu.lcharToMiustr st.data }

Derivability

inductive Miu.Derivable : Miu.Miustr → Prop

The inductive type Derivable has five constructors. The nonrecursive constructor mk corresponds to Hofstadter's axiom that "MI" is derivable. Each of the constructors r1, r2, r3, r4 corresponds to the one of Hofstadter's rules of inference.

• mk: Miu.Derivable (Miu.lcharToMiustr "MI".data)
• r1: ∀ {x : Miu.Miustr}, Miu.Derivable (x ++ [Miu.MiuAtom.I]) → Miu.Derivable (x ++ [Miu.MiuAtom.I, Miu.MiuAtom.U])
• r2: ∀ {x : List Miu.MiuAtom}, Miu.Derivable (Miu.MiuAtom.M :: x) → Miu.Derivable (Miu.MiuAtom.M :: x ++ x)
• r3: ∀ {x y : Miu.Miustr}, Miu.Derivable (x ++ [Miu.MiuAtom.I, Miu.MiuAtom.I, Miu.MiuAtom.I] ++ y) → Miu.Derivable (x ++ Miu.MiuAtom.U :: y)
• r4: ∀ {x y : Miu.Miustr}, Miu.Derivable (x ++ [Miu.MiuAtom.U, Miu.MiuAtom.U] ++ y) → Miu.Derivable (x ++ y)

Rule usage examples

Derivability examples