Kleene's theorem

30 fully proved

Kleene Converse

DefinitionLanguage denoted by a regular expression#✓fully proved

A language is denoted by a regular expression when it is r.matches' for some r.

def IsRegexDenoted (L : Language α) : Prop :=
  ∃ r : RegularExpression α, r.matches' = L

Used by 11

Used byRegex-denoted languages are closed under union · Single-letter languages are regex-denoted · DFA equation coefficients are regex-denoted · DFA equation constant terms are regex-denoted · Languages of DFAs on finitely many numbered states are regex-denoted · Solving a system of language equations · Regex-denoted languages are closed under Kleene star · Regex-denoted languages are closed under concatenation · The language of the empty word is regex-denoted · Regex-denoted languages are closed under finite unions · The empty language is regex-denoted

TheoremThe empty language is regex-denoted#✓fully proved

The empty language is denoted by 0.

theorem IsRegexDenoted.zero : IsRegexDenoted (0 : Language α)

Uses 1 · Used by 2

Statement usesLanguage denoted by a regular expression

Used byDFA equation constant terms are regex-denoted · Regex-denoted languages are closed under finite unions

TheoremThe language of the empty word is regex-denoted#✓fully proved

The language {[]} is denoted by 1.

theorem IsRegexDenoted.one : IsRegexDenoted (1 : Language α)

Uses 1 · Used by 1

Statement usesLanguage denoted by a regular expression

Used byDFA equation constant terms are regex-denoted

TheoremSingle-letter languages are regex-denoted#✓fully proved

A singleton {[a]} is denoted by char a.

theorem IsRegexDenoted.char (a : α) : IsRegexDenoted ({[a]} : Language α)

Uses 1 · Used by 1

Statement usesLanguage denoted by a regular expression

Used byDFA equation coefficients are regex-denoted

TheoremRegex-denoted languages are closed under union#✓fully proved

Denoted languages are closed under union.

theorem IsRegexDenoted.add {L K : Language α} (hL : IsRegexDenoted L) (hK : IsRegexDenoted K) :
    IsRegexDenoted (L + K)

Uses 1 · Used by 2

Statement usesLanguage denoted by a regular expression

Used bySolving a system of language equations · Regex-denoted languages are closed under finite unions

TheoremRegex-denoted languages are closed under concatenation#✓fully proved

Denoted languages are closed under concatenation.

theorem IsRegexDenoted.mul {L K : Language α} (hL : IsRegexDenoted L) (hK : IsRegexDenoted K) :
    IsRegexDenoted (L * K)

Uses 1 · Used by 1

Statement usesLanguage denoted by a regular expression

Used bySolving a system of language equations

TheoremRegex-denoted languages are closed under Kleene star#✓fully proved

Denoted languages are closed under Kleene star.

theorem IsRegexDenoted.kstar {L : Language α} (hL : IsRegexDenoted L) :
    IsRegexDenoted (L∗)

Uses 1 · Used by 1

Statement usesLanguage denoted by a regular expression

Used bySolving a system of language equations

TheoremRegex-denoted languages are closed under finite unions#✓fully proved

Denoted languages are closed under finite unions.

theorem IsRegexDenoted.sum {ι : Type*} {s : Finset ι} {f : ι → Language α}
    (h : ∀ i ∈ s, IsRegexDenoted (f i)) : IsRegexDenoted (∑ i ∈ s, f i)

Uses 3 · Used by 2

Statement usesLanguage denoted by a regular expression

Proof usesRegex-denoted languages are closed under union · The empty language is regex-denoted

Used byDFA equation coefficients are regex-denoted · Solving a system of language equations

TheoremMembership in a finite union of languages#✓fully proved

Membership in a finite union of languages.

theorem mem_sum {ι : Type*} {s : Finset ι} {f : ι → Language α} {w : List α} :
    w ∈ ∑ i ∈ s, f i ↔ ∃ i ∈ s, w ∈ f i

Used by 2

Used byEquation system satisfied by DFA state languages · Membership in a DFA equation coefficient

TheoremEmpty word outside a concatenation#✓fully proved

The empty word is not in a concatenation whose right factor excludes it.

theorem nil_notMem_mul_of_nil_notMem_right {L K : Language α} (hK : [] ∉ K) :
    [] ∉ L * K

Used by 1

Used bySolving a system of language equations

DefinitionCoefficient in the equation system of a DFA#✓fully proved

The system of equations of a DFA at a state: the coefficient of X j in the equation for X q, the finite union of the singletons {[a]} over the letters taking q to j.

def coeff {σ : Type*} [DecidableEq σ] [Fintype α] (M : DFA α σ) (q j : σ) : Language α :=
  ∑ a ∈ Finset.univ.filter (fun a => M.step q a = j), ({[a]} : Language α)

Used by 5

Used byDFA equation coefficients are regex-denoted · Languages of DFAs on finitely many numbered states are regex-denoted · Equation system satisfied by DFA state languages · Membership in a DFA equation coefficient · DFA equation coefficients exclude the empty word

DefinitionConstant term in the equation system of a DFA#✓fully proved

The constant term of the equation for X q: 1 on accepting states, 0 otherwise.

def constTerm {σ : Type*} (M : DFA α σ) (q : σ) : Language α := by
  classical
  exact if q ∈ M.accept then 1 else 0

Used by 3

Used byDFA equation constant terms are regex-denoted · Languages of DFAs on finitely many numbered states are regex-denoted · Equation system satisfied by DFA state languages

DefinitionLanguage accepted from a DFA state#✓fully proved

The language accepted from a state: the unknown X q of the system.

def fromState {σ : Type*} (M : DFA α σ) (q : σ) : Language α :=
  M.acceptsFrom q

Used by 2

Used byLanguages of DFAs on finitely many numbered states are regex-denoted · Equation system satisfied by DFA state languages

TheoremMembership in a DFA equation coefficient#✓fully proved

Membership in a coefficient: the word is a single letter taking q to j.

theorem mem_coeff {σ : Type*} [DecidableEq σ] [Fintype α] {M : DFA α σ} {q j : σ} {w : List α} :
    w ∈ coeff M q j ↔ ∃ a, M.step q a = j ∧ w = [a]

Uses 2 · Used by 2

Statement usesCoefficient in the equation system of a DFA

Proof usesMembership in a finite union of languages

Used byEquation system satisfied by DFA state languages · DFA equation coefficients exclude the empty word

TheoremDFA equation coefficients exclude the empty word#✓fully proved

No coefficient contains the empty word.

theorem nil_notMem_coeff {σ : Type*} [DecidableEq σ] [Fintype α] {M : DFA α σ} {q j : σ} :
    [] ∉ coeff M q j

Uses 2 · Used by 2

Statement usesCoefficient in the equation system of a DFA

Proof usesMembership in a DFA equation coefficient

Used byLanguages of DFAs on finitely many numbered states are regex-denoted · Equation system satisfied by DFA state languages

TheoremDFA equation coefficients are regex-denoted#✓fully proved

Every coefficient is denoted by a regular expression.

theorem denoted_coeff {σ : Type*} [DecidableEq σ] [Fintype α] {M : DFA α σ} {q j : σ} :
    IsRegexDenoted (coeff M q j)

Uses 4 · Used by 1

Statement usesLanguage denoted by a regular expression · Coefficient in the equation system of a DFA

Proof usesSingle-letter languages are regex-denoted · Regex-denoted languages are closed under finite unions

Used byLanguages of DFAs on finitely many numbered states are regex-denoted

TheoremDFA equation constant terms are regex-denoted#✓fully proved

Every constant term is denoted by a regular expression.

theorem denoted_constTerm {σ : Type*} {M : DFA α σ} {q : σ} :
    IsRegexDenoted (constTerm M q)

Uses 4 · Used by 1

Statement usesLanguage denoted by a regular expression · Constant term in the equation system of a DFA

Proof usesThe language of the empty word is regex-denoted · The empty language is regex-denoted

Used byLanguages of DFAs on finitely many numbered states are regex-denoted

TheoremEquation system satisfied by DFA state languages#✓fully proved

The DFA equations: from q, either step on a letter and continue, or stop if q accepts.

theorem fromState_eq {σ : Type*} [DecidableEq σ] [Fintype σ] [Fintype α] {M : DFA α σ} {q : σ} :
    fromState M q = (∑ j, coeff M q j * fromState M j) + constTerm M q

Uses 6 · Used by 1

Statement usesCoefficient in the equation system of a DFA · Constant term in the equation system of a DFA · Language accepted from a DFA state

Proof usesMembership in a DFA equation coefficient · Membership in a finite union of languages · DFA equation coefficients exclude the empty word

Used byLanguages of DFAs on finitely many numbered states are regex-denoted

DefinitionCoefficient after eliminating the last state#✓fully proved

The coefficient of the reduced system obtained by eliminating the last state: the old coefficient, plus the detour through the last state, which may loop there any number of times.

def elimCoeff {n : ℕ} (A : Fin (n + 1) → Fin (n + 1) → Language α) :
    Fin n → Fin n → Language α :=
  fun i j =>
    A (Fin.castSucc i) (Fin.castSucc j) +
      A (Fin.castSucc i) (Fin.last n) * (A (Fin.last n) (Fin.last n))∗ *
        A (Fin.last n) (Fin.castSucc j)

Used by 1

Used bySolving a system of language equations

DefinitionConstant term after eliminating the last state#✓fully proved

The constant term of the reduced system obtained by eliminating the last state.

def elimConst {n : ℕ} (A : Fin (n + 1) → Fin (n + 1) → Language α)
    (B : Fin (n + 1) → Language α) : Fin n → Language α :=
  fun i =>
    B (Fin.castSucc i) +
      A (Fin.castSucc i) (Fin.last n) * (A (Fin.last n) (Fin.last n))∗ * B (Fin.last n)

Used by 1

Used bySolving a system of language equations

TheoremSolving a system of language equations#✓fully proved

If the languages X i satisfy X i = (∑ j, A i j * X j) + B i with every coefficient A i j excluding the empty word and every coefficient and constant term denoted by a regular expression, then every X i is denoted by a regular expression. The proof eliminates the last state with Arden's lemma and applies the induction hypothesis to the reduced system.

theorem exists_regex_of_system (n : ℕ) :
    ∀ {A : Fin n → Fin n → Language α} {B X : Fin n → Language α},
      (∀ i j, IsRegexDenoted (A i j)) → (∀ i j, [] ∉ A i j) →
      (∀ i, IsRegexDenoted (B i)) → (∀ i, X i = (∑ j, A i j * X j) + B i) →
      ∀ i, IsRegexDenoted (X i)

Uses 8 · Used by 1

Statement usesLanguage denoted by a regular expression

Proof usesRegex-denoted languages are closed under union · Regex-denoted languages are closed under Kleene star · Regex-denoted languages are closed under concatenation · Regex-denoted languages are closed under finite unions · Coefficient after eliminating the last state · Constant term after eliminating the last state · Empty word outside a concatenation

Used byLanguages of DFAs on finitely many numbered states are regex-denoted

TheoremLanguages of DFAs on finitely many numbered states are regex-denoted#✓fully proved

The language of a DFA with Fin n states is denoted by a regular expression.

theorem exists_regex_of_dfa_fin {n : ℕ} [Finite α] (M : DFA α (Fin n)) :
    ∃ r : RegularExpression α, r.matches' = M.accepts

Uses 9 · Used by 1

Proof usesLanguage denoted by a regular expression · Coefficient in the equation system of a DFA · Constant term in the equation system of a DFA · DFA equation coefficients are regex-denoted · DFA equation constant terms are regex-denoted · Solving a system of language equations · Language accepted from a DFA state · Equation system satisfied by DFA state languages · DFA equation coefficients exclude the empty word

Used byKleene's theorem: DFA languages are regex-denoted

TheoremKleene's theorem: DFA languages are regex-denoted#✓fully proved

The language of a DFA over a finite state type is denoted by a regular expression.

theorem exists_regex_of_dfa {σ : Type*} [Finite σ] [Finite α] (M : DFA α σ) :
    ∃ r : RegularExpression α, r.matches' = M.accepts

Uses 1 · Used by 1

Proof usesLanguages of DFAs on finitely many numbered states are regex-denoted

Used byKleene's theorem, converse direction

DefinitionLetters occurring in a regular expression#✓fully proved

The letters occurring in a regular expression.

def regexLetters [DecidableEq α] : RegularExpression α → Finset α
  | .zero => ∅
  | .epsilon => ∅
  | .char a => {a}
  | .plus P Q => regexLetters P ∪ regexLetters Q
  | .comp P Q => regexLetters P ∪ regexLetters Q
  | .star P => regexLetters P

Used by 2

Used bySharpness of the finite-alphabet hypothesis · Letters of matched words occur in the regular expression

TheoremLetters of matched words occur in the regular expression#✓fully proved

Every letter of a word matched by r occurs in r.

theorem mem_matches'_letters [DecidableEq α] {r : RegularExpression α} {w : List α}
    (hw : w ∈ r.matches') {a : α} (ha : a ∈ w) : a ∈ regexLetters r

Uses 1 · Used by 1

Statement usesLetters occurring in a regular expression

Used bySharpness of the finite-alphabet hypothesis

DefinitionDFA accepting the one-letter words#✓fully proved

The three-state DFA accepting exactly the one-letter words.

def singletonDFA : DFA α (Fin 3) where
  step q _ := if q = 0 then 1 else 2
  start := 0
  accept := {1}

Used by 2

Used bySharpness of the finite-alphabet hypothesis · The one-letter-word DFA accepts exactly words of length one

TheoremThe one-letter-word DFA accepts exactly words of length one#✓fully proved

The one-letter-word DFA accepts exactly the words of length one.

theorem singletonDFA_accepts :
    (singletonDFA : DFA α (Fin 3)).accepts = {w : List α | w.length = 1}

Uses 1 · Used by 1

Statement usesDFA accepting the one-letter words

Used bySharpness of the finite-alphabet hypothesis

Language

TheoremKleene's theorem, converse direction#✓fully proved

Kleene's theorem, converse direction (Sipser, Introduction to the Theory of Computation, 3rd ed., Theorem 1.54): every regular language over a finite alphabet is denoted by a regular expression. Source: M. Sipser, Introduction to the Theory of Computation, 3rd ed., Theorem 1.54.

theorem IsRegular.exists_regex {α : Type*} [Finite α] {L : Language α} (hL : L.IsRegular) :
    ∃ r : RegularExpression α, r.matches' = L

Uses 1 · Used by 1

Proof usesKleene's theorem: DFA languages are regex-denoted

Used byKleene's theorem

TheoremKleene's theorem#✓fully proved

Kleene's theorem (Sipser, 3rd ed., Theorem 1.54): over a finite alphabet, a language is regular if and only if it is denoted by a regular expression. Source: M. Sipser, Introduction to the Theory of Computation, 3rd ed., Theorem 1.54.

theorem isRegular_iff_exists_regex {α : Type*} [Finite α] {L : Language α} :
    L.IsRegular ↔ ∃ r : RegularExpression α, r.matches' = L

Uses 1

Proof usesKleene's theorem, converse direction

TheoremSharpness of the finite-alphabet hypothesis#✓fully proved

Over an infinite alphabet, the language of one-letter words is regular but is denoted by no regular expression, since a regular expression mentions only finitely many letters. Source: M. Sipser, Introduction to the Theory of Computation, 3rd ed., Theorem 1.54 (finite alphabet).

theorem exists_regular_not_regex {α : Type*} [Infinite α] :
    ∃ L : Language α, L.IsRegular ∧ ∀ r : RegularExpression α, r.matches' ≠ L

Uses 4

Proof usesLetters of matched words occur in the regular expression · Letters occurring in a regular expression · DFA accepting the one-letter words · The one-letter-word DFA accepts exactly words of length one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.