is_regular_mul

theoremverified

The concatenation of two regular languages is regular.

Statement

theorem is_regular_mul {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (L1 * L2).IsRegular

Source

Sipser, Theorem 1.47

Verified

07 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 1

is_regular_iff_enfaA language is regular if and only if it is accepted by an epsilon-nondeterministic finite automaton with finitely many states.

Read back from the Lean

For any type α and any languages L1 and L2 over the alphabet α (that is, sets of lists of elements of α), if L1 is regular and L2 is regular, then their language product (concatenation) L1 * L2 is also regular.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

open Language Set

def is_regular_mul_f {α : Type*} (L2 : Language α) (p : Language α × Set (Language α)) : Language α :=
  ((p.1 * L2 : Set (List α)) ∪ (⋃₀ p.2 : Set (List α)) : Set (List α))

def is_regular_mul_S {α : Type*} (L1 L2 : Language α) (w : List α) : Set (Language α) :=
  { K | ∃ bs, (∃ u ∈ L1, u ++ bs = w) ∧ K = L2.leftQuotient bs }

lemma is_regular_mul_S_subset {α : Type*} (L1 L2 : Language α) (w : List α) :
    is_regular_mul_S L1 L2 w ⊆ range L2.leftQuotient := by
  rintro K ⟨bs, _, rfl⟩
  exact ⟨bs, rfl⟩

lemma is_regular_mul_leftQuotient_eq {α : Type*} (L1 L2 : Language α) (w : List α) :
    (L1 * L2).leftQuotient w = is_regular_mul_f L2 (L1.leftQuotient w, is_regular_mul_S L1 L2 w) := by
  ext y
  simp only [mem_leftQuotient, is_regular_mul_f, Language.mem_mul, is_regular_mul_S]
  constructor
  · intro hy
    rcases hy with ⟨u, hu, v, hv, huv⟩
    rw [List.append_eq_append_iff] at huv
    rcases huv with (⟨as, hu', hy'⟩ | ⟨bs, hw', hv'⟩)
    · right
      refine ⟨L2.leftQuotient as, ⟨as, ⟨u, hu, hu'.symm⟩, rfl⟩, ?_⟩
      show as ++ y ∈ L2
      rw [← hy']
      exact hv
    · left
      refine ⟨bs, ?_, v, hv, hv'.symm⟩
      show w ++ bs ∈ L1
      rw [← hw']
      exact hu
  · rintro (⟨as, has, v, hv, rfl⟩ | ⟨K, ⟨bs, ⟨u, hu, rfl⟩, rfl⟩, hy⟩)
    · refine ⟨w ++ as, has, v, hv, by simp [List.append_assoc]⟩
    · refine ⟨u, hu, bs ++ y, hy, by simp [List.append_assoc]⟩

/-- Regular languages are closed under concatenation. -/
theorem is_regular_mul {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (L1 * L2).IsRegular := by
  rw [Language.isRegular_iff_finite_range_leftQuotient] at h1 h2 ⊢
  have H : (is_regular_mul_f L2 '' (Set.range L1.leftQuotient ×ˢ Set.powerset (Set.range L2.leftQuotient))).Finite :=
    (h1.prod h2.powerset).image (is_regular_mul_f L2)
  refine H.subset ?_
  rintro _ ⟨w, rfl⟩
  rw [is_regular_mul_leftQuotient_eq]
  exact Set.mem_image_of_mem _ ⟨Set.mem_range_self w, is_regular_mul_S_subset L1 L2 w⟩

Discuss this result Challenge it