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
- miu.count_equiv_or_equiv_two_mul_mod3 st en = let a : ℕ := list.count miu.miu_atom.I st, b : ℕ := list.count miu.miu_atom.I en in b ≡ a [MOD 3] ∨ b ≡ 2 * a [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.
goodm xs holds if xs : miustr begins with M and has no M in its tail.
Equations
- miu.goodm xs = (list.head xs = miu.miu_atom.M ∧ miu.miu_atom.M ∉ list.tail xs)
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.
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.miu_atom.I en % 3 = 1 ∨ list.count miu.miu_atom.I en % 3 = 2))
Instances for miu.decstr
Suppose en : miustr. If en is derivable, then the condition decstr en holds.