{ aⁿ bⁿ | n ≥ 0 }: a two-symbol non-regular witness language

The classical two-symbol witness language showing that the regular languages are a proper subclass of the context-free languages: aⁿbⁿ is context-free (trivially) but not regular. The non-regularity proof is the textbook Myhill–Nerode argument: distinct prefixes aⁿ give distinct left quotients of { aⁿ bⁿ }, so Set.range balancedAB.leftQuotient is infinite, contradicting Language.IsRegular.finite_range_leftQuotient.

Sibling of Linglib/Core/Computability/NonContextFree/{AnBnCn, AnBnCnDn, AmBnCmDn}.lean (those use the CFL pumping lemma to escape the context-free hierarchy; this one uses Myhill–Nerode to escape the regular hierarchy). Independent of those files — uses its own AB alphabet rather than the ThreeSymbol/FourSymbol alphabets there.

Main definitions

• AB — the two-symbol alphabet {a, b}.
• IsBalanced w — decidable predicate: w = aⁿbⁿ for n = w.length / 2.
• balancedAB : Language AB — { w | IsBalanced w }.

Main results

• replicate_a_append_replicate_b_isBalanced — witness side.
• replicate_a_append_replicate_b_not_isBalanced — anti-witness via letter-counting on both sides of the supposed decomposition.
• leftQuotient_replicate_a_injective — Myhill–Nerode separator: the test word bⁿ distinguishes left quotients by aⁿ for distinct n.
• balancedAB_not_isRegular — the headline non-regularity theorem, composing the injectivity with Set.infinite_of_injective_forall_mem
  • Language.IsRegular.finite_range_leftQuotient.

Mathlib placement

Promotable to Mathlib.Computability.NonRegular.AnBn as a sibling of the existing Mathlib.Computability.MyhillNerode machinery. The proof uses only mathlib primitives (Language.IsRegular.finite_range_leftQuotient, Set.infinite_of_injective_forall_mem, List.count_replicate, List.count_append).

inductive AB : Type

The two-symbol alphabet {a, b}.

• a : AB
• b : AB

@[implicit_reducible]

instance instDecidableEqAB : DecidableEq AB

Equations

• instDecidableEqAB x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprAB : Repr AB

Equations

• instReprAB = { reprPrec := instReprAB.repr }

def instReprAB.repr : AB → ℕ → Std.Format

Equations

• instReprAB.repr AB.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AB.a")).group prec✝
• instReprAB.repr AB.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AB.b")).group prec✝

@[implicit_reducible]

instance instFintypeAB : Fintype AB

AB has exactly two inhabitants.

Equations

• instFintypeAB = { elems := {AB.a, AB.b}, complete := instFintypeAB._proof_1 }

def IsBalanced (w : List AB) : Prop

A word over AB is balanced iff it consists of n copies of a followed by n copies of b, where n = w.length / 2. The total length of any balanced word is 2 n, so n is recoverable from the length and the equation is decidable via list equality.

Equations

• IsBalanced w = (w = List.replicate (w.length / 2) AB.a ++ List.replicate (w.length / 2) AB.b)

@[implicit_reducible]

instance instDecidablePredListABIsBalanced : DecidablePred IsBalanced

Equations

• instDecidablePredListABIsBalanced x✝ = decEq x✝ (List.replicate (x✝.length / 2) AB.a ++ List.replicate (x✝.length / 2) AB.b)

def balancedAB : Language AB

The classical non-regular language { aⁿ bⁿ | n ≥ 0 }, packaged as a Language AB.

Equations

• balancedAB = {w : List AB | IsBalanced w}

@[simp]

theorem mem_balancedAB (w : List AB) : w ∈ balancedAB ↔ IsBalanced w

theorem replicate_a_append_replicate_b_isBalanced (n : ℕ) : IsBalanced (List.replicate n AB.a ++ List.replicate n AB.b)

The witness side: aⁿ ++ bⁿ is balanced. The forward direction of the language description, packaged for use in the Myhill–Nerode distinguishing-prefix argument.

theorem replicate_a_append_replicate_b_not_isBalanced {m n : ℕ} (hmn : m ≠ n) : ¬IsBalanced (List.replicate m AB.a ++ List.replicate n AB.b)

The anti-witness side: aᵐ ++ bⁿ with m ≠ n is not balanced. The proof counts as and bs on both sides of the supposed balanced decomposition.

theorem leftQuotient_replicate_a_injective : Function.Injective fun (n : ℕ) => balancedAB.leftQuotient (List.replicate n AB.a)

The Myhill–Nerode separation: for m ≠ n, the test word bⁿ is in leftQuotient balancedAB (replicate n a) but not in leftQuotient balancedAB (replicate m a). Hence the two left quotients differ, and the map n ↦ balancedAB.leftQuotient (replicate n a) is injective.

theorem balancedAB_not_isRegular : ¬balancedAB.IsRegular

{ aⁿ bⁿ } is not regular. Classical Myhill–Nerode argument: the left quotients by aⁿ for distinct n are all distinct, so Set.range balancedAB.leftQuotient is infinite, contradicting Language.IsRegular.finite_range_leftQuotient.