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.instZeroLanguage {α : Type u_1} : Zero (Language α)

Zero language has no elements.

Equations

• Language.instZeroLanguage = { zero := ∅ }

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

1 : Language α contains only one element [].

Equations

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

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

Equations

• Language.instInhabitedLanguage = { default := ∅ }

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

The sum of two languages is their union.

Equations

• Language.instAddLanguage = { add := fun (x x_1 : Set (List α)) => x ∪ x_1 }

instance Language.instMulLanguage {α : 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.instMulLanguage = { mul := Set.image2 fun (x x_1 : List α) => x ++ x_1 }

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 (x x_1 : List α) => x ++ x_1) l m

instance Language.instKStarLanguage {α : 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.instKStarLanguage = { kstar := fun (l : Language α) => {x : List α | ∃ (L : List (List α)), x = List.join L ∧ ∀ y ∈ L, y ∈ l} }

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

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 = List.join L ∧ ∀ y ∈ L, y ∈ l

theorem Language.join_mem_kstar {α : Type u_1} {l : Language α} {L : List (List α)} (h : ∀ y ∈ L, y ∈ l) : List.join L ∈ 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 = { toMonoidHom := { toOneHom := { 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 = List.join S ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

theorem Language.kstar_def_nonempty {α : Type u_1} (l : Language α) : KStar.kstar l = {x : List α | ∃ (S : List (List α)), x = List.join S ∧ ∀ 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 = List.join S ∧ List.length S = 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.instKleeneAlgebraLanguage {α : Type u_1} : KleeneAlgebra (Language α)

Equations

• Language.instKleeneAlgebraLanguage = let __src := Language.instSemiring; let __src_1 := Set.completeAtomicBooleanAlgebra; 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

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

@[simp]

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

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

theorem Language.reverse_eq_image {α : Type u_1} (l : Language α) : Language.reverse l = 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 α) : Language.reverse (Language.reverse l) = l

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 : ℕ) : Language.reverse (l ^ n) = Language.reverse l ^ n

@[simp]

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

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)