mathlib3 documentation

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.

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

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

Instances for miu.goodm

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.

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

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

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.

Instances for miu.decstr

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