Decision procedure - sufficient condition and decidability #
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
count I st and
count U st denote the number of
st : miustr.
We'll show that
st is derivable if it has the form
x is a string of
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
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
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
Is such that
count I z is congruent to
1 or 2 modulo 3.
z be such an
miustr and let
count I z, so
c ≡ 1 or 2 [MOD 3].
To derive such an
miustr, it suffices to derive an
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
Us as we go along. Once the number of
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
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.
miu, decision procedure, decidability, decidable_pred, decidable
For any given natural number
c ≡ 1 or 2 [MOD 3], we need to show that can derive an
w consists only of
d = count I w is a power of 2, where
d ≥ c and
d ≡ c [MOD 3].
Given the above lemmas, the desired result reduces to an arithmetic result, given in the file
We'll use this result to show we can derive an
miustr of the form
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
t is aN
miustr consisting of
an even number of
z is any
Any number of successive occurrences of
"UU" can be removed from the end of a
to produce another
In fine-tuning my application of
simp, I issued the following commend to determine which lemmas
set_option trace.simplify.rewrite true
We may replace several consecutive occurrences of
"III" with the same number of
In application of the following lemma,
xs will either be
We collect purely arithmetic lemmas:
add_mod2 is used to ensure we have an even number of
le_pow2_and_pow2_eq_mod3 treats the congruence condition modulo 3.
der_replicate_I_of_mod3 states that
y is any
miustr consisiting just
count I y is 1 or 2 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
We tackle first the base case of the induction. This requires auxiliary results giving
conditions under which
count I ys = length ys.
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
ind_hyp_suf is the inductive step of the sufficiency result.
der_of_decstr states that
derivable en follows from
Finally, we have the main result, namely that
derivable is a decidable predicate.
- miu.derivable.decidable_pred = λ (en : miu.miustr), decidable_of_iff (miu.decstr en) _
By decidability, we can automatically determine whether any given