ωLanguage

This file contains the definition and operations on formal ω-languages, which are sets of infinite sequences over an alphabet α (namely, objects of type ωSequence α).

Main definitions and notations

In general we will use p and q to denote ω-languages and l and m to denote languages (namely, sets of finite sequences of type List α).

• Set operations (union, intersection, complementation), constants (empty and universe sets), and the subset relation are denoted using lattice-theoretic notations (p ∪ q, p ∩ q, pᶜ, ⊥, ⊤, and ≤) and terminologies in definition and theorem names ("inf", "sup", "compl", "bot", "top", "le").
• l * p: ω-language of x ++ω y where x ∈ l and y ∈ p; referred to as "hmul" in definition and theorem names.
• l^ω: ω-language of infinite sequences each of which is the concatenation of infinitely many (nonemoty) members of l; referred to as "omegaPow" in definition and theorem names.
  • Note: Since l^ω is defined using ωSequence.flatten, any theorem about it needs the additional assumption [Inhabited α].
• l↗ω: ω-language of infinite sequences each of which has infinitely many distinct prefixes in l; referred to as "omegaLim" in definition and theorem names.
• p.map f: transform an ω-language p over α into an ω-language over β by mapping through f : α → β; referred to as "map" in definition and theorem names.

Main theorems

• Many algebraic properties of the above operations.
• omegaPow_seq_prop: an alternative characterization of l^ω.
• omegaPow_coind: a "coinductive" rule for proving p is a subset of l^ω.
• hmul_omegaPow_eq_omegaPow: l * l^ω = l^ω.
• kstar_omegaPow_eq_omegaPow: (l∗)^ω = l^ω.
• kstar_hmul_omegaPow_eq_omegaPow: l∗ * l^ω = l^ω.

TODO

• Prove more theorems about omegaLim and map.

def Language.toSet {α : Type u_1} (l : Language α) : Set (List α)

The set of lists in a language.

Equations

• l.toSet = l

structure Cslib.ωLanguage (α : Type u) : Type u

An ω-language is a set of ω-sequences over an alphabet.

• ofSet :: (
• toSet : Set (ωSequence α)

  The set of ω-sequences in an ω-language.

• )

theorem Cslib.ωLanguage.ext {α : Type u} {x y : ωLanguage α} (toSet : x.toSet = y.toSet) : x = y

theorem Cslib.ωLanguage.ext_iff {α : Type u} {x y : ωLanguage α} : x = y ↔ x.toSet = y.toSet

def Cslib.instInhabitedωLanguage.default {a✝ : Type u_4} : ωLanguage a✝

Equations

• Cslib.instInhabitedωLanguage.default = { toSet := default }

@[implicit_reducible]

instance Cslib.instInhabitedωLanguage {a✝ : Type u_4} : Inhabited (ωLanguage a✝)

Equations

• Cslib.instInhabitedωLanguage = { default := Cslib.instInhabitedωLanguage.default }

@[implicit_reducible]

instance Cslib.instCoeSetωSequenceωLanguage {α : Type u_1} : Coe (Set (ωSequence α)) (ωLanguage α)

Equations

• Cslib.instCoeSetωSequenceωLanguage = { coe := fun (f : Set (Cslib.ωSequence α)) => { toSet := f } }

@[simp]

theorem Cslib.ωLanguage.ofSet_toSet {α : Type u_1} (l : ωLanguage α) : { toSet := l.toSet } = l

theorem Cslib.ωLanguage.toSet_ofSet {α : Type u_1} (s : Set (ωSequence α)) : { toSet := s }.toSet = s

def Cslib.ωLanguage.equiv {α : Type u_1} : ωLanguage α ≃ Set (ωSequence α)

The equivalence between ωLanguage α and Set (ωSequence α).

Equations

• Cslib.ωLanguage.equiv = { toFun := Cslib.ωLanguage.toSet, invFun := Cslib.ωLanguage.ofSet, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra {α : Type u_1} : CompleteAtomicBooleanAlgebra (ωLanguage α)

Equations

• Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra = Cslib.ωLanguage.equiv.completeAtomicBooleanAlgebra

@[implicit_reducible]

instance Cslib.ωLanguage.instSetLikeωSequence {α : Type u_1} : SetLike (ωLanguage α) (ωSequence α)

Equations

• Cslib.ωLanguage.instSetLikeωSequence = { coe := Cslib.ωLanguage.toSet, coe_injective' := ⋯ }

@[implicit_reducible]

instance Cslib.ωLanguage.instHasSubset {α : Type u_1} : HasSubset (ωLanguage α)

Equations

• Cslib.ωLanguage.instHasSubset = { Subset := fun (x1 x2 : Cslib.ωLanguage α) => x1 ≤ x2 }

theorem Cslib.ωLanguage.le_def {α : Type u_1} (p q : ωLanguage α) : p ≤ q ↔ p.toSet ⊆ q.toSet

theorem Cslib.ωLanguage.top_def {α : Type u_1} : ⊤ = { toSet := Set.univ }

theorem Cslib.ωLanguage.bot_def {α : Type u_1} : ⊥ = { toSet := ∅ }

theorem Cslib.ωLanguage.sup_def {α : Type u_1} (p q : ωLanguage α) : p ⊔ q = { toSet := p.toSet ∪ q.toSet }

theorem Cslib.ωLanguage.inf_def {α : Type u_1} (p q : ωLanguage α) : p ⊓ q = { toSet := p.toSet ∩ q.toSet }

theorem Cslib.ωLanguage.compl_def {α : Type u_1} (p : ωLanguage α) : pᶜ = { toSet := p.toSetᶜ }

theorem Cslib.ωLanguage.sSup_def {α : Type u_1} (s : Set (ωLanguage α)) : sSup s = { toSet := ⋃ p ∈ s, p.toSet }

theorem Cslib.ωLanguage.sInf_def {α : Type u_1} (s : Set (ωLanguage α)) : sInf s = { toSet := ⋂ p ∈ s, p.toSet }

theorem Cslib.ωLanguage.iSup_def {α : Type u_1} {ι : Sort v} {p : ι → ωLanguage α} : ⨆ (i : ι), p i = { toSet := ⋃ (i : ι), (p i).toSet }

theorem Cslib.ωLanguage.iInf_def {α : Type u_1} {ι : Sort v} {p : ι → ωLanguage α} : ⨅ (i : ι), p i = { toSet := ⋂ (i : ι), (p i).toSet }

@[implicit_reducible]

instance Cslib.ωLanguage.instHMulLanguage {α : Type u_1} : HMul (Language α) (ωLanguage α) (ωLanguage α)

The concatenation of a language l and an ω-language p is the ω-language made of infinite sequences x ++ω y where x ∈ l and y ∈ p.

Equations

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

theorem Cslib.ωLanguage.hmul_def {α : Type u_1} (l : Language α) (p : ωLanguage α) : l * p = { toSet := Set.image2 (fun (x1 : List α) (x2 : ωSequence α) => x1 ++ω x2) l.toSet p.toSet }

def Cslib.ωLanguage.omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : ωLanguage α

Concatenation of infinitely many copies of a languages, resulting in an ω-language. A.k.a. ω-power.

Equations

• Cslib.ωLanguage.omegaPow l = { toSet := {s : Cslib.ωSequence α | ∃ (xs : Cslib.ωSequence (List α)), xs.flatten = s ∧ ∀ (k : ℕ), xs k ∈ l - 1} }

class Cslib.ωLanguage.OmegaPow (α : Type u_4) (β : outParam (Type u_5)) : Type (max u_4 u_5)

Notation class for omegaPow.

• omegaPow : α → β

  The omegaPow operation.

def Cslib.ωLanguage.«term_^ω» : Lean.TrailingParserDescr

Use the postfix notation ^ωforomegaPow`.

Equations

• Cslib.ωLanguage.«term_^ω» = Lean.ParserDescr.trailingNode `Cslib.ωLanguage.«term_^ω» 1024 1024 (Lean.ParserDescr.symbol "^ω")

@[implicit_reducible]

instance Cslib.ωLanguage.instOmegaPowLanguageOfInhabited {α : Type u_1} [Inhabited α] : OmegaPow (Language α) (ωLanguage α)

Equations

• Cslib.ωLanguage.instOmegaPowLanguageOfInhabited = { omegaPow := Cslib.ωLanguage.omegaPow }

theorem Cslib.ωLanguage.omegaPow_def {α : Type u_1} [Inhabited α] (l : Language α) : l^ω = { toSet := {s : ωSequence α | ∃ (xs : ωSequence (List α)), xs.flatten = s ∧ ∀ (k : ℕ), xs k ∈ l - 1} }

def Cslib.ωLanguage.omegaLim {α : Type u_1} (l : Language α) : ωLanguage α

The ω-limit of a language l is the ω-language of infinite sequences each of which contains infinitely many distinct prefixes in l.

Equations

• Cslib.ωLanguage.omegaLim l = { toSet := {s : Cslib.ωSequence α | ∃ᶠ (m : ℕ) in Filter.atTop, s.extract 0 m ∈ l} }

class Cslib.ωLanguage.OmegaLim (α : Type u_4) (β : outParam (Type u_5)) : Type (max u_4 u_5)

Notation class for omegaLim.

• omegaLim : α → β

  The omegaLim operation.

def Cslib.ωLanguage.«term_↗ω» : Lean.TrailingParserDescr

Use the postfix notation ↗ωforomegaLim`.

Equations

• Cslib.ωLanguage.«term_↗ω» = Lean.ParserDescr.trailingNode `Cslib.ωLanguage.«term_↗ω» 1024 1024 (Lean.ParserDescr.symbol "↗ω")

@[implicit_reducible]

instance Cslib.ωLanguage.instOmegaLim {α : Type u_1} : OmegaLim (Language α) (ωLanguage α)

Equations

• Cslib.ωLanguage.instOmegaLim = { omegaLim := Cslib.ωLanguage.omegaLim }

theorem Cslib.ωLanguage.omegaLim_def {α : Type u_1} (l : Language α) : l↗ω = { toSet := {s : ωSequence α | ∃ᶠ (m : ℕ) in Filter.atTop, s.extract 0 m ∈ l} }

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

transform an ω-language p over α into an ω-language over β by mapping through f : α → β.

Equations

• Cslib.ωLanguage.map f p = { toSet := Cslib.ωSequence.map f '' p.toSet }

theorem Cslib.ωLanguage.map_def {α : Type u_1} {β : Type u_2} (f : α → β) (p : ωLanguage α) : map f p = { toSet := ωSequence.map f '' p.toSet }

theorem Cslib.ωLanguage.mem_def {α : Type u_1} (p : ωLanguage α) (s : ωSequence α) : s ∈ p ↔ s ∈ p.toSet

theorem Cslib.ωLanguage.mem_ext {α : Type u_1} {p q : ωLanguage α} (h : ∀ (s : ωSequence α), s ∈ p ↔ s ∈ q) : p = q

@[simp]

theorem Cslib.ωLanguage.mem_top {α : Type u_1} (s : ωSequence α) : s ∈ ⊤

@[simp]

theorem Cslib.ωLanguage.notMem_bot {α : Type u_1} (s : ωSequence α) : s ∉ ⊥

@[simp]

theorem Cslib.ωLanguage.mem_sup {α : Type u_1} (p q : ωLanguage α) (s : ωSequence α) : s ∈ p ⊔ q ↔ s ∈ p ∨ s ∈ q

@[simp]

theorem Cslib.ωLanguage.mem_inf {α : Type u_1} (p q : ωLanguage α) (s : ωSequence α) : s ∈ p ⊓ q ↔ s ∈ p ∧ s ∈ q

@[simp]

theorem Cslib.ωLanguage.mem_compl {α : Type u_1} (p : ωLanguage α) (s : ωSequence α) : s ∈ pᶜ ↔ s ∉ p

@[simp]

theorem Cslib.ωLanguage.mem_sSup {α : Type u_1} (ps : Set (ωLanguage α)) {s : ωSequence α} : s ∈ sSup ps ↔ ∃ p ∈ ps, s ∈ p

@[simp]

theorem Cslib.ωLanguage.mem_sInf {α : Type u_1} (ps : Set (ωLanguage α)) {s : ωSequence α} : s ∈ sInf ps ↔ ∀ p ∈ ps, s ∈ p

@[simp]

theorem Cslib.ωLanguage.mem_iSup {α : Type u_1} {ι : Sort v} {p : ι → ωLanguage α} {s : ωSequence α} : s ∈ ⨆ (i : ι), p i ↔ ∃ (i : ι), s ∈ p i

@[simp]

theorem Cslib.ωLanguage.mem_iInf {α : Type u_1} {ι : Sort v} {p : ι → ωLanguage α} {s : ωSequence α} : s ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), s ∈ p i

@[simp]

theorem Cslib.ωLanguage.mem_hmul {α : Type u_1} {l : Language α} {p : ωLanguage α} {s : ωSequence α} : s ∈ l * p ↔ ∃ x ∈ l, ∃ t ∈ p, x ++ω t = s

theorem Cslib.ωLanguage.append_mem_hmul {α : Type u_1} {l : Language α} {p : ωLanguage α} {x : List α} {s : ωSequence α} : x ∈ l → s ∈ p → x ++ω s ∈ l * p

@[simp]

theorem Cslib.ωLanguage.mem_omegaPow {α : Type u_1} {l : Language α} {s : ωSequence α} [Inhabited α] : s ∈ l^ω ↔ ∃ (xs : ωSequence (List α)), xs.flatten = s ∧ ∀ (k : ℕ), xs k ∈ l - 1

theorem Cslib.ωLanguage.flatten_mem_omegaPow {α : Type u_1} {l : Language α} [Inhabited α] {xs : ωSequence (List α)} (h_xs : ∀ (k : ℕ), xs k ∈ l - 1) : xs.flatten ∈ l^ω

@[simp]

theorem Cslib.ωLanguage.mem_omegaLim {α : Type u_1} {l : Language α} {s : ωSequence α} : s ∈ l↗ω ↔ ∃ᶠ (m : ℕ) in Filter.atTop, s.extract 0 m ∈ l

theorem Cslib.ωLanguage.mul_hmul {α : Type u_1} {l m : Language α} {p : ωLanguage α} : l * m * p = l * (m * p)

@[simp]

theorem Cslib.ωLanguage.zero_hmul {α : Type u_1} {p : ωLanguage α} : 0 * p = ⊥

@[simp]

theorem Cslib.ωLanguage.hmul_bot {α : Type u_1} {l : Language α} : l * ⊥ = ⊥

@[simp]

theorem Cslib.ωLanguage.one_hmul {α : Type u_1} {p : ωLanguage α} : 1 * p = p

theorem Cslib.ωLanguage.hmul_sup {α : Type u_1} {l : Language α} {p q : ωLanguage α} : l * (p ⊔ q) = l * p ⊔ l * q

theorem Cslib.ωLanguage.add_hmul {α : Type u_1} {l m : Language α} {p : ωLanguage α} : (l + m) * p = l * p ⊔ m * p

theorem Cslib.ωLanguage.iSup_hmul {α : Type u_1} {ι : Sort v} (l : ι → Language α) (p : ωLanguage α) : (⨆ (i : ι), l i) * p = ⨆ (i : ι), l i * p

theorem Cslib.ωLanguage.hmul_iSup {α : Type u_1} {ι : Sort v} (p : ι → ωLanguage α) (l : Language α) : l * ⨆ (i : ι), p i = ⨆ (i : ι), l * p i

theorem Cslib.ωLanguage.le_hmul_congr {α : Type u_1} {l1 l2 : Language α} {p1 p2 : ωLanguage α} (hl : l1 ≤ l2) (hp : p1 ≤ p2) : l1 * p1 ≤ l2 * p2

theorem Cslib.ωLanguage.le_omegaPow_congr {α : Type u_1} [Inhabited α] {l1 l2 : Language α} (h : l1 ≤ l2) : l1^ω ≤ l2^ω

@[simp]

theorem Cslib.ωLanguage.omegaPow_of_sub_one {α : Type u_1} {l : Language α} [Inhabited α] : (l - 1)^ω = l^ω

@[simp]

theorem Cslib.ωLanguage.zero_omegaPow {α : Type u_1} [Inhabited α] : 0^ω = ⊥

@[simp]

theorem Cslib.ωLanguage.one_omegaPow {α : Type u_1} [Inhabited α] : 1^ω = ⊥

@[simp]

theorem Cslib.ωLanguage.omegaPow_of_le_one {α : Type u_1} {l : Language α} [Inhabited α] (h : l ≤ 1) : l^ω = ⊥

theorem Cslib.ωLanguage.omegaPow_eq_empty {α : Type u_1} {l : Language α} [Inhabited α] (h : l^ω = ⊥) : l ≤ 1

theorem Cslib.ωLanguage.hmul_seq_prop {α : Type u_1} {l : Language α} {p : ωLanguage α} : l * p = { toSet := {s : ωSequence α | ∃ (k : ℕ), ωSequence.take k s ∈ l ∧ ωSequence.drop k s ∈ p} }

An alternative characterization of l * p.

theorem Cslib.ωLanguage.omegaPow_seq_prop {α : Type u_1} {l : Language α} [Inhabited α] : l^ω = { toSet := {s : ωSequence α | ∃ (f : ℕ → ℕ), StrictMono f ∧ f 0 = 0 ∧ ∀ (m : ℕ), s.extract (f m) (f (m + 1)) ∈ l} }

An alternative characterization of l^ω.

theorem Cslib.ωLanguage.omegaPow_coind' {α : Type u_1} {l : Language α} {p : ωLanguage α} [Inhabited α] (h_nn : [] ∉ l) (h_le : p ≤ l * p) : p ≤ l^ω

theorem Cslib.ωLanguage.omegaPow_coind {α : Type u_1} {l : Language α} {p : ωLanguage α} [Inhabited α] (h_le : p ≤ (l - 1) * p) : p ≤ l^ω

A "coinductive" rule for proving p is a subset of l^ω.

theorem Cslib.ωLanguage.omegaPow_le_hmul_omegaPow' {α : Type u_1} [Inhabited α] (l : Language α) : l^ω ≤ (l - 1) * l^ω

theorem Cslib.ωLanguage.omegaPow_le_hmul_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : l^ω ≤ l * l^ω

theorem Cslib.ωLanguage.hmul_omegaPow_le_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : l * l^ω ≤ l^ω

@[simp]

theorem Cslib.ωLanguage.hmul_omegaPow_eq_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : l * l^ω = l^ω

theorem Cslib.ωLanguage.omegaPow_le_kstar_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : l^ω ≤ (KStar.kstar l)^ω

theorem Cslib.ωLanguage.kstar_omegaPow_le_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : (KStar.kstar l)^ω ≤ l^ω

@[simp]

theorem Cslib.ωLanguage.kstar_omegaPow_eq_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : (KStar.kstar l)^ω = l^ω

@[simp]

theorem Cslib.ωLanguage.kstar_hmul_omegaPow_eq_omegaPow {α : Type u_1} [Inhabited α] (l : Language α) : KStar.kstar l * l^ω = l^ω

@[simp]

theorem Cslib.ωLanguage.omegaLim_zero {α : Type u_1} : 0↗ω = ⊥

@[simp]

theorem Cslib.ωLanguage.map_id {α : Type u_1} (p : ωLanguage α) : map id p = p

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