a^n b^n is not regular

This file proves that the language {aⁿbⁿ | n ∈ ℕ} (encoded with false = a, true = b) is not regular, using the Myhill–Nerode theorem: it is shown to have infinitely many distinct left quotients, hence is not regular.

Main declarations

• anbn_not_isRegular — Proof that anbn is not regular.
• map_anbn_not_isRegular — Injective alphabet maps preserve the nonregularity of anbn.

theorem anbn_leftQuotient_replicate_false (k : ℕ) : List.replicate k true ∈ anbn.leftQuotient (List.replicate k false)

Left quotient of anbn by replicate k false contains replicate k true.

theorem anbn_leftQuotient_replicate_false_ne {k j : ℕ} (hjk : j ≠ k) : List.replicate j true ∉ anbn.leftQuotient (List.replicate k false)

Left quotient of anbn by replicate k false does NOT contain replicate j true when j ≠ k.

theorem anbn_leftQuotient_injective : Function.Injective fun (k : ℕ) => anbn.leftQuotient (List.replicate k false)

The left quotients of anbn indexed by replicate k false are pairwise distinct.

theorem anbn_leftQuotient_range_infinite : ¬(Set.range anbn.leftQuotient).Finite

The range of left quotients of anbn is infinite.

theorem anbn_not_isRegular : ¬anbn.IsRegular

The language {aⁿbⁿ} is not regular.

theorem map_anbn_not_isRegular {T : Type u_1} {f : Bool → T} (hf : Function.Injective f) : ¬((Language.map f) anbn).IsRegular

Injective alphabet maps preserve the nonregularity of the anbn witness.