# mathlib3documentation

mathlib-archive / miu_language.decision_nec

# Decision procedure: necessary condition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Given st en : miustr, the relation count_equiv_or_equiv_two_mul_mod3 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
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.

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

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 decidable_pred, 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.

@[protected, instance]
def miu.goodm (xs : miu.miustr) :
Prop

goodm xs holds if xs : miustr begins with M and has no M in its tail.

Equations
Instances for miu.goodm
theorem miu.goodmi  :

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_rule3 (as bs : miu.miustr) (h₁ : miu.derivable ++ bs)) (h₂ : miu.goodm ++ bs)) :

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

theorem miu.goodm_of_rule4 (as bs : miu.miustr) (h₁ : miu.derivable ++ bs)) (h₂ : miu.goodm ++ bs)) :
miu.goodm (as ++ bs)

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

We put togther our two conditions to give one necessary condition decstr for an miustr to be derivable.

def miu.decstr (en : miu.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
Instances for miu.decstr
@[protected, instance]
theorem miu.decstr_of_der {en : miu.miustr} :

Suppose en : miustr. If en is derivable, then the condition decstr en holds.