ω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 Cslib.ωLanguage (α : Type u_4) : Type u_4

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

Equations

• Cslib.ωLanguage α = Set (Cslib.ωSequence α)

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

Equations

• Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra = Set.instCompleteAtomicBooleanAlgebra

instance Cslib.ωLanguage.instMembershipωSequence {α : Type u_1} : Membership (ωSequence α) (ωLanguage α)

Equations

• Cslib.ωLanguage.instMembershipωSequence = { mem := Set.Mem }

instance Cslib.ωLanguage.instSingletonωSequence {α : Type u_1} : Singleton (ωSequence α) (ωLanguage α)

Equations

• Cslib.ωLanguage.instSingletonωSequence = { singleton := Set.singleton }

instance Cslib.ωLanguage.instInsertωSequence {α : Type u_1} : Insert (ωSequence α) (ωLanguage α)

Equations

• Cslib.ωLanguage.instInsertωSequence = { insert := Set.insert }

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

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

• Cslib.ωLanguage.instHMulLanguage = { hMul := Set.image2 fun (x1 : List α) (x2 : Cslib.ωSequence α) => x1 ++ω x2 }

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

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 = {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 "^ω")

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^ω = {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 = {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 "↗ω")

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↗ω = {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 = Set.image (Cslib.ωSequence.map f)

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

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

theorem Cslib.ωLanguage.ext_iff {α : Type u_1} {p q : ωLanguage α} : p = q ↔ ∀ (s : ωSequence α), s ∈ p ↔ s ∈ 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_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 = {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^ω = {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