# 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 `M`

s, and the number of `I`

s 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:

- xI → xIU,
- Mx → Mxx,
- xIIIy → xUy,
- 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*] [AdMK17] - Douglas R Hofstadter,
*Gödel, Escher, Bach*

## Tags #

miu, derivable strings

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

- M: Miu.MiuAtom
- I: Miu.MiuAtom
- U: Miu.MiuAtom

## Instances For

## 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.

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 }

`MiuAtom.repr`

is the 'natural' function from `MiuAtom`

to `String`

.

## Equations

- Miu.MiuAtom.M.repr = "M"
- Miu.MiuAtom.I.repr = "I"
- Miu.MiuAtom.U.repr = "U"

## Instances For

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 }

## Equations

- Miu.instMembershipMiuAtomMiustr = id inferInstance

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

## Instances For

## Equations

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

In the other direction, we set up a coercion from `String`

to `Miustr`

.

## Equations

- Miu.lcharToMiustr [] = []
- Miu.lcharToMiustr ('M' :: cs) = Miu.MiuAtom.M :: Miu.lcharToMiustr cs
- Miu.lcharToMiustr ('I' :: cs) = Miu.MiuAtom.I :: Miu.lcharToMiustr cs
- Miu.lcharToMiustr ('U' :: cs) = Miu.MiuAtom.U :: Miu.lcharToMiustr cs
- Miu.lcharToMiustr (c :: cs) = []

## Instances For

## Equations

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

### Derivability #

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)