Language Operations

This file defines basic operations on languages used throughout the closure-property proofs.

Main declarations

• bijemapLang
• permuteLang

theorem Language.mem_list_prod_iff_forall2 {α : Type u_1} (S : List (Language α)) (w : List α) : w ∈ S.prod ↔ ∃ (W : List (List α)), w = W.flatten ∧ List.Forall₂ (fun (w : List α) (s : Language α) => w ∈ s) W S

def Language.subst {α β : Type} (L : Language α) (f : α → Language β) : Language β

Equations

• L.subst f = {u : List β | ∃ w ∈ L, u ∈ (List.map f w).prod}

theorem Language.subst_pair_eq_mul {β : Type} (f : Bool → Language β) : {[false, true]}.subst f = f false * f true

theorem Language.subst_singletons_eq_add {β : Type} (f : Bool → Language β) : {[false], [true]}.subst f = f false + f true

theorem Language.subst_univ_unit_eq_kstar {β : Type} (f : Unit → Language β) : subst Set.univ f = KStar.kstar (f ())

theorem Language.mem_prod_singletons_iff {α β : Type} (f : α → β) (w : List α) (u : List β) : u ∈ (List.map (fun (x : α) => {[f x]}) w).prod ↔ u = List.map f w

theorem Language.subst_singletons_eq_map {α β : Type} (L : Language α) (f : α → β) : (L.subst fun (x : α) => {[f x]}) = (map f) L

Substituting each symbol x with the singleton language {[f x]} is the same as mapping the whole language along f.

def Language.prefixLang {α : Type u_1} (L : Language α) : Language α

The prefix language of L consists of all words that can be extended on the right to a word in L.

Equations

• L.prefixLang = {w : List α | ∃ (v : List α), w ++ v ∈ L}

@[simp]

theorem Language.mem_prefixLang {α : Type u_1} {L : Language α} {w : List α} : w ∈ L.prefixLang ↔ ∃ (v : List α), w ++ v ∈ L

theorem Language.subset_prefixLang {α : Type u_1} (L : Language α) : L ≤ L.prefixLang

theorem Language.nil_mem_prefixLang {α : Type u_1} {L : Language α} (h : ∃ (w : List α), w ∈ L) : [] ∈ L.prefixLang

theorem Language.prefixLang_mono {α : Type u_1} {L₁ L₂ : Language α} (h : L₁ ≤ L₂) : L₁.prefixLang ≤ L₂.prefixLang

@[simp]

theorem Language.prefixLang_zero {α : Type u_1} : prefixLang 0 = 0

@[simp]

theorem Language.prefixLang_add {α : Type u_1} (L₁ L₂ : Language α) : (L₁ + L₂).prefixLang = L₁.prefixLang + L₂.prefixLang

theorem Language.prefixLang_prefixLang {α : Type u_1} (L : Language α) : L.prefixLang.prefixLang = L.prefixLang

def Language.suffixLang {α : Type u_1} (L : Language α) : Language α

The suffix language of L consists of all words that can be extended on the left to a word in L.

Equations

• L.suffixLang = {w : List α | ∃ (v : List α), v ++ w ∈ L}

@[simp]

theorem Language.mem_suffixLang {α : Type u_1} {L : Language α} {w : List α} : w ∈ L.suffixLang ↔ ∃ (v : List α), v ++ w ∈ L

theorem Language.subset_suffixLang {α : Type u_1} (L : Language α) : L ≤ L.suffixLang

theorem Language.suffixLang_mono {α : Type u_1} {L₁ L₂ : Language α} (h : L₁ ≤ L₂) : L₁.suffixLang ≤ L₂.suffixLang

@[simp]

theorem Language.suffixLang_zero {α : Type u_1} : suffixLang 0 = 0

@[simp]

theorem Language.suffixLang_add {α : Type u_1} (L₁ L₂ : Language α) : (L₁ + L₂).suffixLang = L₁.suffixLang + L₂.suffixLang

def Language.bijemapLang {T : Type u_1} {T' : Type u_2} (L : Language T) (π : T ≃ T') : Language T'

Equations

• L.bijemapLang π w = (List.map (⇑π.symm) w ∈ L)

def Language.permuteLang {T : Type u_1} (L : Language T) (π : Equiv.Perm T) : Language T

Equations

• L.permuteLang π = L.bijemapLang π

@[simp]

theorem Language.bijemapLang_symm_bijemapLang {T : Type u_2} {T' : Type u_1} (L : Language T) (π : T ≃ T') : (L.bijemapLang π).bijemapLang π.symm = L

theorem Language.suffixLang_eq_reverse_prefixLang_reverse {T : Type u_1} (L : Language T) : L.suffixLang = L.reverse.prefixLang.reverse

theorem Language.prefixLang_eq_reverse_suffixLang_reverse {T : Type u_1} (L : Language T) : L.prefixLang = L.reverse.suffixLang.reverse

def Language.rightQuotient {α : Type u_1} (L R : Language α) : Language α

The right quotient of L by R: the set of words w such that w ++ v ∈ L for some v ∈ R. This generalises prefixLang (which is rightQuotient L Set.univ).

Equations

• L.rightQuotient R = {w : List α | ∃ v ∈ R, w ++ v ∈ L}

instance Language.instHDiv_langlib {α : Type u_1} : HDiv (Language α) (Language α) (Language α)

Equations

• Language.instHDiv_langlib = { hDiv := Language.rightQuotient }

def Language.«term_\\_» : Lean.TrailingParserDescr

Equations

• Language.«term_\\_» = Lean.ParserDescr.trailingNode `Language.«term_\\_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\\\ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem Language.mem_rightQuotient {α : Type u_1} {L R : Language α} {w : List α} : w ∈ L.rightQuotient R ↔ ∃ v ∈ R, w ++ v ∈ L

theorem Language.prefixLang_eq_rightQuotient_univ {α : Type u_1} (L : Language α) : L.prefixLang = L.rightQuotient Set.univ

theorem Language.reverse_leftQuotient_eq_rightQuotient_reverse_singleton {α : Type u_1} (L : Language α) (x : List α) : ((fun (x : List α) (L : Language α) => L.leftQuotient x) x L).reverse = L.reverse / {x.reverse}

theorem Language.leftQuotient_eq_reverse_rightQuotient_reverse_singleton {α : Type u_1} (L : Language α) (x : List α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) x L = (L.reverse / {x.reverse}).reverse

theorem Language.rightQuotient_mono_left {α : Type u_1} {L₁ L₂ R : Language α} (h : L₁ ≤ L₂) : L₁ / R ≤ L₂ / R

theorem Language.rightQuotient_mono_right {α : Type u_1} {L R₁ R₂ : Language α} (h : R₁ ≤ R₂) : L / R₁ ≤ L / R₂

@[simp]

theorem Language.rightQuotient_add_right {α : Type u_1} (L R₁ R₂ : Language α) : L / (R₁ + R₂) = L / R₁ + L / R₂

@[simp]

theorem Language.rightQuotient_zero_left {α : Type u_1} (R : Language α) : 0 / R = 0

@[simp]

theorem Language.rightQuotient_zero_right {α : Type u_1} (L : Language α) : L / 0 = 0

@[simp]

theorem Language.rightQuotient_add_left {α : Type u_1} (L₁ L₂ R : Language α) : (L₁ + L₂) / R = L₁ / R + L₂ / R

theorem Language.subset_rightQuotient_univ {α : Type u_1} (L : Language α) : L ≤ L.rightQuotient Set.univ

theorem Language.leftQuotient_mono {α : Type u_1} {L₁ L₂ : Language α} (h : L₁ ≤ L₂) (x : List α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) x L₁ ≤ (fun (x : List α) (L : Language α) => L.leftQuotient x) x L₂

@[simp]

theorem Language.leftQuotient_zero {α : Type u_1} (x : List α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) x 0 = 0

@[simp]

theorem Language.nil_leftQuotient {α : Type u_1} (L : Language α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) [] L = L

@[simp]

theorem Language.cons_leftQuotient {α : Type u_1} (a : α) (x : List α) (L : Language α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) (a :: x) L = (fun (x : List α) (L : Language α) => L.leftQuotient x) x ((fun (x : List α) (L : Language α) => L.leftQuotient x) [a] L)

@[simp]

theorem Language.append_leftQuotient {α : Type u_1} (x y : List α) (L : Language α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) (x ++ y) L = (fun (x : List α) (L : Language α) => L.leftQuotient x) y ((fun (x : List α) (L : Language α) => L.leftQuotient x) x L)

@[simp]

theorem Language.leftQuotient_add {α : Type u_1} (x : List α) (L₁ L₂ : Language α) : (fun (x : List α) (L : Language α) => L.leftQuotient x) x (L₁ + L₂) = (fun (x : List α) (L : Language α) => L.leftQuotient x) x L₁ + (fun (x : List α) (L : Language α) => L.leftQuotient x) x L₂