mathlib3 documentation

mathlib-archive / miu_language.decision_suf

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.

theorem miu.add_mod2 (a : ) :
(t : ), a + a % 2 = t * 2

For every a, the number a + a % 2 is even.

theorem miu.le_pow2_and_pow2_eq_mod3 (a : ) (h : a % 3 = 1 a % 3 = 2) :
(m : ), a 2 ^ m 2 ^ m % 3 = a % 3

If a is 1 or 2 modulo 3, then exists k a power of 2 for which a ≤ k and a ≡ k [MOD 3].

der_replicate_I_of_mod3 states that M::y is derivable if y is any miustr consisiting just of Is, 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 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.

theorem miu.base_case_suf (en : miu.miustr) (h : miu.decstr en) (hu : list.count miu.miu_atom.U en = 0) :

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.

theorem miu.der_of_decstr {en : miu.miustr} (h : miu.decstr en) :

der_of_decstr states that derivable en follows from decstr en.

Decidability of derivable #

@[protected, instance]

Finally, we have the main result, namely that derivable is a decidable predicate.

Equations

By decidability, we can automatically determine whether any given miustr is derivable.