feat: add Cslib/Computability/Languages/OmegaLanguage.lean

Cslib.lean

@@ -1,8 +1,51 @@
+import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.DFA
+import Cslib.Computability.Automata.DFAToNFA
+import Cslib.Computability.Automata.EpsilonNFA
+import Cslib.Computability.Automata.EpsilonNFAToNFA
+import Cslib.Computability.Automata.NA
+import Cslib.Computability.Automata.NFA
+import Cslib.Computability.Automata.NFAToDFA
+import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Foundations.Control.Monad.Free
+import Cslib.Foundations.Control.Monad.Free.Effects
+import Cslib.Foundations.Control.Monad.Free.Fold
+import Cslib.Foundations.Data.FinFun
+import Cslib.Foundations.Data.HasFresh
+import Cslib.Foundations.Data.OmegaSequence.Defs
+import Cslib.Foundations.Data.OmegaSequence.Init
+import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.Simulation
 import Cslib.Foundations.Semantics.LTS.TraceEq
-import Cslib.Foundations.Data.Relation
-import Cslib.Languages.CombinatoryLogic.Defs
+import Cslib.Foundations.Semantics.ReductionSystem.Basic
+import Cslib.Foundations.Syntax.HasAlphaEquiv
+import Cslib.Foundations.Syntax.HasSubstitution
+import Cslib.Foundations.Syntax.HasWellFormed
+import Cslib.Languages.CCS.Basic
+import Cslib.Languages.CCS.BehaviouralTheory
+import Cslib.Languages.CCS.Semantics
 import Cslib.Languages.CombinatoryLogic.Basic
+import Cslib.Languages.CombinatoryLogic.Confluence
+import Cslib.Languages.CombinatoryLogic.Defs
+import Cslib.Languages.CombinatoryLogic.Recursion
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 import Cslib.Logics.LinearLogic.CLL.Basic
+import Cslib.Logics.LinearLogic.CLL.CutElimination
+import Cslib.Logics.LinearLogic.CLL.MProof
 import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic

Cslib/Computability/Languages/OmegaLanguage.lean

@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2025-present Ching-Tsun Chou All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+import Cslib.Foundations.Data.OmegaSequence.Init
+import Mathlib.Computability.Language
+import Mathlib.Order.Filter.AtTopBot.Defs
+import Mathlib.Tactic
+
+/-!
+# ω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 α`.
+
+## 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 α`).
+
+* `p ∪ q`, `p ∩ q`, `pᶜ`, `∅`: the usual set operations.
+* `l * p`: ω-language of `x ++ω y` where `x ∈ l` and `y ∈ p`.
+* `l ^ω`: ω-language of infinite sequences each of which is the concatenation of
+  infinitely many (non-nil) members of `l`.
+* `l ↗ω`: ω-language of infinite sequences each of which has infinitely many
+  prefixes in `l`.
+
+## Main definitions
+
+* `ωLanguage α`: a set of infinite sequences over the alphabet `α`
+* `p.map f`: transform an ω-language `p` over `α` into an ω-language over `β`
+  by translating through `f : α → β`
+
+## Main theorems
+
+-/
+
+open List Set Filter Computability
+
+universe v
+
+variable {α β γ : Type*}
+
+/-- An ω-language is a set of strings over an alphabet. -/
+def ωLanguage (α) :=
+  Set (ωSequence α)
+
+namespace ωLanguage
+
+instance : Membership (ωSequence α) (ωLanguage α) := ⟨Set.Mem⟩
+instance : Singleton (ωSequence α) (ωLanguage α) := ⟨Set.singleton⟩
+instance : Insert (ωSequence α) (ωLanguage α) := ⟨Set.insert⟩
+instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (ωLanguage α) :=
+  Set.instCompleteAtomicBooleanAlgebra
+
+variable {l m : Language α} {p q : ωLanguage α} {a b x : List α} {s t : ωSequence α}
+
+instance : Inhabited (ωLanguage α) := ⟨(∅ : Set _)⟩
+
+/-- ω-language ∅ has no elements. -/
+instance : EmptyCollection (ωLanguage α) :=
+  ⟨(∅ : Set _)⟩
+
+theorem empty_def : (∅ : ωLanguage α) = (∅ : Set (ωSequence α)) :=
+  rfl
+
+/-- The union of two ω-languages. -/
+instance : Union (ωLanguage α) :=
+  ⟨((· ∪ ·) : Set (ωSequence α) → Set (ωSequence α) → Set (ωSequence α))⟩
+
+theorem union_def (p q : ωLanguage α) : p ∪ q = (p ∪ q : Set (ωSequence α)) :=
+  rfl
+
+/-- The intersection of two ω-languages. -/
+instance : Inter (ωLanguage α) :=
+  ⟨((· ∩ ·) : Set (ωSequence α) → Set (ωSequence α) → Set (ωSequence α))⟩
+
+theorem inter_def (p q : ωLanguage α) : p ∩ q = (p ∩ q : Set (ωSequence α)) :=
+  rfl
+
+theorem compl_def (p : ωLanguage α) : pᶜ = (pᶜ : Set (ωSequence α)) :=
+  rfl
+
+/-- The product of a language l and an ω-language `p` is the ω-language made of
+infinite sequences `x ++ω y` where `x ∈ l` and `y ∈ p`. -/
+instance : HMul (Language α) (ωLanguage α) (ωLanguage α) :=
+  ⟨image2 (· ++ω ·)⟩
+
+theorem hmul_def (l : Language α) (p : ωLanguage α) : l * p = image2 (· ++ω ·) l p :=
+  rfl
+
+/-- Concatenation of infinitely many copies of a languages, resulting in an ω-language.
+A.k.a. ω-power.
+-/
+def omegaPower (l : Language α) : ωLanguage α :=
+  { s | ∃ φ : ωSequence ℕ, StrictMono φ ∧ φ 0 = 0 ∧ ∀ m, s.extract (φ m) (φ (m + 1)) ∈ l }
+
+/-- Use the postfix notation ^ω` for `omegaPower`. -/
+@[notation_class]
+class OmegaPower (α : Type*) (β : outParam (Type*)) where
+  omegaPower : α → β
+
+postfix:1024 "^ω" => OmegaPower.omegaPower
+
+instance : OmegaPower (Language α) (ωLanguage α) :=
+  { omegaPower := omegaPower }
+
+theorem omegaPower_def (l : Language α) :
+    l^ω = { s | ∃ φ : ωSequence ℕ, StrictMono φ ∧ φ 0 = 0 ∧ ∀ m, s.extract (φ m) (φ (m + 1)) ∈ l }
+  := rfl
+
+/- The ω-limit of a language `l` is the ω-language of infinite sequences each of which
+contains infinitely many prefixes in `l`.
+-/
+def omegaLimit (l : Language α) : ωLanguage α :=
+  { s | ∃ᶠ m in atTop, s.extract 0 m ∈ l }
+
+/-- Use the postfix notation ↗ω` for `omegaLimit`. -/
+@[notation_class]
+class OmegaLimit (α : Type*) (β : outParam (Type*)) where
+  omegaLimit : α → β
+
+postfix:1024 "↗ω" => OmegaLimit.omegaLimit
+
+instance instOmegaLimit : OmegaLimit (Language α) (ωLanguage α) :=
+  { omegaLimit := omegaLimit }
+
+theorem omegaLimit_def (l : Language α) :
+    l↗ω = { s | ∃ᶠ m in atTop, s.extract 0 m ∈ l } :=
+  rfl
+
+def map (f : α → β) : ωLanguage α → ωLanguage β := image (ωSequence.map f)
+
+theorem map_def (f : α → β) (p : ωLanguage α) :
+    p.map f = image (ωSequence.map f) p :=
+  rfl
+
+@[ext]
+theorem ext (h : ∀ (s : ωSequence α), s ∈ p ↔ s ∈ q) : p = q :=
+  Set.ext h
+
+@[simp]
+theorem notMem_empty (s : ωSequence α) : s ∉ (∅ : ωLanguage α) :=
+  id
+
+@[simp]
+theorem mem_union (p q : ωLanguage α) (s : ωSequence α) : s ∈ p ∪ q ↔ s ∈ p ∨ s ∈ q :=
+  Iff.rfl
+
+@[simp]
+theorem mem_inter (p q : ωLanguage α) (s : ωSequence α) : s ∈ p ∩ q ↔ s ∈ p ∧ s ∈ q :=
+  Iff.rfl
+
+@[simp]
+theorem mem_compl (p : ωLanguage α) (s : ωSequence α) : s ∈ pᶜ ↔ ¬ s ∈ p :=
+  Iff.rfl
+
+theorem mem_hmul : s ∈ l * p ↔ ∃ x ∈ l, ∃ t ∈ p, x ++ω t = s :=
+  mem_image2
+
+theorem append_mem_hmul : x ∈ l → s ∈ p → x ++ω s ∈ l * p :=
+  mem_image2_of_mem
+
+@[simp]
+theorem map_id (p : ωLanguage α) : map id p = p :=
+  by simp [map]
+
+@[simp]
+theorem map_map (g : β → γ) (f : α → β) (p : ωLanguage α) : map g (map f p) = map (g ∘ f) p := by
+  simp [map, image_image]
+
+end ωLanguage

Cslib/Foundations/Data/OmegaSequence/Defs.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2025-present Ching-Tsun Chou All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+import Mathlib.Data.Nat.Notation
+
+/-!
+# Definition of `ωSequence` and functions on infinite sequences
+
+An `ωSequence α` is an infinite sequence of elements of `α`.  It is basically
+a wrapper around the type `ℕ → α` which supports the dot-notation and
+the analogues of many familiar API functions of `List α`.  In particular,
+the element at postion `n : ℕ` of `s : ωSequence α` is obtained using the
+function application notation `s n`.
+
+In this file we define `ωSequence` and its API functions.
+Most code below is adapted from Mathlib.Data.Stream.Defs.
+-/
+
+universe u v w
+variable {α : Type u} {β : Type v} {δ : Type w}
+
+/-- An `ωSequence α` is an infinite sequence of elements of `α`. -/
+def ωSequence (α : Type u) := ℕ → α
+
+namespace ωSequence
+
+/-- Head of an ω-sequence: `ωSequence.head s = ωSequence s 0`. -/
+abbrev head (s : ωSequence α) : α := s 0
+
+/-- Tail of an ω-sequence: `ωSequence.tail (h :: t) = t`. -/
+def tail (s : ωSequence α) : ωSequence α := fun i => s (i + 1)
+
+/-- Drop first `n` elements of an ω-sequence. -/
+def drop (n : ℕ) (s : ωSequence α) : ωSequence α := fun i => s (i + n)
+
+/-- `take n s` returns a list of the `n` first elements of ω-sequence `s` -/
+def take : ℕ → ωSequence α → List α
+  | 0, _ => []
+  | n + 1, s => List.cons (head s) (take n (tail s))
+
+/-- Get the list containing the elements of `xs` from position `m` to `n - 1`. -/
+def extract (xs : ωSequence α) (m n : ℕ) : List α :=
+  take (n - m) (xs.drop m)
+
+/-- Prepend an element to an ω-sequence. -/
+def cons (a : α) (s : ωSequence α) : ωSequence α
+  | 0 => a
+  | n + 1 => s n
+
+@[inherit_doc] scoped infixr:67 " ::ω " => cons
+
+/-- Append an ω-sequence to a list. -/
+def appendωSequence : List α → ωSequence α → ωSequence α
+  | [], s => s
+  | List.cons a l, s => a ::ω appendωSequence l s
+
+@[inherit_doc] infixl:65 " ++ω " => appendωSequence
+
+/-- The constant ω-sequence: `ωSequence n (ωSequence.const a) = a`. -/
+def const (a : α) : ωSequence α := fun _ => a
+
+/-- Apply a function `f` to all elements of an ω-sequence `s`. -/
+def map (f : α → β) (s : ωSequence α) : ωSequence β := fun n => f (s n)
+
+/-- Zip two ω-sequences using a binary operation:
+`ωSequence n (ωSequence.zip f s₁ s₂) = f (ωSequence s₁) (ωSequence s₂)`. -/
+def zip (f : α → β → δ) (s₁ : ωSequence α) (s₂ : ωSequence β) : ωSequence δ :=
+  fun n => f (s₁ n) (s₂ n)
+
+/-- Iterates of a function as an ω-sequence. -/
+def iterate (f : α → α) (a : α) : ωSequence α
+  | 0 => a
+  | n + 1 => f (iterate f a n)
+
+end ωSequence