Languages

This file contains the definition and operations on formal languages over an alphabet. Note that "strings" are implemented as lists over the alphabet. Union and concatenation define a Kleene algebra over the languages. In addition to that, we define a reversal of a language and prove that it behaves well with respect to other language operations.

def Language (α : Type u_4) : Type u_4

A language is a set of strings over an alphabet.

Equations

• Language α = Set (List α)

instance instMembershipListLanguage {α : Type u_1} : Membership (List α) (Language α)

Equations

• instMembershipListLanguage = { mem := Set.Mem }

instance instSingletonListLanguage {α : Type u_1} : Singleton (List α) (Language α)

Equations

• instSingletonListLanguage = { singleton := Set.singleton }

instance instInsertListLanguage {α : Type u_1} : Insert (List α) (Language α)

Equations

• instInsertListLanguage = { insert := Set.insert }

instance instCompleteAtomicBooleanAlgebraLanguage {α : Type u_1} : CompleteAtomicBooleanAlgebra (Language α)

Equations

• instCompleteAtomicBooleanAlgebraLanguage = Set.completeAtomicBooleanAlgebra

instance Language.instZero {α : Type u_1} : Zero (Language α)

Zero language has no elements.

Equations

• Language.instZero = { zero := ∅ }

instance Language.instOne {α : Type u_1} : One (Language α)

1 : Language α contains only one element [].

Equations

• Language.instOne = { one := {[]} }

instance Language.instInhabited {α : Type u_1} : Inhabited (Language α)

Equations

• Language.instInhabited = { default := ∅ }

instance Language.instAdd {α : Type u_1} : Add (Language α)

The sum of two languages is their union.

Equations

• Language.instAdd = { add := fun (x1 x2 : Set (List α)) => x1 ∪ x2 }

instance Language.instMul {α : Type u_1} : Mul (Language α)

The product of two languages l and m is the language made of the strings x ++ y where x ∈ l and y ∈ m.

Equations

• Language.instMul = { mul := Set.image2 fun (x1 x2 : List α) => x1 ++ x2 }

theorem Language.zero_def {α : Type u_1} : 0 = ∅

theorem Language.one_def {α : Type u_1} : 1 = {[]}

theorem Language.add_def {α : Type u_1} (l : Language α) (m : Language α) : l + m = l ∪ m

theorem Language.mul_def {α : Type u_1} (l : Language α) (m : Language α) : l * m = Set.image2 (fun (x1 x2 : List α) => x1 ++ x2) l m

instance Language.instKStar {α : Type u_1} : KStar (Language α)

The Kleene star of a language L is the set of all strings which can be written by concatenating strings from L.

Equations

• Language.instKStar = { kstar := fun (l : Language α) => {x : List α | ∃ (L : List (List α)), x = L.join ∧ ∀ y ∈ L, y ∈ l} }

theorem Language.kstar_def {α : Type u_1} (l : Language α) : KStar.kstar l = {x : List α | ∃ (L : List (List α)), x = L.join ∧ ∀ y ∈ L, y ∈ l}

theorem Language.ext_iff {α : Type u_1} {l : Language α} {m : Language α} : l = m ↔ ∀ (x : List α), x ∈ l ↔ x ∈ m

theorem Language.ext {α : Type u_1} {l : Language α} {m : Language α} (h : ∀ (x : List α), x ∈ l ↔ x ∈ m) : l = m

@[simp]

theorem Language.not_mem_zero {α : Type u_1} (x : List α) : x ∉ 0

@[simp]

theorem Language.mem_one {α : Type u_1} (x : List α) : x ∈ 1 ↔ x = []

theorem Language.nil_mem_one {α : Type u_1} : [] ∈ 1

theorem Language.mem_add {α : Type u_1} (l : Language α) (m : Language α) (x : List α) : x ∈ l + m ↔ x ∈ l ∨ x ∈ m

theorem Language.mem_mul {α : Type u_1} {l : Language α} {m : Language α} {x : List α} : x ∈ l * m ↔ ∃ a ∈ l, ∃ b ∈ m, a ++ b = x

theorem Language.append_mem_mul {α : Type u_1} {l : Language α} {m : Language α} {a : List α} {b : List α} : a ∈ l → b ∈ m → a ++ b ∈ l * m

theorem Language.mem_kstar {α : Type u_1} {l : Language α} {x : List α} : x ∈ KStar.kstar l ↔ ∃ (L : List (List α)), x = L.join ∧ ∀ y ∈ L, y ∈ l

theorem Language.join_mem_kstar {α : Type u_1} {l : Language α} {L : List (List α)} (h : ∀ y ∈ L, y ∈ l) : L.join ∈ KStar.kstar l

theorem Language.nil_mem_kstar {α : Type u_1} (l : Language α) : [] ∈ KStar.kstar l

instance Language.instSemiring {α : Type u_1} : Semiring (Language α)

Equations

• Language.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRec ⋯ ⋯

@[simp]

theorem Language.add_self {α : Type u_1} (l : Language α) : l + l = l

def Language.map {α : Type u_1} {β : Type u_2} (f : α → β) : Language α →+* Language β

Maps the alphabet of a language.

Equations

• Language.map f = { toFun := Set.image (List.map f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Language.map_id {α : Type u_1} (l : Language α) : (Language.map id) l = l

@[simp]

theorem Language.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (l : Language α) : (Language.map g) ((Language.map f) l) = (Language.map (g ∘ f)) l

theorem Language.mem_kstar_iff_exists_nonempty {α : Type u_1} {l : Language α} {x : List α} : x ∈ KStar.kstar l ↔ ∃ (S : List (List α)), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

theorem Language.kstar_def_nonempty {α : Type u_1} (l : Language α) : KStar.kstar l = {x : List α | ∃ (S : List (List α)), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

theorem Language.le_iff {α : Type u_1} (l : Language α) (m : Language α) : l ≤ m ↔ l + m = m

theorem Language.le_mul_congr {α : Type u_1} {l₁ : Language α} {l₂ : Language α} {m₁ : Language α} {m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂

theorem Language.le_add_congr {α : Type u_1} {l₁ : Language α} {l₂ : Language α} {m₁ : Language α} {m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂

theorem Language.mem_iSup {α : Type u_1} {ι : Sort v} {l : ι → Language α} {x : List α} : x ∈ ⨆ (i : ι), l i ↔ ∃ (i : ι), x ∈ l i

theorem Language.iSup_mul {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m

theorem Language.mul_iSup {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : m * ⨆ (i : ι), l i = ⨆ (i : ι), m * l i

theorem Language.iSup_add {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m

theorem Language.add_iSup {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : m + ⨆ (i : ι), l i = ⨆ (i : ι), m + l i

theorem Language.mem_pow {α : Type u_1} {l : Language α} {x : List α} {n : ℕ} : x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.join ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l

theorem Language.kstar_eq_iSup_pow {α : Type u_1} (l : Language α) : KStar.kstar l = ⨆ (i : ℕ), l ^ i

@[simp]

theorem Language.map_kstar {α : Type u_1} {β : Type u_2} (f : α → β) (l : Language α) : (Language.map f) (KStar.kstar l) = KStar.kstar ((Language.map f) l)

theorem Language.mul_self_kstar_comm {α : Type u_1} (l : Language α) : KStar.kstar l * l = l * KStar.kstar l

@[simp]

theorem Language.one_add_self_mul_kstar_eq_kstar {α : Type u_1} (l : Language α) : 1 + l * KStar.kstar l = KStar.kstar l

@[simp]

theorem Language.one_add_kstar_mul_self_eq_kstar {α : Type u_1} (l : Language α) : 1 + KStar.kstar l * l = KStar.kstar l

instance Language.instKleeneAlgebra {α : Type u_1} : KleeneAlgebra (Language α)

Equations

• Language.instKleeneAlgebra = KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

def Language.reverse {α : Type u_1} (l : Language α) : Language α

Language l.reverse is defined as the set of words from l backwards.

Equations

• l.reverse = {w : List α | w.reverse ∈ l}

@[simp]

theorem Language.mem_reverse {α : Type u_1} {l : Language α} {a : List α} : a ∈ l.reverse ↔ a.reverse ∈ l

theorem Language.reverse_mem_reverse {α : Type u_1} {l : Language α} {a : List α} : a.reverse ∈ l.reverse ↔ a ∈ l

theorem Language.reverse_eq_image {α : Type u_1} (l : Language α) : l.reverse = List.reverse '' l

@[simp]

theorem Language.reverse_zero {α : Type u_1} : Language.reverse 0 = 0

@[simp]

theorem Language.reverse_one {α : Type u_1} : Language.reverse 1 = 1

theorem Language.reverse_involutive {α : Type u_1} : Function.Involutive Language.reverse

theorem Language.reverse_bijective {α : Type u_1} : Function.Bijective Language.reverse

theorem Language.reverse_injective {α : Type u_1} : Function.Injective Language.reverse

theorem Language.reverse_surjective {α : Type u_1} : Function.Surjective Language.reverse

@[simp]

theorem Language.reverse_reverse {α : Type u_1} (l : Language α) : l.reverse.reverse = l

@[simp]

theorem Language.reverse_add {α : Type u_1} (l : Language α) (m : Language α) : (l + m).reverse = l.reverse + m.reverse

@[simp]

theorem Language.reverse_mul {α : Type u_1} (l : Language α) (m : Language α) : (l * m).reverse = m.reverse * l.reverse

@[simp]

theorem Language.reverse_iSup {α : Type u_1} {ι : Sort u_4} (l : ι → Language α) : (⨆ (i : ι), l i).reverse = ⨆ (i : ι), (l i).reverse

@[simp]

theorem Language.reverse_iInf {α : Type u_1} {ι : Sort u_4} (l : ι → Language α) : (⨅ (i : ι), l i).reverse = ⨅ (i : ι), (l i).reverse

@[simp]

theorem Language.reverseIso_symm_apply (α : Type u_1) (l' : (Language α)ᵐᵒᵖ) : (Language.reverseIso α).symm l' = (MulOpposite.unop l').reverse

@[simp]

theorem Language.reverseIso_apply (α : Type u_1) (l : Language α) : (Language.reverseIso α) l = MulOpposite.op l.reverse

def Language.reverseIso (α : Type u_1) : Language α ≃+* (Language α)ᵐᵒᵖ

Language.reverse as a ring isomorphism to the opposite ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Language.reverse_pow {α : Type u_1} (l : Language α) (n : ℕ) : (l ^ n).reverse = l.reverse ^ n

@[simp]

theorem Language.reverse_kstar {α : Type u_1} (l : Language α) : (KStar.kstar l).reverse = KStar.kstar l.reverse

inductive Symbol (T : Type u_1) (N : Type u_2) : Type (max u_1 u_2)

Symbols for use by all kinds of grammars.

• terminal: {T : Type u_1} → {N : Type u_2} → T → Symbol T N

  Terminal symbols (of the same type as the language)

• nonterminal: {T : Type u_1} → {N : Type u_2} → N → Symbol T N

  Nonterminal symbols (must not be present at the end of word being generated)

instance instDecidableEqSymbol : {T : Type u_4} → {N : Type u_5} → [inst : DecidableEq T] → [inst : DecidableEq N] → DecidableEq (Symbol T N)

Equations

• instDecidableEqSymbol = decEqSymbol✝

instance instReprSymbol : {T : Type u_4} → {N : Type u_5} → [inst : Repr T] → [inst : Repr N] → Repr (Symbol T N)

Equations

• instReprSymbol = { reprPrec := reprSymbol✝ }

instance instFintypeSymbol : {T : Type u_4} → {N : Type u_5} → [inst : Fintype T] → [inst : Fintype N] → Fintype (Symbol T N)

Equations

• instFintypeSymbol = Fintype.ofEquiv (T ⊕ N) (Symbol.proxyTypeEquiv T N)