Decision procedure: necessary condition

We introduce a condition Decstr and show that if a string en is Derivable, then Decstr en holds.

Using this, we give a negative answer to the question: is "MU" derivable?

Tags

miu, decision procedure

Numerical condition on the I count

Suppose st : Miustr. Then count I st is the number of Is in st. We'll show, if Derivable st, then count I st must be 1 or 2 modulo 3. To do this, it suffices to show that if the en : Miustr is derived from st, then count I en moudulo 3 is either equal to or is twice count I st, modulo 3.

def Miu.CountEquivOrEquivTwoMulMod3 (st en : Miustr) : Prop

Given st en : Miustr, the relation CountEquivOrEquivTwoMulMod3 st en holds if st and en either have equal count I, modulo 3, or count I en is twice count I st, modulo 3.

Equations

• Miu.CountEquivOrEquivTwoMulMod3 st en = (List.count Miu.MiuAtom.I en ≡ List.count Miu.MiuAtom.I st [MOD 3] ∨ List.count Miu.MiuAtom.I en ≡ 2 * List.count Miu.MiuAtom.I st [MOD 3])

theorem Miu.mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2) (h2 : b % 3 = a % 3 ∨ b % 3 = 2 * a % 3) : b % 3 = 1 ∨ b % 3 = 2

If a is 1 or 2 mod 3 and if b is a or twice a mod 3, then b is 1 or 2 mod 3.

theorem Miu.count_equiv_one_or_two_mod3_of_derivable (en : Miustr) : Derivable en → List.count MiuAtom.I en % 3 = 1 ∨ List.count MiuAtom.I en % 3 = 2

count_equiv_one_or_two_mod3_of_derivable shows any derivable string must have a count I that is 1 or 2 modulo 3.

theorem Miu.not_derivable_mu : ¬Derivable (lcharToMiustr "MU".data)

Using the above theorem, we solve the MU puzzle, showing that "MU" is not derivable. Once we have proved that Derivable is an instance of DecidablePred, this will follow immediately from dec_trivial.

Condition on M

That solves the MU puzzle, but we'll proceed by demonstrating the other necessary condition for a string to be derivable, namely that the string must start with an M and contain no M in its tail.

def Miu.Goodm (xs : Miustr) : Prop

Goodm xs holds if xs : Miustr begins with M and has no M in its tail.

Equations

• Miu.Goodm xs = (List.headI xs = Miu.MiuAtom.M ∧ Miu.MiuAtom.M ∉ List.tail xs)

instance Miu.instDecidablePredMiustrGoodm : DecidablePred Goodm

Equations

• Miu.instDecidablePredMiustrGoodm = id inferInstance

theorem Miu.goodmi : Goodm [MiuAtom.M, MiuAtom.I]

Demonstration that "MI" starts with M and has no M in its tail.

We'll show, for each i from 1 to 4, that if en follows by Rule i from st and if Goodm st holds, then so does Goodm en.

theorem Miu.goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ [MiuAtom.I])) (h₂ : Goodm (xs ++ [MiuAtom.I])) : Goodm (xs ++ [MiuAtom.I, MiuAtom.U])

theorem Miu.goodm_of_rule2 (xs : Miustr) : Derivable (MiuAtom.M :: xs) → ∀ (h₂ : Goodm (MiuAtom.M :: xs)), Goodm (MiuAtom.M :: xs ++ xs)

theorem Miu.goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [MiuAtom.I, MiuAtom.I, MiuAtom.I] ++ bs)) (h₂ : Goodm (as ++ [MiuAtom.I, MiuAtom.I, MiuAtom.I] ++ bs)) : Goodm (as ++ MiuAtom.U :: bs)

The proof of the next lemma is identical, on the tactic level, to the previous proof.

theorem Miu.goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [MiuAtom.U, MiuAtom.U] ++ bs)) (h₂ : Goodm (as ++ [MiuAtom.U, MiuAtom.U] ++ bs)) : Goodm (as ++ bs)

theorem Miu.goodm_of_derivable (en : Miustr) : Derivable en → Goodm en

Any derivable string must begin with M and have no M in its tail.

We put together our two conditions to give one necessary condition Decstr for an Miustr to be derivable.

def Miu.Decstr (en : Miustr) : Prop

Decstr en is the condition that count I en is 1 or 2 modulo 3, that en starts with M, and that en has no M in its tail. We automatically derive that this is a decidable predicate.

Equations

• Miu.Decstr en = (Miu.Goodm en ∧ (List.count Miu.MiuAtom.I en % 3 = 1 ∨ List.count Miu.MiuAtom.I en % 3 = 2))

instance Miu.instDecidablePredMiustrDecstr : DecidablePred Decstr

Equations

• Miu.instDecidablePredMiustrDecstr = id inferInstance

theorem Miu.decstr_of_der {en : Miustr} : Derivable en → Decstr en

Suppose en : Miustr. If en is Derivable, then the condition Decstr en holds.