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.

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.

Instances For
    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 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.

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

    Instances For

      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 together our two conditions to give one necessary condition Decstr for an Miustr to be derivable.

      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

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