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 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 a 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.

theorem Miu.der_of_der_append_replicate_U_even {z : Miustr} {m : ℕ} (h : Derivable (z ++ List.replicate (m * 2) MiuAtom.U)) : Derivable z

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 command to determine which lemmas simp uses.

set_option trace.simplify.rewrite true

theorem Miu.der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append (c k : ℕ) : c % 3 = 1 ∨ c % 3 = 2 → ∀ (xs : Miustr) (hder : Derivable (MiuAtom.M :: List.replicate (c + 3 * k) MiuAtom.I ++ xs)), Derivable (MiuAtom.M :: (List.replicate c MiuAtom.I ++ List.replicate k MiuAtom.U) ++ xs)

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].

theorem Miu.replicate_pow_minus_append {m : ℕ} : MiuAtom.M :: List.replicate (2 ^ m - 1) MiuAtom.I ++ [MiuAtom.I] = MiuAtom.M :: List.replicate (2 ^ m) MiuAtom.I

theorem Miu.der_replicate_I_of_mod3 (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2) : Derivable (MiuAtom.M :: List.replicate c MiuAtom.I)

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 Decstr en is sufficient 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.

theorem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : List.count MiuAtom.U ys = 0) (hm : MiuAtom.M ∉ ys) : List.count MiuAtom.I ys = List.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 : Miustr) (h : Decstr en) (hu : List.count MiuAtom.U en = 0) : Derivable en

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.mem_of_count_U_eq_succ {xs : Miustr} {k : ℕ} (h : List.count MiuAtom.U xs = k.succ) : MiuAtom.U ∈ xs

theorem Miu.eq_append_cons_U_of_count_U_pos {k : ℕ} {zs : Miustr} (h : List.count MiuAtom.U zs = k.succ) : ∃ (as : Miustr) (bs : Miustr), zs = as ++ MiuAtom.U :: bs

theorem Miu.ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : List.count MiuAtom.U ys = k.succ) (hdec : Decstr ys) : ∃ (as : Miustr) (bs : Miustr), ys = MiuAtom.M :: as ++ MiuAtom.U :: bs ∧ List.count MiuAtom.U (MiuAtom.M :: as ++ [MiuAtom.I, MiuAtom.I, MiuAtom.I] ++ bs) = k ∧ Decstr (MiuAtom.M :: as ++ [MiuAtom.I, MiuAtom.I, MiuAtom.I] ++ bs)

ind_hyp_suf is the inductive step of the sufficiency result.

theorem Miu.der_of_decstr {en : Miustr} (h : Decstr en) : Derivable en

der_of_decstr states that Derivable en follows from Decstr en.

Decidability of Derivable

instance Miu.instDecidablePredMiustrDerivable : DecidablePred Derivable

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

Equations

• Miu.instDecidablePredMiustrDerivable x✝ = decidable_of_iff (Miu.Decstr x✝) ⋯

By decidability, we can automatically determine whether any given Miustr is Derivable.