# 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 `DecidablePred`

.

Let `count I st`

and `count U st`

denote the number of `I`

s (respectively `U`

s) in `st : Miustr`

.

We'll show that `st`

is derivable if it has the form `M::x`

where `x`

is a string of `I`

s and `U`

s
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
`I`

s such that the number of `I`

s 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 `I`

s 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 `I`

s 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 `I`

s 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 `I`

s from the end of `M::w`

,
creating `U`

s as we go along. Once the number of `I`

s equals `m`

, we remove `U`

s two at a time
until we have no `U`

s. The only issue is that we may begin the removal process with an odd number
of `U`

s.

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 `I`

s. We thereby
introduce an additional `U`

and ensure that the final number of `U`

s will be even.

## Tags #

miu, decision procedure, decidability, decidable_pred, decidable

## Converting `I`

s to `U`

s #

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 `I`

s, 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 a string
consisting only of `I`

s 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 `U`

s 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 `U`

s
while `le_pow2_and_pow2_eq_mod3`

treats the congruence condition modulo 3.

`der_replicate_I_of_mod3`

states that `M::y`

is `Derivable`

if `y`

is any `Miustr`

consisiting just
of `I`

s, where `count I y`

is 1 or 2 modulo 3.

`Decstr`

is a sufficient condition #

The remainder of this file sets up the proof that `Decstr 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.

By decidability, we can automatically determine whether any given `Miustr`

is `Derivable`

.