Decision procedure - sufficient condition and decidability #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We give a sufficient condition for a string to be derivable in the MIU language. Together with the
necessary condition, we use this to prove that derivable is an instance of decidable_pred.
Let count I st and count U st denote the number of Is (respectively Us) in st : miustr.
We'll show that st is derivable if it has the form M::x where x is a string of Is and Us
for which count I x is congruent to 1 or 2 modulo 3.
To prove this, it suffices to show derivable M::y where y is any miustr consisting only of
Is such that the number of Is in y is a+3b, where a = count I x and b = count U x.
This suffices because Rule 3 permits us to change any string of three consecutive Is into a U.
As count I y = (count I x) + 3*(count U x) ≡ (count I x) [MOD 3], it suffices to show
derivable M::z where z is an miustr of Is such that count I z is congruent to
1 or 2 modulo 3.
Let z be such an miustr and let c denote count I z, so c ≡ 1 or 2 [MOD 3].
To derive such an miustr, it suffices to derive an miustr M::w, where again w is an
miustr of only Is with the additional conditions that count I w is a power of 2, that
count I w ≥ c and that count I w ≡ c [MOD 3].
To see that this suffices, note that we can remove triples of Is from the end of M::w,
creating Us as we go along. Once the number of Is equals m, we remove Us two at a time
until we have no Us. The only issue is that we may begin the removal process with an odd number
of Us.
Writing d = count I w, we see that this happens if and only if (d-c)/3 is odd.
In this case, we must apply Rule 1 to z, prior to removing triples of Is. We thereby
introduce an additional U and ensure that the final number of Us will be even.
Tags #
miu, decision procedure, decidability, decidable_pred, decidable
Converting Is to Us #
For any given natural number c ≡ 1 or 2 [MOD 3], we need to show that can derive an miustr
M::w where w consists only of Is, where d = count I w is a power of 2, where d ≥ c and
where d ≡ c [MOD 3].
Given the above lemmas, the desired result reduces to an arithmetic result, given in the file
arithmetic.lean.
We'll use this result to show we can derive an miustr of the form M::z where z is an string
consisting only of Is such that count I z ≡ 1 or 2 [MOD 3].
As an intermediate step, we show that derive z from zt, where t is aN miustr consisting of
an even number of Us and z is any miustr.
Any number of successive occurrences of "UU" can be removed from the end of a derivable miustr
to produce another derivable miustr.
In fine-tuning my application of simp, I issued the following commend to determine which lemmas
simp uses.
set_option trace.simplify.rewrite true
We may replace several consecutive occurrences of "III" with the same number of "U"s.
In application of the following lemma, xs will either be [] or [U].
Arithmetic #
We collect purely arithmetic lemmas: add_mod2 is used to ensure we have an even number of Us
while le_pow2_and_pow2_eq_mod3 treats the congruence condition modulo 3.
decstr is a sufficient condition #
The remainder of this file sets up the proof that dectstr en is sufficent to ensure
derivable en. Decidability of derivable en is an easy consequence.
The proof proceeds by induction on the count U of en.
We tackle first the base case of the induction. This requires auxiliary results giving
conditions under which count I ys = length ys.
If an miustr has a zero count U and contains no M, then its count I is its length.
base_case_suf is the base case of the sufficiency result.
Before continuing to the proof of the induction step, we need other auxiliary results that
relate to count U.
ind_hyp_suf is the inductive step of the sufficiency result.
der_of_decstr states that derivable en follows from decstr en.
Decidability of derivable #
Finally, we have the main result, namely that derivable is a decidable predicate.
Equations
- miu.derivable.decidable_pred = λ (en : miu.miustr), decidable_of_iff (miu.decstr en) _
By decidability, we can automatically determine whether any given miustr is derivable.