From 54a452b0d0fe435e095809c64a47067a50a2a9ea Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Fri, 3 Oct 2025 14:57:22 -0700 Subject: [PATCH 1/3] feat: add Cslib/Foundations/Data/OmegaList/* --- Cslib.lean | 46 +- Cslib/Foundations/Data/OmegaList/Defs.lean | 172 +++++ Cslib/Foundations/Data/OmegaList/Init.lean | 701 +++++++++++++++++++++ CslibTests.lean | 8 + 4 files changed, 925 insertions(+), 2 deletions(-) create mode 100644 Cslib/Foundations/Data/OmegaList/Defs.lean create mode 100644 Cslib/Foundations/Data/OmegaList/Init.lean create mode 100644 CslibTests.lean diff --git a/Cslib.lean b/Cslib.lean index f5cbcfd0..8453b60e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,8 +1,50 @@ +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.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.OmegaList.Defs +import Cslib.Foundations.Data.OmegaList.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 diff --git a/Cslib/Foundations/Data/OmegaList/Defs.lean b/Cslib/Foundations/Data/OmegaList/Defs.lean new file mode 100644 index 00000000..7abf7d4b --- /dev/null +++ b/Cslib/Foundations/Data/OmegaList/Defs.lean @@ -0,0 +1,172 @@ +/- +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 `ωList` and functions on infinite lists + +An `ωList α` 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 this file we define `ωList` and some functions that +take and/or return ω-lists. + +Most code below is inherited from Mathlib.Data.Stream.Defs. +-/ + +universe u v w +variable {α : Type u} {β : Type v} {δ : Type w} + +/-- An `ωList α` is an infinite sequence of elements of `α`. -/ +def ωList (α : Type u) := ℕ → α + +namespace ωList + +/-- Prepend an element to an ω-list. -/ +def cons (a : α) (s : ωList α) : ωList α + | 0 => a + | n + 1 => s n + +@[inherit_doc] scoped infixr:67 " :: " => cons + +/-- Get the `n`-th element of an ω-list. -/ +def get (s : ωList α) (n : ℕ) : α := s n + +/-- Head of an ω-list: `ωList.head s = ωList.get s 0`. -/ +abbrev head (s : ωList α) : α := s.get 0 + +/-- Tail of an ω-list: `ωList.tail (h :: t) = t`. -/ +def tail (s : ωList α) : ωList α := fun i => s.get (i + 1) + +/-- Drop first `n` elements of an ω-list. -/ +def drop (n : ℕ) (s : ωList α) : ωList α := fun i => s.get (i + n) + +/-- Proposition saying that all elements of an ω-list satisfy a predicate. -/ +def All (p : α → Prop) (s : ωList α) := ∀ n, p (get s n) + +/-- Proposition saying that at least one element of an ω-list satisfies a predicate. -/ +def Any (p : α → Prop) (s : ωList α) := ∃ n, p (get s n) + +/-- `a ∈ s` means that `a = ωList.get n s` for some `n`. -/ +instance : Membership α (ωList α) := + ⟨fun s a => Any (fun b => a = b) s⟩ + +/-- Apply a function `f` to all elements of an ω-list `s`. -/ +def map (f : α → β) (s : ωList α) : ωList β := fun n => f (get s n) + +/-- Zip two ω-lists using a binary operation: +`ωList.get n (ωList.zip f s₁ s₂) = f (ωList.get s₁) (ωList.get s₂)`. -/ +def zip (f : α → β → δ) (s₁ : ωList α) (s₂ : ωList β) : ωList δ := + fun n => f (get s₁ n) (get s₂ n) + +/-- Enumerate an ω-list by tagging each element with its index. -/ +def enum (s : ωList α) : ωList (ℕ × α) := fun n => (n, s.get n) + +/-- The constant ω-list: `ωList.get n (ωList.const a) = a`. -/ +def const (a : α) : ωList α := fun _ => a + +/-- Iterates of a function as an ω-list. -/ +def iterate (f : α → α) (a : α) : ωList α + | 0 => a + | n + 1 => f (iterate f a n) + +/-- Given functions `f : α → β` and `g : α → α`, `corec f g` creates an ω-list by: +1. Starting with an initial value `a : α` +2. Applying `g` repeatedly to get an ω-list of α values +3. Applying `f` to each value to convert them to β +-/ +def corec (f : α → β) (g : α → α) : α → ωList β := fun a => map f (iterate g a) + +/-- Given an initial value `a : α` and functions `f : α → β` and `g : α → α`, +`corecOn a f g` creates an ω-list by repeatedly: +1. Applying `f` to the current value to get the next ω-list element +2. Applying `g` to get the next value to process +This is equivalent to `corec f g a`. -/ +def corecOn (a : α) (f : α → β) (g : α → α) : ωList β := + corec f g a + +/-- Given a function `f : α → β × α`, `corec' f` creates an ω-list by repeatedly: +1. Starting with an initial value `a : α` +2. Applying `f` to get both the next ω-list element (β) and next state value (α) +This is a more convenient form when the next element and state are computed together. -/ +def corec' (f : α → β × α) : α → ωList β := + corec (Prod.fst ∘ f) (Prod.snd ∘ f) + +/-- Use a state monad to generate an ω-list through corecursion -/ +def corecState {σ α} (cmd : StateM σ α) (s : σ) : ωList α := + corec Prod.fst (cmd.run ∘ Prod.snd) (cmd.run s) + +-- corec is also known as unfolds +abbrev unfolds (g : α → β) (f : α → α) (a : α) : ωList β := + corec g f a + +/-- Interleave two ω-lists. -/ +def interleave (s₁ s₂ : ωList α) : ωList α := + corecOn (s₁, s₂) (fun ⟨s₁, _⟩ => head s₁) fun ⟨s₁, s₂⟩ => (s₂, tail s₁) + +@[inherit_doc] infixl:65 " ⋈ " => interleave + +/-- Elements of an ω-list with even indices. -/ +def even (s : ωList α) : ωList α := + corec head (fun s => tail (tail s)) s + +/-- Elements of an ω-list with odd indices. -/ +def odd (s : ωList α) : ωList α := + even (tail s) + +/-- Append an ω-list to a list. -/ +def appendωList : List α → ωList α → ωList α + | [], s => s + | List.cons a l, s => a::appendωList l s + +@[inherit_doc] infixl:65 " ++ₛ " => appendωList + +/-- `take n s` returns a list of the `n` first elements of ω-list `s` -/ +def take : ℕ → ωList α → List α + | 0, _ => [] + | n + 1, s => List.cons (head s) (take n (tail s)) + +/-- An auxiliary definition for `ωList.cycle` corecursive def -/ +protected def cycleF : α × List α × α × List α → α + | (v, _, _, _) => v + +/-- An auxiliary definition for `ωList.cycle` corecursive def -/ +protected def cycleG : α × List α × α × List α → α × List α × α × List α + | (_, [], v₀, l₀) => (v₀, l₀, v₀, l₀) + | (_, List.cons v₂ l₂, v₀, l₀) => (v₂, l₂, v₀, l₀) + +/-- Interpret a nonempty list as a cyclic ω-list. -/ +def cycle : ∀ l : List α, l ≠ [] → ωList α + | [], h => absurd rfl h + | List.cons a l, _ => corec ωList.cycleF ωList.cycleG (a, l, a, l) + +/-- Tails of an ω-list, starting with `ωList.tail s`. -/ +def tails (s : ωList α) : ωList (ωList α) := + corec id tail (tail s) + +/-- An auxiliary definition for `ωList.inits`. -/ +def initsCore (l : List α) (s : ωList α) : ωList (List α) := + corecOn (l, s) (fun ⟨a, _⟩ => a) fun p => + match p with + | (l', s') => (l' ++ [head s'], tail s') + +/-- Nonempty initial segments of an ω-list. -/ +def inits (s : ωList α) : ωList (List α) := + initsCore [head s] (tail s) + +/-- A constant ω-list, same as `ωList.const`. -/ +def pure (a : α) : ωList α := + const a + +/-- Given an ω-list of functions and an ω-list of values, apply `n`-th function to `n`-th value. -/ +def apply (f : ωList (α → β)) (s : ωList α) : ωList β := fun n => (get f n) (get s n) + +@[inherit_doc] infixl:75 " ⊛ " => apply -- input as `\circledast` + +/-- The ω-list of natural numbers: `ωList.get n ωList.nats = n`. -/ +def nats : ωList ℕ := fun n => n + +end ωList diff --git a/Cslib/Foundations/Data/OmegaList/Init.lean b/Cslib/Foundations/Data/OmegaList/Init.lean new file mode 100644 index 00000000..58c60791 --- /dev/null +++ b/Cslib/Foundations/Data/OmegaList/Init.lean @@ -0,0 +1,701 @@ +/- +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.OmegaList.Defs +import Mathlib.Logic.Function.Basic +import Mathlib.Data.Nat.Basic +import Mathlib.Tactic.Common + +/-! +# ω-lists a.k.a. infinite lists a.k.a. infinite sequences + +Most code below is inherited from Mathlib.Data.Stream.Init. +-/ + +open Nat Function Option + +namespace ωList + +universe u v w +variable {α : Type u} {β : Type v} {δ : Type w} +variable (m n : ℕ) (x y : List α) (a b : ωList α) + +instance [Inhabited α] : Inhabited (ωList α) := + ⟨ωList.const default⟩ + +@[simp] protected theorem eta (s : ωList α) : head s :: tail s = s := + funext fun i => by cases i <;> rfl + +/-- Alias for `ωList.eta` to match `List` API. -/ +alias cons_head_tail := ωList.eta + +@[ext] +protected theorem ext {s₁ s₂ : ωList α} : (∀ n, get s₁ n = get s₂ n) → s₁ = s₂ := + fun h => funext h + +@[simp] +theorem get_zero_cons (a : α) (s : ωList α) : get (a::s) 0 = a := + rfl + +@[simp] +theorem head_cons (a : α) (s : ωList α) : head (a::s) = a := + rfl + +@[simp] +theorem tail_cons (a : α) (s : ωList α) : tail (a::s) = s := + rfl + +@[simp] +theorem get_drop (n m : ℕ) (s : ωList α) : get (drop m s) n = get s (m + n) := by + rw [Nat.add_comm] + rfl + +theorem tail_eq_drop (s : ωList α) : tail s = drop 1 s := + rfl + +@[simp] +theorem drop_drop (n m : ℕ) (s : ωList α) : drop n (drop m s) = drop (m + n) s := by + ext; simp [Nat.add_assoc] + +@[simp] theorem get_tail {n : ℕ} {s : ωList α} : s.tail.get n = s.get (n + 1) := rfl + +@[simp] theorem tail_drop' {i : ℕ} {s : ωList α} : tail (drop i s) = s.drop (i + 1) := by + ext; simp [Nat.add_comm, Nat.add_left_comm] + +@[simp] theorem drop_tail' {i : ℕ} {s : ωList α} : drop i (tail s) = s.drop (i + 1) := rfl + +theorem tail_drop (n : ℕ) (s : ωList α) : tail (drop n s) = drop n (tail s) := by simp + +theorem get_succ (n : ℕ) (s : ωList α) : get s (succ n) = get (tail s) n := + rfl + +@[simp] +theorem get_succ_cons (n : ℕ) (s : ωList α) (x : α) : get (x :: s) n.succ = get s n := + rfl + +@[simp] lemma get_cons_append_zero {a : α} {x : List α} {s : ωList α} : + (a :: x ++ₛ s).get 0 = a := rfl + +@[simp] lemma append_eq_cons {a : α} {as : ωList α} : [a] ++ₛ as = a :: as := rfl + +@[simp] theorem drop_zero {s : ωList α} : s.drop 0 = s := rfl + +theorem drop_succ (n : ℕ) (s : ωList α) : drop (succ n) s = drop n (tail s) := + rfl + +theorem head_drop (a : ωList α) (n : ℕ) : (a.drop n).head = a.get n := by simp + +theorem cons_injective2 : Function.Injective2 (cons : α → ωList α → ωList α) := fun x y s t h => + ⟨by rw [← get_zero_cons x s, h, get_zero_cons], + ωList.ext fun n => by rw [← get_succ_cons n _ x, h, get_succ_cons]⟩ + +theorem cons_injective_left (s : ωList α) : Function.Injective fun x => cons x s := + cons_injective2.left _ + +theorem cons_injective_right (x : α) : Function.Injective (cons x) := + cons_injective2.right _ + +theorem all_def (p : α → Prop) (s : ωList α) : All p s = ∀ n, p (get s n) := + rfl + +theorem any_def (p : α → Prop) (s : ωList α) : Any p s = ∃ n, p (get s n) := + rfl + +@[simp] +theorem mem_cons (a : α) (s : ωList α) : a ∈ a::s := + Exists.intro 0 rfl + +theorem mem_cons_of_mem {a : α} {s : ωList α} (b : α) : a ∈ s → a ∈ b::s := fun ⟨n, h⟩ => + Exists.intro (succ n) (by rw [get_succ, tail_cons, h]) + +theorem eq_or_mem_of_mem_cons {a b : α} {s : ωList α} : (a ∈ b::s) → a = b ∨ a ∈ s := + fun ⟨n, h⟩ => by + rcases n with - | n' + · left + exact h + · right + rw [get_succ, tail_cons] at h + exact ⟨n', h⟩ + +theorem mem_of_get_eq {n : ℕ} {s : ωList α} {a : α} : a = get s n → a ∈ s := fun h => + Exists.intro n h + +theorem mem_iff_exists_get_eq {s : ωList α} {a : α} : a ∈ s ↔ ∃ n, a = s.get n where + mp := by simp [Membership.mem, any_def] + mpr h := mem_of_get_eq h.choose_spec + +section Map + +variable (f : α → β) + +theorem drop_map (n : ℕ) (s : ωList α) : drop n (map f s) = map f (drop n s) := + ωList.ext fun _ => rfl + +@[simp] +theorem get_map (n : ℕ) (s : ωList α) : get (map f s) n = f (get s n) := + rfl + +theorem tail_map (s : ωList α) : tail (map f s) = map f (tail s) := rfl + +@[simp] +theorem head_map (s : ωList α) : head (map f s) = f (head s) := + rfl + +theorem map_eq (s : ωList α) : map f s = f (head s)::map f (tail s) := by + rw [← ωList.eta (map f s), tail_map, head_map] + +theorem map_cons (a : α) (s : ωList α) : map f (a::s) = f a::map f s := by + rw [← ωList.eta (map f (a::s)), map_eq]; rfl + +@[simp] +theorem map_id (s : ωList α) : map id s = s := + rfl + +@[simp] +theorem map_map (g : β → δ) (f : α → β) (s : ωList α) : map g (map f s) = map (g ∘ f) s := + rfl + +@[simp] +theorem map_tail (s : ωList α) : map f (tail s) = tail (map f s) := + rfl + +theorem mem_map {a : α} {s : ωList α} : a ∈ s → f a ∈ map f s := fun ⟨n, h⟩ => + Exists.intro n (by rw [get_map, h]) + +theorem exists_of_mem_map {f} {b : β} {s : ωList α} : b ∈ map f s → ∃ a, a ∈ s ∧ f a = b := + fun ⟨n, h⟩ => ⟨get s n, ⟨n, rfl⟩, h.symm⟩ + +end Map + +section Zip + +variable (f : α → β → δ) + +theorem drop_zip (n : ℕ) (s₁ : ωList α) (s₂ : ωList β) : + drop n (zip f s₁ s₂) = zip f (drop n s₁) (drop n s₂) := + ωList.ext fun _ => rfl + +@[simp] +theorem get_zip (n : ℕ) (s₁ : ωList α) (s₂ : ωList β) : + get (zip f s₁ s₂) n = f (get s₁ n) (get s₂ n) := + rfl + +theorem head_zip (s₁ : ωList α) (s₂ : ωList β) : head (zip f s₁ s₂) = f (head s₁) (head s₂) := + rfl + +theorem tail_zip (s₁ : ωList α) (s₂ : ωList β) : + tail (zip f s₁ s₂) = zip f (tail s₁) (tail s₂) := + rfl + +theorem zip_eq (s₁ : ωList α) (s₂ : ωList β) : + zip f s₁ s₂ = f (head s₁) (head s₂)::zip f (tail s₁) (tail s₂) := by + rw [← ωList.eta (zip f s₁ s₂)]; rfl + +@[simp] +theorem get_enum (s : ωList α) (n : ℕ) : get (enum s) n = (n, s.get n) := + rfl + +theorem enum_eq_zip (s : ωList α) : enum s = zip Prod.mk nats s := + rfl + +end Zip + +@[simp] +theorem mem_const (a : α) : a ∈ const a := + Exists.intro 0 rfl + +theorem const_eq (a : α) : const a = a::const a := by + apply ωList.ext; intro n + cases n <;> rfl + +@[simp] +theorem tail_const (a : α) : tail (const a) = const a := + suffices tail (a::const a) = const a by rwa [← const_eq] at this + rfl + +@[simp] +theorem map_const (f : α → β) (a : α) : map f (const a) = const (f a) := + rfl + +@[simp] +theorem get_const (n : ℕ) (a : α) : get (const a) n = a := + rfl + +@[simp] +theorem drop_const (n : ℕ) (a : α) : drop n (const a) = const a := + ωList.ext fun _ => rfl + +@[simp] +theorem head_iterate (f : α → α) (a : α) : head (iterate f a) = a := + rfl + +theorem get_succ_iterate' (n : ℕ) (f : α → α) (a : α) : + get (iterate f a) (succ n) = f (get (iterate f a) n) := rfl + +theorem tail_iterate (f : α → α) (a : α) : tail (iterate f a) = iterate f (f a) := by + ext n + rw [get_tail] + induction n with + | zero => rfl + | succ n ih => rw [get_succ_iterate', ih, get_succ_iterate'] + +theorem iterate_eq (f : α → α) (a : α) : iterate f a = a::iterate f (f a) := by + rw [← ωList.eta (iterate f a)] + rw [tail_iterate]; rfl + +@[simp] +theorem get_zero_iterate (f : α → α) (a : α) : get (iterate f a) 0 = a := + rfl + +theorem get_succ_iterate (n : ℕ) (f : α → α) (a : α) : + get (iterate f a) (succ n) = get (iterate f (f a)) n := by rw [get_succ, tail_iterate] + +section Bisim + +variable (R : ωList α → ωList α → Prop) + +/-- equivalence relation -/ +local infixl:50 " ~ " => R + +/-- ω-lists `s₁` and `s₂` are defined to be bisimulations if +their heads are equal and tails are bisimulations. -/ +def IsBisimulation := + ∀ ⦃s₁ s₂⦄, s₁ ~ s₂ → + head s₁ = head s₂ ∧ tail s₁ ~ tail s₂ + +theorem get_of_bisim (bisim : IsBisimulation R) {s₁ s₂} : + ∀ n, s₁ ~ s₂ → get s₁ n = get s₂ n ∧ drop (n + 1) s₁ ~ drop (n + 1) s₂ + | 0, h => bisim h + | n + 1, h => + match bisim h with + | ⟨_, trel⟩ => get_of_bisim bisim n trel + +-- If two ω-lists are bisimilar, then they are equal +theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} : s₁ ~ s₂ → s₁ = s₂ := fun r => + ωList.ext fun n => And.left (get_of_bisim R bisim n r) + +end Bisim + +theorem bisim_simple (s₁ s₂ : ωList α) : + head s₁ = head s₂ → s₁ = tail s₁ → s₂ = tail s₂ → s₁ = s₂ := fun hh ht₁ ht₂ => + eq_of_bisim (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) + (fun s₁ s₂ ⟨h₁, h₂, h₃⟩ => by grind) + (And.intro hh (And.intro ht₁ ht₂)) + +theorem coinduction {s₁ s₂ : ωList α} : + head s₁ = head s₂ → + (∀ (β : Type u) (fr : ωList α → β), + fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂)) → s₁ = s₂ := + fun hh ht => + eq_of_bisim + (fun s₁ s₂ => + head s₁ = head s₂ ∧ + ∀ (β : Type u) (fr : ωList α → β), fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂)) + (fun s₁ s₂ h => + have h₁ : head s₁ = head s₂ := And.left h + have h₂ : head (tail s₁) = head (tail s₂) := And.right h α (@head α) h₁ + have h₃ : + ∀ (β : Type u) (fr : ωList α → β), + fr (tail s₁) = fr (tail s₂) → fr (tail (tail s₁)) = fr (tail (tail s₂)) := + fun β fr => And.right h β fun s => fr (tail s) + And.intro h₁ (And.intro h₂ h₃)) + (And.intro hh ht) + +@[simp] +theorem iterate_id (a : α) : iterate id a = const a := + coinduction rfl fun β fr ch => by rw [tail_iterate, tail_const]; exact ch + +theorem map_iterate (f : α → α) (a : α) : iterate f (f a) = map f (iterate f a) := by + funext n + induction n with + | zero => rfl + | succ n ih => + unfold map iterate get + rw [map, get] at ih + rw [iterate] + exact congrArg f ih + +section Corec + +theorem corec_def (f : α → β) (g : α → α) (a : α) : corec f g a = map f (iterate g a) := + rfl + +theorem corec_eq (f : α → β) (g : α → α) (a : α) : corec f g a = f a :: corec f g (g a) := by + rw [corec_def, map_eq, head_iterate, tail_iterate]; rfl + +theorem corec_id_id_eq_const (a : α) : corec id id a = const a := by + rw [corec_def, map_id, iterate_id] + +theorem corec_id_f_eq_iterate (f : α → α) (a : α) : corec id f a = iterate f a := + rfl + +end Corec + +section Corec' + +theorem corec'_eq (f : α → β × α) (a : α) : corec' f a = (f a).1 :: corec' f (f a).2 := + corec_eq _ _ _ + +end Corec' + +theorem unfolds_eq (g : α → β) (f : α → α) (a : α) : unfolds g f a = g a :: unfolds g f (f a) := by + unfold unfolds; rw [corec_eq] + +theorem get_unfolds_head_tail (n : ℕ) (s : ωList α) : get (unfolds head tail s) n = get s n := by + induction n generalizing s with + | zero => rfl + | succ n ih => rw [get_succ, get_succ, unfolds_eq, tail_cons, ih] + +theorem unfolds_head_eq : ∀ s : ωList α, unfolds head tail s = s := fun s => + ωList.ext fun n => get_unfolds_head_tail n s + +theorem interleave_eq (s₁ s₂ : ωList α) : s₁ ⋈ s₂ = head s₁::head s₂::(tail s₁ ⋈ tail s₂) := by + let t := tail s₁ ⋈ tail s₂ + change s₁ ⋈ s₂ = head s₁::head s₂::t + unfold interleave; unfold corecOn; rw [corec_eq]; dsimp; rw [corec_eq]; rfl + +theorem tail_interleave (s₁ s₂ : ωList α) : tail (s₁ ⋈ s₂) = s₂ ⋈ tail s₁ := by + unfold interleave corecOn; rw [corec_eq]; rfl + +theorem interleave_tail_tail (s₁ s₂ : ωList α) : tail s₁ ⋈ tail s₂ = tail (tail (s₁ ⋈ s₂)) := by + rw [interleave_eq s₁ s₂]; rfl + +theorem get_interleave_left : ∀ (n : ℕ) (s₁ s₂ : ωList α), + get (s₁ ⋈ s₂) (2 * n) = get s₁ n + | 0, _, _ => rfl + | n + 1, s₁, s₂ => by + change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n) + rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons] + rw [get_interleave_left n (tail s₁) (tail s₂)] + rfl + +theorem get_interleave_right : ∀ (n : ℕ) (s₁ s₂ : ωList α), + get (s₁ ⋈ s₂) (2 * n + 1) = get s₂ n + | 0, _, _ => rfl + | n + 1, s₁, s₂ => by + change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n) + rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons, + get_interleave_right n (tail s₁) (tail s₂)] + rfl + +theorem mem_interleave_left {a : α} {s₁ : ωList α} (s₂ : ωList α) : a ∈ s₁ → a ∈ s₁ ⋈ s₂ := + fun ⟨n, h⟩ => Exists.intro (2 * n) (by rw [h, get_interleave_left]) + +theorem mem_interleave_right {a : α} {s₁ : ωList α} (s₂ : ωList α) : a ∈ s₂ → a ∈ s₁ ⋈ s₂ := + fun ⟨n, h⟩ => Exists.intro (2 * n + 1) (by rw [h, get_interleave_right]) + +theorem odd_eq (s : ωList α) : odd s = even (tail s) := + rfl + +@[simp] +theorem head_even (s : ωList α) : head (even s) = head s := + rfl + +theorem tail_even (s : ωList α) : tail (even s) = even (tail (tail s)) := by + unfold even + rw [corec_eq] + rfl + +theorem even_cons_cons (a₁ a₂ : α) (s : ωList α) : even (a₁::a₂::s) = a₁::even s := by + unfold even + rw [corec_eq]; rfl + +theorem even_tail (s : ωList α) : even (tail s) = odd s := + rfl + +theorem even_interleave (s₁ s₂ : ωList α) : even (s₁ ⋈ s₂) = s₁ := + eq_of_bisim (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) + (fun s₁' s₁ ⟨s₂, h₁⟩ => by + rw [h₁] + constructor + · rfl + · exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩) + (Exists.intro s₂ rfl) + +theorem interleave_even_odd (s₁ : ωList α) : even s₁ ⋈ odd s₁ = s₁ := + eq_of_bisim (fun s' s => s' = even s ⋈ odd s) + (fun s' s (h : s' = even s ⋈ odd s) => by + rw [h]; constructor + · rfl + · simp [odd_eq, odd_eq, tail_interleave, tail_even]) + rfl + +theorem get_even : ∀ (n : ℕ) (s : ωList α), get (even s) n = get s (2 * n) + | 0, _ => rfl + | succ n, s => by + change get (even s) (succ n) = get s (succ (succ (2 * n))) + rw [get_succ, get_succ, tail_even, get_even n]; rfl + +theorem get_odd : ∀ (n : ℕ) (s : ωList α), get (odd s) n = get s (2 * n + 1) := fun n s => by + rw [odd_eq, get_even]; rfl + +theorem mem_of_mem_even (a : α) (s : ωList α) : a ∈ even s → a ∈ s := fun ⟨n, h⟩ => + Exists.intro (2 * n) (by rw [h, get_even]) + +theorem mem_of_mem_odd (a : α) (s : ωList α) : a ∈ odd s → a ∈ s := fun ⟨n, h⟩ => + Exists.intro (2 * n + 1) (by rw [h, get_odd]) + +@[simp] theorem nil_append_ωList (s : ωList α) : appendωList [] s = s := + rfl + +theorem cons_append_ωList (a : α) (l : List α) (s : ωList α) : + appendωList (a::l) s = a::appendωList l s := + rfl + +@[simp] theorem append_append_ωList : ∀ (l₁ l₂ : List α) (s : ωList α), + l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s) + | [], _, _ => rfl + | List.cons a l₁, l₂, s => by + rw [List.cons_append, cons_append_ωList, cons_append_ωList, append_append_ωList l₁] + +lemma get_append_left (h : n < x.length) : (x ++ₛ a).get n = x[n] := by + induction x generalizing n with + | nil => simp at h + | cons b x ih => + rcases n with (_ | n) + · simp + · simp [ih n (by simpa using h), cons_append_ωList] + +@[simp] lemma get_append_right : (x ++ₛ a).get (x.length + n) = a.get n := by + induction x <;> simp [Nat.succ_add, *, cons_append_ωList] + +@[simp] lemma get_append_length : (x ++ₛ a).get x.length = a.get 0 := get_append_right 0 x a + +lemma append_right_injective (h : x ++ₛ a = x ++ₛ b) : a = b := by + ext n; replace h := congr_arg (fun a ↦ a.get (x.length + n)) h; simpa using h + +@[simp] lemma append_right_inj : x ++ₛ a = x ++ₛ b ↔ a = b := + ⟨append_right_injective x a b, by simp +contextual⟩ + +lemma append_left_injective (h : x ++ₛ a = y ++ₛ b) (hl : x.length = y.length) : x = y := by + apply List.ext_getElem hl + intros + rw [← get_append_left, ← get_append_left, h] + +theorem map_append_ωList (f : α → β) : + ∀ (l : List α) (s : ωList α), map f (l ++ₛ s) = List.map f l ++ₛ map f s + | [], _ => rfl + | List.cons a l, s => by + rw [cons_append_ωList, List.map_cons, map_cons, cons_append_ωList, map_append_ωList f l] + +theorem drop_append_ωList : ∀ (l : List α) (s : ωList α), drop l.length (l ++ₛ s) = s + | [], s => rfl + | List.cons a l, s => by + rw [List.length_cons, drop_succ, cons_append_ωList, tail_cons, drop_append_ωList l s] + +theorem append_ωList_head_tail (s : ωList α) : [head s] ++ₛ tail s = s := by + simp + +theorem mem_append_ωList_right : ∀ {a : α} (l : List α) {s : ωList α}, a ∈ s → a ∈ l ++ₛ s + | _, [], _, h => h + | a, List.cons _ l, s, h => + have ih : a ∈ l ++ₛ s := mem_append_ωList_right l h + mem_cons_of_mem _ ih + +theorem mem_append_ωList_left : ∀ {a : α} {l : List α} (s : ωList α), a ∈ l → a ∈ l ++ₛ s + | _, [], _, h => absurd h List.not_mem_nil + | a, List.cons b l, s, h => + Or.elim (List.eq_or_mem_of_mem_cons h) (fun aeqb : a = b => Exists.intro 0 aeqb) + fun ainl : a ∈ l => mem_cons_of_mem b (mem_append_ωList_left s ainl) + +@[simp] +theorem take_zero (s : ωList α) : take 0 s = [] := + rfl + +-- This lemma used to be simp, but we removed it from the simp set because: +-- 1) It duplicates the (often large) `s` term, resulting in large tactic states. +-- 2) It conflicts with the very useful `dropLast_take` lemma below (causing nonconfluence). +theorem take_succ (n : ℕ) (s : ωList α) : take (succ n) s = head s::take n (tail s) := + rfl + +@[simp] theorem take_succ_cons {a : α} (n : ℕ) (s : ωList α) : + take (n+1) (a::s) = a :: take n s := rfl + +theorem take_succ' {s : ωList α} : ∀ n, s.take (n+1) = s.take n ++ [s.get n] + | 0 => rfl + | n+1 => by rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail] + +@[simp] +theorem length_take (n : ℕ) (s : ωList α) : (take n s).length = n := by + induction n generalizing s <;> simp [*, take_succ] + +@[simp] +theorem take_take {s : ωList α} : ∀ {m n}, (s.take n).take m = s.take (min n m) + | 0, n => by rw [Nat.min_zero, List.take_zero, take_zero] + | m, 0 => by rw [Nat.zero_min, take_zero, List.take_nil] + | m+1, n+1 => by rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take] + +@[simp] theorem concat_take_get {n : ℕ} {s : ωList α} : s.take n ++ [s.get n] = s.take (n + 1) := + (take_succ' n).symm + +theorem getElem?_take {s : ωList α} : ∀ {k n}, k < n → (s.take n)[k]? = s.get k + | 0, _+1, _ => by simp only [length_take, zero_lt_succ, List.getElem?_eq_getElem]; rfl + | k+1, n+1, h => by + rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ] + +theorem getElem?_take_succ (n : ℕ) (s : ωList α) : + (take (succ n) s)[n]? = some (get s n) := + getElem?_take (Nat.lt_succ_self n) + +@[simp] theorem dropLast_take {n : ℕ} {xs : ωList α} : + (ωList.take n xs).dropLast = ωList.take (n-1) xs := by + cases n with + | zero => simp + | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one] + +@[simp] +theorem append_take_drop (n : ℕ) (s : ωList α) : appendωList (take n s) (drop n s) = s := by + induction n generalizing s with + | zero => rfl + | succ n ih =>rw [take_succ, drop_succ, cons_append_ωList, ih (tail s), ωList.eta] + +lemma append_take : x ++ (a.take n) = (x ++ₛ a).take (x.length + n) := by + induction x <;> simp [take, Nat.add_comm, cons_append_ωList, *] + +@[simp] lemma take_get (h : m < (a.take n).length) : (a.take n)[m] = a.get m := by + nth_rw 2 [← append_take_drop n a]; rw [get_append_left] + +theorem take_append_of_le_length (h : n ≤ x.length) : + (x ++ₛ a).take n = x.take n := by + apply List.ext_getElem (by simp [h]) + intro _ _ _; rw [List.getElem_take, take_get, get_append_left] + +lemma take_add : a.take (m + n) = a.take m ++ (a.drop m).take n := by + apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n) <;> + simp [- drop_drop] + +@[gcongr] lemma take_prefix_take_left (h : m ≤ n) : a.take m <+: a.take n := by + rw [(by simp [h] : a.take m = (a.take n).take m)] + apply List.take_prefix + +@[simp] lemma take_prefix : a.take m <+: a.take n ↔ m ≤ n := + ⟨fun h ↦ by simpa using h.length_le, take_prefix_take_left m n a⟩ + +lemma map_take (f : α → β) : (a.take n).map f = (a.map f).take n := by + apply List.ext_getElem <;> simp + +lemma take_drop : (a.drop m).take n = (a.take (m + n)).drop m := by + apply List.ext_getElem <;> simp + +lemma drop_append_of_le_length (h : n ≤ x.length) : + (x ++ₛ a).drop n = x.drop n ++ₛ a := by + obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h + ext k; rcases lt_or_ge k m with _ | hk + · rw [get_drop, get_append_left, get_append_left, List.getElem_drop]; simpa [hm] + · obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk + have hm' : m = (x.drop n).length := by simp [hm] + simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right] + +-- Take theorem reduces a proof of equality of infinite ω-lists to an +-- induction over all their finite approximations. +theorem take_theorem (s₁ s₂ : ωList α) (h : ∀ n : ℕ, take n s₁ = take n s₂) : s₁ = s₂ := by + ext n + induction n with + | zero => simpa [take] using h 1 + | succ n => + have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by + rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))] + injection h₁ + +protected theorem cycle_g_cons (a : α) (a₁ : α) (l₁ : List α) (a₀ : α) (l₀ : List α) : + ωList.cycleG (a, a₁::l₁, a₀, l₀) = (a₁, l₁, a₀, l₀) := + rfl + +theorem cycle_eq : ∀ (l : List α) (h : l ≠ []), cycle l h = l ++ₛ cycle l h + | [], h => absurd rfl h + | List.cons a l, _ => + have gen (l' a') : corec ωList.cycleF ωList.cycleG (a', l', a, l) = + (a'::l') ++ₛ corec ωList.cycleF ωList.cycleG (a, l, a, l) := by + induction l' generalizing a' with + | nil => rw [corec_eq]; rfl + | cons a₁ l₁ ih => rw [corec_eq, ωList.cycle_g_cons, ih a₁]; rfl + gen l a + +theorem mem_cycle {a : α} {l : List α} : ∀ h : l ≠ [], a ∈ l → a ∈ cycle l h := fun h ainl => by + rw [cycle_eq]; exact mem_append_ωList_left _ ainl + +@[simp] +theorem cycle_singleton (a : α) : cycle [a] (by simp) = const a := + coinduction rfl fun β fr ch => by rwa [cycle_eq, const_eq] + +theorem tails_eq (s : ωList α) : tails s = tail s::tails (tail s) := by + unfold tails; rw [corec_eq]; rfl + +@[simp] +theorem get_tails (n : ℕ) (s : ωList α) : get (tails s) n = drop n (tail s) := by + induction n generalizing s with + | zero => rfl + | succ n ih => rw [get_succ, drop_succ, tails_eq, tail_cons, ih] + +theorem tails_eq_iterate (s : ωList α) : tails s = iterate tail (tail s) := + rfl + +theorem inits_core_eq (l : List α) (s : ωList α) : + initsCore l s = l::initsCore (l ++ [head s]) (tail s) := by + unfold initsCore corecOn + rw [corec_eq] + +theorem tail_inits (s : ωList α) : + tail (inits s) = initsCore [head s, head (tail s)] (tail (tail s)) := by + unfold inits + rw [inits_core_eq]; rfl + +theorem inits_tail (s : ωList α) : inits (tail s) = initsCore [head (tail s)] (tail (tail s)) := + rfl + +theorem cons_get_inits_core (a : α) (n : ℕ) (l : List α) (s : ωList α) : + (a :: get (initsCore l s) n) = get (initsCore (a :: l) s) n := by + induction n generalizing l s with + | zero => rfl + | succ n ih => + rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s] + rfl + +@[simp] +theorem get_inits (n : ℕ) (s : ωList α) : get (inits s) n = take (succ n) s := by + induction n generalizing s with + | zero => rfl + | succ n ih => rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core] + +theorem inits_eq (s : ωList α) : + inits s = [head s]::map (List.cons (head s)) (inits (tail s)) := by + apply ωList.ext; intro n + cases n + · rfl + · rw [get_inits, get_succ, tail_cons, get_map, get_inits] + rfl + +theorem zip_inits_tails (s : ωList α) : zip appendωList (inits s) (tails s) = const s := by + apply ωList.ext; intro n + rw [get_zip, get_inits, get_tails, get_const, take_succ, cons_append_ωList, append_take_drop, + ωList.eta] + +theorem identity (s : ωList α) : pure id ⊛ s = s := + rfl + +theorem composition (g : ωList (β → δ)) (f : ωList (α → β)) (s : ωList α) : + pure comp ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s) := + rfl + +theorem homomorphism (f : α → β) (a : α) : pure f ⊛ pure a = pure (f a) := + rfl + +theorem interchange (fs : ωList (α → β)) (a : α) : + fs ⊛ pure a = (pure fun f : α → β => f a) ⊛ fs := + rfl + +theorem map_eq_apply (f : α → β) (s : ωList α) : map f s = pure f ⊛ s := + rfl + +theorem get_nats (n : ℕ) : get nats n = n := + rfl + +theorem nats_eq : nats = cons 0 (map succ nats) := by + apply ωList.ext; intro n + cases n + · rfl + rw [get_succ]; rfl + +end ωList diff --git a/CslibTests.lean b/CslibTests.lean new file mode 100644 index 00000000..9aaa8875 --- /dev/null +++ b/CslibTests.lean @@ -0,0 +1,8 @@ +import CslibTests.Bisimulation +import CslibTests.CCS +import CslibTests.DFA +import CslibTests.FreeMonad +import CslibTests.HasFresh +import CslibTests.LTS +import CslibTests.LambdaCalculus +import CslibTests.ReductionSystem From 305b6a815ce53c405bd514e83ec710fc85606776 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Mon, 6 Oct 2025 16:50:09 -0700 Subject: [PATCH 2/3] feat: customize Cslib/Foundations/Data/OmegaList/* --- Cslib/Foundations/Data/OmegaList/Defs.lean | 42 ++-- Cslib/Foundations/Data/OmegaList/Init.lean | 271 ++++++++++++++------- 2 files changed, 211 insertions(+), 102 deletions(-) diff --git a/Cslib/Foundations/Data/OmegaList/Defs.lean b/Cslib/Foundations/Data/OmegaList/Defs.lean index 7abf7d4b..47709d6b 100644 --- a/Cslib/Foundations/Data/OmegaList/Defs.lean +++ b/Cslib/Foundations/Data/OmegaList/Defs.lean @@ -8,13 +8,14 @@ import Mathlib.Data.Nat.Notation /-! # Definition of `ωList` and functions on infinite lists -An `ωList α` 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 this file we define `ωList` and some functions that -take and/or return ω-lists. - -Most code below is inherited from Mathlib.Data.Stream.Defs. +An `ωList α` is an infinite sequence of elements of `α`. It isbasically +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 : ωList α` is obtained using the +function application notation `s n`. + +In this file we define `ωList` and its API functions. +Most code below is adapted from Mathlib.Data.Stream.Defs. -/ universe u v w @@ -32,38 +33,35 @@ def cons (a : α) (s : ωList α) : ωList α @[inherit_doc] scoped infixr:67 " :: " => cons -/-- Get the `n`-th element of an ω-list. -/ -def get (s : ωList α) (n : ℕ) : α := s n - /-- Head of an ω-list: `ωList.head s = ωList.get s 0`. -/ -abbrev head (s : ωList α) : α := s.get 0 +abbrev head (s : ωList α) : α := s 0 /-- Tail of an ω-list: `ωList.tail (h :: t) = t`. -/ -def tail (s : ωList α) : ωList α := fun i => s.get (i + 1) +def tail (s : ωList α) : ωList α := fun i => s (i + 1) /-- Drop first `n` elements of an ω-list. -/ -def drop (n : ℕ) (s : ωList α) : ωList α := fun i => s.get (i + n) +def drop (n : ℕ) (s : ωList α) : ωList α := fun i => s (i + n) /-- Proposition saying that all elements of an ω-list satisfy a predicate. -/ -def All (p : α → Prop) (s : ωList α) := ∀ n, p (get s n) +def All (p : α → Prop) (s : ωList α) := ∀ n, p (s n) /-- Proposition saying that at least one element of an ω-list satisfies a predicate. -/ -def Any (p : α → Prop) (s : ωList α) := ∃ n, p (get s n) +def Any (p : α → Prop) (s : ωList α) := ∃ n, p (s n) /-- `a ∈ s` means that `a = ωList.get n s` for some `n`. -/ instance : Membership α (ωList α) := ⟨fun s a => Any (fun b => a = b) s⟩ /-- Apply a function `f` to all elements of an ω-list `s`. -/ -def map (f : α → β) (s : ωList α) : ωList β := fun n => f (get s n) +def map (f : α → β) (s : ωList α) : ωList β := fun n => f (s n) /-- Zip two ω-lists using a binary operation: `ωList.get n (ωList.zip f s₁ s₂) = f (ωList.get s₁) (ωList.get s₂)`. -/ def zip (f : α → β → δ) (s₁ : ωList α) (s₂ : ωList β) : ωList δ := - fun n => f (get s₁ n) (get s₂ n) + fun n => f (s₁ n) (s₂ n) /-- Enumerate an ω-list by tagging each element with its index. -/ -def enum (s : ωList α) : ωList (ℕ × α) := fun n => (n, s.get n) +def enum (s : ωList α) : ωList (ℕ × α) := fun n => (n, s n) /-- The constant ω-list: `ωList.get n (ωList.const a) = a`. -/ def const (a : α) : ωList α := fun _ => a @@ -122,13 +120,17 @@ def appendωList : List α → ωList α → ωList α | [], s => s | List.cons a l, s => a::appendωList l s -@[inherit_doc] infixl:65 " ++ₛ " => appendωList +@[inherit_doc] infixl:65 " ++ₗ " => appendωList /-- `take n s` returns a list of the `n` first elements of ω-list `s` -/ def take : ℕ → ωList α → 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 : ωList α) (m n : ℕ) : List α := + take (n - m) (xs.drop m) + /-- An auxiliary definition for `ωList.cycle` corecursive def -/ protected def cycleF : α × List α × α × List α → α | (v, _, _, _) => v @@ -162,7 +164,7 @@ def pure (a : α) : ωList α := const a /-- Given an ω-list of functions and an ω-list of values, apply `n`-th function to `n`-th value. -/ -def apply (f : ωList (α → β)) (s : ωList α) : ωList β := fun n => (get f n) (get s n) +def apply (f : ωList (α → β)) (s : ωList α) : ωList β := fun n => (f n) (s n) @[inherit_doc] infixl:75 " ⊛ " => apply -- input as `\circledast` diff --git a/Cslib/Foundations/Data/OmegaList/Init.lean b/Cslib/Foundations/Data/OmegaList/Init.lean index 58c60791..a11c9a7d 100644 --- a/Cslib/Foundations/Data/OmegaList/Init.lean +++ b/Cslib/Foundations/Data/OmegaList/Init.lean @@ -5,13 +5,14 @@ Authors: Ching-Tsun Chou -/ import Cslib.Foundations.Data.OmegaList.Defs import Mathlib.Logic.Function.Basic +import Mathlib.Data.List.OfFn import Mathlib.Data.Nat.Basic -import Mathlib.Tactic.Common +import Mathlib.Tactic /-! # ω-lists a.k.a. infinite lists a.k.a. infinite sequences -Most code below is inherited from Mathlib.Data.Stream.Init. +Most code below is adapted from Mathlib.Data.Stream.Init. -/ open Nat Function Option @@ -32,11 +33,11 @@ instance [Inhabited α] : Inhabited (ωList α) := alias cons_head_tail := ωList.eta @[ext] -protected theorem ext {s₁ s₂ : ωList α} : (∀ n, get s₁ n = get s₂ n) → s₁ = s₂ := +protected theorem ext {s₁ s₂ : ωList α} : (∀ n, s₁ n = s₂ n) → s₁ = s₂ := fun h => funext h @[simp] -theorem get_zero_cons (a : α) (s : ωList α) : get (a::s) 0 = a := +theorem get_zero_cons (a : α) (s : ωList α) : (a::s) 0 = a := rfl @[simp] @@ -48,7 +49,7 @@ theorem tail_cons (a : α) (s : ωList α) : tail (a::s) = s := rfl @[simp] -theorem get_drop (n m : ℕ) (s : ωList α) : get (drop m s) n = get s (m + n) := by +theorem get_drop (n m : ℕ) (s : ωList α) : (drop m s) n = s (m + n) := by rw [Nat.add_comm] rfl @@ -59,7 +60,7 @@ theorem tail_eq_drop (s : ωList α) : tail s = drop 1 s := theorem drop_drop (n m : ℕ) (s : ωList α) : drop n (drop m s) = drop (m + n) s := by ext; simp [Nat.add_assoc] -@[simp] theorem get_tail {n : ℕ} {s : ωList α} : s.tail.get n = s.get (n + 1) := rfl +@[simp] theorem get_tail {n : ℕ} {s : ωList α} : s.tail n = s (n + 1) := rfl @[simp] theorem tail_drop' {i : ℕ} {s : ωList α} : tail (drop i s) = s.drop (i + 1) := by ext; simp [Nat.add_comm, Nat.add_left_comm] @@ -68,28 +69,28 @@ theorem drop_drop (n m : ℕ) (s : ωList α) : drop n (drop m s) = drop (m + n) theorem tail_drop (n : ℕ) (s : ωList α) : tail (drop n s) = drop n (tail s) := by simp -theorem get_succ (n : ℕ) (s : ωList α) : get s (succ n) = get (tail s) n := +theorem get_succ (n : ℕ) (s : ωList α) : s (succ n) = (tail s) n := rfl @[simp] -theorem get_succ_cons (n : ℕ) (s : ωList α) (x : α) : get (x :: s) n.succ = get s n := +theorem get_succ_cons (n : ℕ) (s : ωList α) (x : α) : (x :: s) n.succ = s n := rfl @[simp] lemma get_cons_append_zero {a : α} {x : List α} {s : ωList α} : - (a :: x ++ₛ s).get 0 = a := rfl + (a :: x ++ₗ s) 0 = a := rfl -@[simp] lemma append_eq_cons {a : α} {as : ωList α} : [a] ++ₛ as = a :: as := rfl +@[simp] lemma append_eq_cons {a : α} {as : ωList α} : [a] ++ₗ as = a :: as := rfl @[simp] theorem drop_zero {s : ωList α} : s.drop 0 = s := rfl theorem drop_succ (n : ℕ) (s : ωList α) : drop (succ n) s = drop n (tail s) := rfl -theorem head_drop (a : ωList α) (n : ℕ) : (a.drop n).head = a.get n := by simp +theorem head_drop (a : ωList α) (n : ℕ) : (a.drop n).head = a n := by simp theorem cons_injective2 : Function.Injective2 (cons : α → ωList α → ωList α) := fun x y s t h => ⟨by rw [← get_zero_cons x s, h, get_zero_cons], - ωList.ext fun n => by rw [← get_succ_cons n _ x, h, get_succ_cons]⟩ + ωList.ext fun n => by rw [← get_succ_cons n s x, h, get_succ_cons]⟩ theorem cons_injective_left (s : ωList α) : Function.Injective fun x => cons x s := cons_injective2.left _ @@ -97,10 +98,10 @@ theorem cons_injective_left (s : ωList α) : Function.Injective fun x => cons x theorem cons_injective_right (x : α) : Function.Injective (cons x) := cons_injective2.right _ -theorem all_def (p : α → Prop) (s : ωList α) : All p s = ∀ n, p (get s n) := +theorem all_def (p : α → Prop) (s : ωList α) : All p s = ∀ n, p (s n) := rfl -theorem any_def (p : α → Prop) (s : ωList α) : Any p s = ∃ n, p (get s n) := +theorem any_def (p : α → Prop) (s : ωList α) : Any p s = ∃ n, p (s n) := rfl @[simp] @@ -108,7 +109,7 @@ theorem mem_cons (a : α) (s : ωList α) : a ∈ a::s := Exists.intro 0 rfl theorem mem_cons_of_mem {a : α} {s : ωList α} (b : α) : a ∈ s → a ∈ b::s := fun ⟨n, h⟩ => - Exists.intro (succ n) (by rw [get_succ, tail_cons, h]) + Exists.intro (succ n) (by rw [get_succ n (b :: s), tail_cons, h]) theorem eq_or_mem_of_mem_cons {a b : α} {s : ωList α} : (a ∈ b::s) → a = b ∨ a ∈ s := fun ⟨n, h⟩ => by @@ -116,13 +117,13 @@ theorem eq_or_mem_of_mem_cons {a b : α} {s : ωList α} : (a ∈ b::s) → a = · left exact h · right - rw [get_succ, tail_cons] at h + rw [get_succ n' (b :: s), tail_cons] at h exact ⟨n', h⟩ -theorem mem_of_get_eq {n : ℕ} {s : ωList α} {a : α} : a = get s n → a ∈ s := fun h => +theorem mem_of_get_eq {n : ℕ} {s : ωList α} {a : α} : a = s n → a ∈ s := fun h => Exists.intro n h -theorem mem_iff_exists_get_eq {s : ωList α} {a : α} : a ∈ s ↔ ∃ n, a = s.get n where +theorem mem_iff_exists_get_eq {s : ωList α} {a : α} : a ∈ s ↔ ∃ n, a = s n where mp := by simp [Membership.mem, any_def] mpr h := mem_of_get_eq h.choose_spec @@ -134,7 +135,7 @@ theorem drop_map (n : ℕ) (s : ωList α) : drop n (map f s) = map f (drop n s) ωList.ext fun _ => rfl @[simp] -theorem get_map (n : ℕ) (s : ωList α) : get (map f s) n = f (get s n) := +theorem get_map (n : ℕ) (s : ωList α) : (map f s) n = f (s n) := rfl theorem tail_map (s : ωList α) : tail (map f s) = map f (tail s) := rfl @@ -165,7 +166,7 @@ theorem mem_map {a : α} {s : ωList α} : a ∈ s → f a ∈ map f s := fun Exists.intro n (by rw [get_map, h]) theorem exists_of_mem_map {f} {b : β} {s : ωList α} : b ∈ map f s → ∃ a, a ∈ s ∧ f a = b := - fun ⟨n, h⟩ => ⟨get s n, ⟨n, rfl⟩, h.symm⟩ + fun ⟨n, h⟩ => ⟨s n, ⟨n, rfl⟩, h.symm⟩ end Map @@ -179,7 +180,7 @@ theorem drop_zip (n : ℕ) (s₁ : ωList α) (s₂ : ωList β) : @[simp] theorem get_zip (n : ℕ) (s₁ : ωList α) (s₂ : ωList β) : - get (zip f s₁ s₂) n = f (get s₁ n) (get s₂ n) := + (zip f s₁ s₂) n = f (s₁ n) (s₂ n) := rfl theorem head_zip (s₁ : ωList α) (s₂ : ωList β) : head (zip f s₁ s₂) = f (head s₁) (head s₂) := @@ -194,7 +195,7 @@ theorem zip_eq (s₁ : ωList α) (s₂ : ωList β) : rw [← ωList.eta (zip f s₁ s₂)]; rfl @[simp] -theorem get_enum (s : ωList α) (n : ℕ) : get (enum s) n = (n, s.get n) := +theorem get_enum (s : ωList α) (n : ℕ) : (enum s) n = (n, s n) := rfl theorem enum_eq_zip (s : ωList α) : enum s = zip Prod.mk nats s := @@ -220,7 +221,7 @@ theorem map_const (f : α → β) (a : α) : map f (const a) = const (f a) := rfl @[simp] -theorem get_const (n : ℕ) (a : α) : get (const a) n = a := +theorem get_const (n : ℕ) (a : α) : (const a) n = a := rfl @[simp] @@ -232,7 +233,7 @@ theorem head_iterate (f : α → α) (a : α) : head (iterate f a) = a := rfl theorem get_succ_iterate' (n : ℕ) (f : α → α) (a : α) : - get (iterate f a) (succ n) = f (get (iterate f a) n) := rfl + (iterate f a) (succ n) = f ((iterate f a) n) := rfl theorem tail_iterate (f : α → α) (a : α) : tail (iterate f a) = iterate f (f a) := by ext n @@ -246,11 +247,11 @@ theorem iterate_eq (f : α → α) (a : α) : iterate f a = a::iterate f (f a) : rw [tail_iterate]; rfl @[simp] -theorem get_zero_iterate (f : α → α) (a : α) : get (iterate f a) 0 = a := +theorem get_zero_iterate (f : α → α) (a : α) : (iterate f a) 0 = a := rfl theorem get_succ_iterate (n : ℕ) (f : α → α) (a : α) : - get (iterate f a) (succ n) = get (iterate f (f a)) n := by rw [get_succ, tail_iterate] + (iterate f a) (succ n) = (iterate f (f a)) n := by rw [get_succ n (iterate f a), tail_iterate] section Bisim @@ -266,7 +267,7 @@ def IsBisimulation := head s₁ = head s₂ ∧ tail s₁ ~ tail s₂ theorem get_of_bisim (bisim : IsBisimulation R) {s₁ s₂} : - ∀ n, s₁ ~ s₂ → get s₁ n = get s₂ n ∧ drop (n + 1) s₁ ~ drop (n + 1) s₂ + ∀ n, s₁ ~ s₂ → s₁ n = s₂ n ∧ drop (n + 1) s₁ ~ drop (n + 1) s₂ | 0, h => bisim h | n + 1, h => match bisim h with @@ -281,7 +282,7 @@ end Bisim theorem bisim_simple (s₁ s₂ : ωList α) : head s₁ = head s₂ → s₁ = tail s₁ → s₂ = tail s₂ → s₁ = s₂ := fun hh ht₁ ht₂ => eq_of_bisim (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) - (fun s₁ s₂ ⟨h₁, h₂, h₃⟩ => by grind) + (fun s₁ s₂ ⟨h₁, h₂, h₃⟩ => by rw [← h₂, ← h₃] ; grind) (And.intro hh (And.intro ht₁ ht₂)) theorem coinduction {s₁ s₂ : ωList α} : @@ -312,10 +313,9 @@ theorem map_iterate (f : α → α) (a : α) : iterate f (f a) = map f (iterate induction n with | zero => rfl | succ n ih => - unfold map iterate get - rw [map, get] at ih - rw [iterate] - exact congrArg f ih + unfold map iterate + rw [map] at ih + simp [ih] section Corec @@ -343,10 +343,10 @@ end Corec' theorem unfolds_eq (g : α → β) (f : α → α) (a : α) : unfolds g f a = g a :: unfolds g f (f a) := by unfold unfolds; rw [corec_eq] -theorem get_unfolds_head_tail (n : ℕ) (s : ωList α) : get (unfolds head tail s) n = get s n := by +theorem get_unfolds_head_tail (n : ℕ) (s : ωList α) : (unfolds head tail s) n = s n := by induction n generalizing s with | zero => rfl - | succ n ih => rw [get_succ, get_succ, unfolds_eq, tail_cons, ih] + | succ n ih => rw [get_succ n (unfolds head tail s), get_succ n s, unfolds_eq, tail_cons, ih] theorem unfolds_head_eq : ∀ s : ωList α, unfolds head tail s = s := fun s => ωList.ext fun n => get_unfolds_head_tail n s @@ -363,21 +363,22 @@ theorem interleave_tail_tail (s₁ s₂ : ωList α) : tail s₁ ⋈ tail s₂ = rw [interleave_eq s₁ s₂]; rfl theorem get_interleave_left : ∀ (n : ℕ) (s₁ s₂ : ωList α), - get (s₁ ⋈ s₂) (2 * n) = get s₁ n + (s₁ ⋈ s₂) (2 * n) = s₁ n | 0, _, _ => rfl | n + 1, s₁, s₂ => by - change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n) - rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons] + change (s₁ ⋈ s₂) (succ (succ (2 * n))) = s₁ (succ n) + rw [get_succ (2 * n).succ (s₁ ⋈ s₂), get_succ (2 * n) (s₁ ⋈ s₂).tail, + interleave_eq, tail_cons, tail_cons] rw [get_interleave_left n (tail s₁) (tail s₂)] rfl theorem get_interleave_right : ∀ (n : ℕ) (s₁ s₂ : ωList α), - get (s₁ ⋈ s₂) (2 * n + 1) = get s₂ n + (s₁ ⋈ s₂) (2 * n + 1) = s₂ n | 0, _, _ => rfl | n + 1, s₁, s₂ => by - change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n) - rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons, - get_interleave_right n (tail s₁) (tail s₂)] + change (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = s₂ (succ n) + rw [get_succ (2 * n + 1).succ (s₁ ⋈ s₂), get_succ (2 * n + 1) (s₁ ⋈ s₂).tail, + interleave_eq, tail_cons, tail_cons, get_interleave_right n (tail s₁) (tail s₂)] rfl theorem mem_interleave_left {a : α} {s₁ : ωList α} (s₂ : ωList α) : a ∈ s₁ → a ∈ s₁ ⋈ s₂ := @@ -422,13 +423,13 @@ theorem interleave_even_odd (s₁ : ωList α) : even s₁ ⋈ odd s₁ = s₁ : · simp [odd_eq, odd_eq, tail_interleave, tail_even]) rfl -theorem get_even : ∀ (n : ℕ) (s : ωList α), get (even s) n = get s (2 * n) +theorem get_even : ∀ (n : ℕ) (s : ωList α), (even s) n = s (2 * n) | 0, _ => rfl | succ n, s => by - change get (even s) (succ n) = get s (succ (succ (2 * n))) - rw [get_succ, get_succ, tail_even, get_even n]; rfl + change (even s) (succ n) = s (succ (succ (2 * n))) + rw [get_succ n s.even, get_succ (2 * n).succ s, tail_even, get_even n]; rfl -theorem get_odd : ∀ (n : ℕ) (s : ωList α), get (odd s) n = get s (2 * n + 1) := fun n s => by +theorem get_odd : ∀ (n : ℕ) (s : ωList α), (odd s) n = s (2 * n + 1) := fun n s => by rw [odd_eq, get_even]; rfl theorem mem_of_mem_even (a : α) (s : ωList α) : a ∈ even s → a ∈ s := fun ⟨n, h⟩ => @@ -445,12 +446,12 @@ theorem cons_append_ωList (a : α) (l : List α) (s : ωList α) : rfl @[simp] theorem append_append_ωList : ∀ (l₁ l₂ : List α) (s : ωList α), - l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s) + l₁ ++ l₂ ++ₗ s = l₁ ++ₗ (l₂ ++ₗ s) | [], _, _ => rfl | List.cons a l₁, l₂, s => by rw [List.cons_append, cons_append_ωList, cons_append_ωList, append_append_ωList l₁] -lemma get_append_left (h : n < x.length) : (x ++ₛ a).get n = x[n] := by +lemma get_append_left (h : n < x.length) : (x ++ₗ a) n = x[n] := by induction x generalizing n with | nil => simp at h | cons b x ih => @@ -458,43 +459,48 @@ lemma get_append_left (h : n < x.length) : (x ++ₛ a).get n = x[n] := by · simp · simp [ih n (by simpa using h), cons_append_ωList] -@[simp] lemma get_append_right : (x ++ₛ a).get (x.length + n) = a.get n := by +@[simp] lemma get_append_right : (x ++ₗ a) (x.length + n) = a n := by induction x <;> simp [Nat.succ_add, *, cons_append_ωList] -@[simp] lemma get_append_length : (x ++ₛ a).get x.length = a.get 0 := get_append_right 0 x a +theorem get_append_right' {xl : List α} {xs : ωList α} {k : ℕ} (h : xl.length ≤ k) : + (xl ++ₗ xs) k = xs (k - xl.length) := by + obtain ⟨n, rfl⟩ := show ∃ n, k = xl.length + n by use (k - xl.length) ; omega + simp only [Nat.add_sub_cancel_left] ; apply get_append_right -lemma append_right_injective (h : x ++ₛ a = x ++ₛ b) : a = b := by - ext n; replace h := congr_arg (fun a ↦ a.get (x.length + n)) h; simpa using h +@[simp] lemma get_append_length : (x ++ₗ a) x.length = a 0 := get_append_right 0 x a -@[simp] lemma append_right_inj : x ++ₛ a = x ++ₛ b ↔ a = b := +lemma append_right_injective (h : x ++ₗ a = x ++ₗ b) : a = b := by + ext n; replace h := congr_arg (fun a ↦ a (x.length + n)) h; simpa using h + +@[simp] lemma append_right_inj : x ++ₗ a = x ++ₗ b ↔ a = b := ⟨append_right_injective x a b, by simp +contextual⟩ -lemma append_left_injective (h : x ++ₛ a = y ++ₛ b) (hl : x.length = y.length) : x = y := by +lemma append_left_injective (h : x ++ₗ a = y ++ₗ b) (hl : x.length = y.length) : x = y := by apply List.ext_getElem hl intros rw [← get_append_left, ← get_append_left, h] theorem map_append_ωList (f : α → β) : - ∀ (l : List α) (s : ωList α), map f (l ++ₛ s) = List.map f l ++ₛ map f s + ∀ (l : List α) (s : ωList α), map f (l ++ₗ s) = List.map f l ++ₗ map f s | [], _ => rfl | List.cons a l, s => by rw [cons_append_ωList, List.map_cons, map_cons, cons_append_ωList, map_append_ωList f l] -theorem drop_append_ωList : ∀ (l : List α) (s : ωList α), drop l.length (l ++ₛ s) = s +theorem drop_append_ωList : ∀ (l : List α) (s : ωList α), drop l.length (l ++ₗ s) = s | [], s => rfl | List.cons a l, s => by rw [List.length_cons, drop_succ, cons_append_ωList, tail_cons, drop_append_ωList l s] -theorem append_ωList_head_tail (s : ωList α) : [head s] ++ₛ tail s = s := by +theorem append_ωList_head_tail (s : ωList α) : [head s] ++ₗ tail s = s := by simp -theorem mem_append_ωList_right : ∀ {a : α} (l : List α) {s : ωList α}, a ∈ s → a ∈ l ++ₛ s +theorem mem_append_ωList_right : ∀ {a : α} (l : List α) {s : ωList α}, a ∈ s → a ∈ l ++ₗ s | _, [], _, h => h | a, List.cons _ l, s, h => - have ih : a ∈ l ++ₛ s := mem_append_ωList_right l h + have ih : a ∈ l ++ₗ s := mem_append_ωList_right l h mem_cons_of_mem _ ih -theorem mem_append_ωList_left : ∀ {a : α} {l : List α} (s : ωList α), a ∈ l → a ∈ l ++ₛ s +theorem mem_append_ωList_left : ∀ {a : α} {l : List α} (s : ωList α), a ∈ l → a ∈ l ++ₗ s | _, [], _, h => absurd h List.not_mem_nil | a, List.cons b l, s, h => Or.elim (List.eq_or_mem_of_mem_cons h) (fun aeqb : a = b => Exists.intro 0 aeqb) @@ -513,10 +519,20 @@ theorem take_succ (n : ℕ) (s : ωList α) : take (succ n) s = head s::take n ( @[simp] theorem take_succ_cons {a : α} (n : ℕ) (s : ωList α) : take (n+1) (a::s) = a :: take n s := rfl -theorem take_succ' {s : ωList α} : ∀ n, s.take (n+1) = s.take n ++ [s.get n] +theorem take_succ' {s : ωList α} : ∀ n, s.take (n+1) = s.take n ++ [s n] | 0 => rfl | n+1 => by rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail] +@[simp] +theorem take_one {xs : ωList α} : + xs.take 1 = [xs 0] := by + simp only [take_succ, take_zero] + +@[simp] +theorem take_one' {xs : ωList α} : + xs.take 1 = [xs 0] := by + apply take_one + @[simp] theorem length_take (n : ℕ) (s : ωList α) : (take n s).length = n := by induction n generalizing s <;> simp [*, take_succ] @@ -527,16 +543,16 @@ theorem take_take {s : ωList α} : ∀ {m n}, (s.take n).take m = s.take (min n | m, 0 => by rw [Nat.zero_min, take_zero, List.take_nil] | m+1, n+1 => by rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take] -@[simp] theorem concat_take_get {n : ℕ} {s : ωList α} : s.take n ++ [s.get n] = s.take (n + 1) := +@[simp] theorem concat_take_get {n : ℕ} {s : ωList α} : s.take n ++ [s n] = s.take (n + 1) := (take_succ' n).symm -theorem getElem?_take {s : ωList α} : ∀ {k n}, k < n → (s.take n)[k]? = s.get k +theorem getElem?_take {s : ωList α} : ∀ {k n}, k < n → (s.take n)[k]? = s k | 0, _+1, _ => by simp only [length_take, zero_lt_succ, List.getElem?_eq_getElem]; rfl | k+1, n+1, h => by - rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ] + rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ k s] theorem getElem?_take_succ (n : ℕ) (s : ωList α) : - (take (succ n) s)[n]? = some (get s n) := + (take (succ n) s)[n]? = some (s n) := getElem?_take (Nat.lt_succ_self n) @[simp] theorem dropLast_take {n : ℕ} {xs : ωList α} : @@ -551,14 +567,14 @@ theorem append_take_drop (n : ℕ) (s : ωList α) : appendωList (take n s) (dr | zero => rfl | succ n ih =>rw [take_succ, drop_succ, cons_append_ωList, ih (tail s), ωList.eta] -lemma append_take : x ++ (a.take n) = (x ++ₛ a).take (x.length + n) := by +lemma append_take : x ++ (a.take n) = (x ++ₗ a).take (x.length + n) := by induction x <;> simp [take, Nat.add_comm, cons_append_ωList, *] -@[simp] lemma take_get (h : m < (a.take n).length) : (a.take n)[m] = a.get m := by +@[simp] lemma take_get (h : m < (a.take n).length) : (a.take n)[m] = a m := by nth_rw 2 [← append_take_drop n a]; rw [get_append_left] theorem take_append_of_le_length (h : n ≤ x.length) : - (x ++ₛ a).take n = x.take n := by + (x ++ₗ a).take n = x.take n := by apply List.ext_getElem (by simp [h]) intro _ _ _; rw [List.getElem_take, take_get, get_append_left] @@ -580,7 +596,7 @@ lemma take_drop : (a.drop m).take n = (a.take (m + n)).drop m := by apply List.ext_getElem <;> simp lemma drop_append_of_le_length (h : n ≤ x.length) : - (x ++ₛ a).drop n = x.drop n ++ₛ a := by + (x ++ₗ a).drop n = x.drop n ++ₗ a := by obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h ext k; rcases lt_or_ge k m with _ | hk · rw [get_drop, get_append_left, get_append_left, List.getElem_drop]; simpa [hm] @@ -588,6 +604,11 @@ lemma drop_append_of_le_length (h : n ≤ x.length) : have hm' : m = (x.drop n).length := by simp [hm] simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right] +theorem drop_append_of_ge_length {xl : List α} {xs : ωList α} {n : ℕ} (h : xl.length ≤ n) : + (xl ++ₗ xs).drop n = xs.drop (n - xl.length) := by + ext k ; simp (disch := omega) only [get_drop, get_append_right'] + congr ; omega + -- Take theorem reduces a proof of equality of infinite ω-lists to an -- induction over all their finite approximations. theorem take_theorem (s₁ s₂ : ωList α) (h : ∀ n : ℕ, take n s₁ = take n s₂) : s₁ = s₂ := by @@ -595,7 +616,7 @@ theorem take_theorem (s₁ s₂ : ωList α) (h : ∀ n : ℕ, take n s₁ = tak induction n with | zero => simpa [take] using h 1 | succ n => - have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by + have h₁ : some (s₁ (succ n)) = some (s₂ (succ n)) := by rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))] injection h₁ @@ -603,11 +624,11 @@ protected theorem cycle_g_cons (a : α) (a₁ : α) (l₁ : List α) (a₀ : α) ωList.cycleG (a, a₁::l₁, a₀, l₀) = (a₁, l₁, a₀, l₀) := rfl -theorem cycle_eq : ∀ (l : List α) (h : l ≠ []), cycle l h = l ++ₛ cycle l h +theorem cycle_eq : ∀ (l : List α) (h : l ≠ []), cycle l h = l ++ₗ cycle l h | [], h => absurd rfl h | List.cons a l, _ => have gen (l' a') : corec ωList.cycleF ωList.cycleG (a', l', a, l) = - (a'::l') ++ₛ corec ωList.cycleF ωList.cycleG (a, l, a, l) := by + (a'::l') ++ₗ corec ωList.cycleF ωList.cycleG (a, l, a, l) := by induction l' generalizing a' with | nil => rw [corec_eq]; rfl | cons a₁ l₁ ih => rw [corec_eq, ωList.cycle_g_cons, ih a₁]; rfl @@ -624,10 +645,10 @@ theorem tails_eq (s : ωList α) : tails s = tail s::tails (tail s) := by unfold tails; rw [corec_eq]; rfl @[simp] -theorem get_tails (n : ℕ) (s : ωList α) : get (tails s) n = drop n (tail s) := by +theorem get_tails (n : ℕ) (s : ωList α) : (tails s) n = drop n (tail s) := by induction n generalizing s with | zero => rfl - | succ n ih => rw [get_succ, drop_succ, tails_eq, tail_cons, ih] + | succ n ih => rw [get_succ n s.tails, drop_succ, tails_eq, tail_cons, ih] theorem tails_eq_iterate (s : ωList α) : tails s = iterate tail (tail s) := rfl @@ -646,25 +667,27 @@ theorem inits_tail (s : ωList α) : inits (tail s) = initsCore [head (tail s)] rfl theorem cons_get_inits_core (a : α) (n : ℕ) (l : List α) (s : ωList α) : - (a :: get (initsCore l s) n) = get (initsCore (a :: l) s) n := by + (a :: (initsCore l s) n) = (initsCore (a :: l) s) n := by induction n generalizing l s with | zero => rfl | succ n ih => - rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s] + rw [get_succ n (initsCore l s), inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s] rfl @[simp] -theorem get_inits (n : ℕ) (s : ωList α) : get (inits s) n = take (succ n) s := by +theorem get_inits (n : ℕ) (s : ωList α) : (inits s) n = take (succ n) s := by induction n generalizing s with | zero => rfl - | succ n ih => rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core] + | succ n ih => + rw [get_succ n s.inits, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core] theorem inits_eq (s : ωList α) : inits s = [head s]::map (List.cons (head s)) (inits (tail s)) := by apply ωList.ext; intro n - cases n + induction' n with n _ · rfl - · rw [get_inits, get_succ, tail_cons, get_map, get_inits] + · rw [get_inits, get_succ n ([s.head] :: map (List.cons s.head) s.tail.inits), + tail_cons, get_map, get_inits] rfl theorem zip_inits_tails (s : ωList α) : zip appendωList (inits s) (tails s) = const s := by @@ -689,13 +712,97 @@ theorem interchange (fs : ωList (α → β)) (a : α) : theorem map_eq_apply (f : α → β) (s : ωList α) : map f s = pure f ⊛ s := rfl -theorem get_nats (n : ℕ) : get nats n = n := +theorem get_nats (n : ℕ) : nats n = n := rfl theorem nats_eq : nats = cons 0 (map succ nats) := by apply ωList.ext; intro n - cases n + induction' n with n _ · rfl - rw [get_succ]; rfl + rw [get_succ n nats] ; rfl + +theorem extract_eq_drop_take {xs : ωList α} {m n : ℕ} : + xs.extract m n = take (n - m) (xs.drop m) := by + rfl + +theorem extract_eq_ofFn {xs : ωList α} {m n : ℕ} : + xs.extract m n = List.ofFn (fun k : Fin (n - m) ↦ xs (m + k)) := by + ext k x ; rcases (show k < n - m ∨ ¬ k < n - m by omega) with h_k | h_k + <;> simp (disch := omega) [extract_eq_drop_take, getElem?_take, get_drop] + <;> aesop + +theorem extract_eq_extract {xs xs' : ωList α} {m n m' n' : ℕ} + (h : xs.extract m n = xs'.extract m' n') : + n - m = n' - m' ∧ ∀ k < n - m, xs (m + k) = xs' (m' + k) := by + simp only [extract_eq_ofFn, List.ofFn_inj', Sigma.mk.injEq] at h + obtain ⟨h_eq, h_fun⟩ := h + rw [← h_eq] at h_fun ; simp only [heq_eq_eq, funext_iff, Fin.forall_iff] at h_fun + simp only [← h_eq, true_and] ; intro k h_k ; simp only [h_fun k h_k] + +theorem extract_eq_take {xs : ωList α} {n : ℕ} : + xs.extract 0 n = xs.take n := by + simp only [extract_eq_drop_take, Nat.sub_zero, drop_zero] + +theorem append_extract_drop {xs : ωList α} {n : ℕ} : + (xs.extract 0 n) ++ₗ (xs.drop n) = xs := by + simp only [extract_eq_take, append_take_drop] + +theorem extract_apppend_right_right {xl : List α} {xs : ωList α} {m n : ℕ} (h : xl.length ≤ m) : + (xl ++ₗ xs).extract m n = xs.extract (m - xl.length) (n - xl.length) := by + have h1 : n - xl.length - (m - xl.length) = n - m := by omega + simp (disch := omega) only [extract_eq_drop_take, drop_append_of_ge_length, h1] + +theorem extract_append_zero_right {xl : List α} {xs : ωList α} {n : ℕ} (h : xl.length ≤ n) : + (xl ++ₗ xs).extract 0 n = xl ++ (xs.extract 0 (n - xl.length)) := by + obtain ⟨k, rfl⟩ := show ∃ k, n = xl.length + k by use (n - xl.length) ; omega + simp only [extract_eq_take, ← append_take, Nat.add_sub_cancel_left] + +theorem extract_drop {xs : ωList α} {k m n : ℕ} : + (xs.drop k).extract m n = xs.extract (k + m) (k + n) := by + have h1 : k + n - (k + m) = n - m := by omega + simp only [extract_eq_drop_take, drop_drop, h1] + +theorem length_extract {xs : ωList α} {m n : ℕ} : + (xs.extract m n).length = n - m := by + simp only [extract_eq_drop_take, length_take] + +theorem extract_eq_nil {xs : ωList α} {n : ℕ} : + xs.extract n n = [] := by + simp only [extract_eq_drop_take, Nat.sub_self, take_zero] + +theorem extract_eq_nil_iff {xs : ωList α} {m n : ℕ} : + xs.extract m n = [] ↔ m ≥ n := by + simp only [extract_eq_drop_take, ← List.length_eq_zero_iff, length_take, ge_iff_le] + omega + +theorem get_extract {xs : ωList α} {m n k : ℕ} (h : k < n - m) : + (xs.extract m n)[k]'(by simp only [length_extract, h]) = xs (m + k) := by + simp only [extract_eq_drop_take, take_get, get_drop] + +theorem append_extract_extract {xs : ωList α} {k m n : ℕ} (h_km : k ≤ m) (h_mn : m ≤ n) : + (xs.extract k m) ++ (xs.extract m n) = xs.extract k n := by + have h1 : n - k = (m - k) + (n - m) := by omega + have h2 : k + (m - k) = m := by omega + simp only [extract_eq_drop_take, h1, take_add, drop_drop, h2] + +theorem extract_succ_right {xs : ωList α} {m n : ℕ} (h_mn : m ≤ n) : + xs.extract m (n + 1) = xs.extract m n ++ [xs n] := by + rw [← append_extract_extract h_mn (show n ≤ n + 1 by omega)] ; congr + simp only [extract_eq_drop_take, Nat.add_sub_cancel_left, take_one, get_drop, Nat.add_zero] + +theorem extract_extract2' {xs : ωList α} {m n i j : ℕ} (h : j ≤ n - m) : + (xs.extract m n).extract i j = xs.extract (m + i) (m + j) := by + ext k x ; rcases (show k < j - i ∨ ¬ k < j - i by omega) with h_k | h_k + <;> simp [extract_eq_ofFn, h_k] + · simp [(show i + k < n - m by omega), (show k < m + j - (m + i) by omega), Nat.add_assoc] + · simp only [(show ¬k < m + j - (m + i) by omega), IsEmpty.forall_iff] + +theorem extract_extract2 {xs : ωList α} {n i j : ℕ} (h : j ≤ n) : + (xs.extract 0 n).extract i j = xs.extract i j := by + simp only [extract_extract2' (show j ≤ n - 0 by omega), Nat.zero_add] + +theorem extract_extract1 {xs : ωList α} {n i : ℕ} : + (xs.extract 0 n).extract i = xs.extract i n := by + simp only [length_extract, extract_extract2 (show n ≤ n by omega), Nat.sub_zero] end ωList From 6cafde410a493458b22788611957b1acdf980c11 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Mon, 6 Oct 2025 14:15:10 -0700 Subject: [PATCH 3/3] feat: An initial version of Buchi and Muller automata --- Cslib.lean | 2 + Cslib/Computability/Automata/BuchiNA.lean | 43 ++++++++++++++++++ Cslib/Computability/Automata/DA.lean | 9 ++++ Cslib/Computability/Automata/MullerDA.lean | 53 ++++++++++++++++++++++ Cslib/Computability/Automata/NA.lean | 6 +++ 5 files changed, 113 insertions(+) create mode 100644 Cslib/Computability/Automata/BuchiNA.lean create mode 100644 Cslib/Computability/Automata/MullerDA.lean diff --git a/Cslib.lean b/Cslib.lean index 8453b60e..ac1fde9b 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,8 +1,10 @@ +import Cslib.Computability.Automata.BuchiNA 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.MullerDA import Cslib.Computability.Automata.NA import Cslib.Computability.Automata.NFA import Cslib.Computability.Automata.NFAToDFA diff --git a/Cslib/Computability/Automata/BuchiNA.lean b/Cslib/Computability/Automata/BuchiNA.lean new file mode 100644 index 00000000..2f4d33c8 --- /dev/null +++ b/Cslib/Computability/Automata/BuchiNA.lean @@ -0,0 +1,43 @@ +/- +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.Computability.Automata.NA +import Mathlib.Order.Filter.AtTopBot.Defs + +open Filter + +/-- Nondeterministic Büchi automaton is a nondeterministic automaton over +finite sets of states and symbols together with a finite set of accepting states. -/ +structure BuchiNA (State : Type _) (Symbol : Type _) extends NA State Symbol where + /-- The set of accepting states of the automaton. -/ + accept : Set State + /-- The automaton is finite-state. -/ + finite_state : Finite State + /-- The type of symbols (also called 'alphabet') is finite. -/ + finite_symbol : Finite Symbol + +namespace BuchiNA + +variable {State : Type _} {Symbol : Type _} + +/-- A nondeterministic Büchi automaton accepts an ω-word `xs` iff it has an infinite run +on `xs` which passes through accepting states infinitely often. +-/ +@[scoped grind] +def Accepts (nba : BuchiNA State Symbol) (xs : ωList Symbol) := + ∃ ss, nba.InfRun xs ss ∧ ∃ᶠ k in atTop, ss k ∈ nba.accept + +/-- The language of a nondeterministic Büchi automaton is the set of ω-words that it accepts. -/ +@[scoped grind] +def language (nba : BuchiNA State Symbol) : Set (ωList Symbol) := + { xs | nba.Accepts xs } + +/-- A string is accepted by a a nondeterministic Büchi automaton iff it is in its language. -/ +@[scoped grind] +theorem accepts_mem_language (nba : BuchiNA State Symbol) (xs : ωList Symbol) : + nba.Accepts xs ↔ xs ∈ nba.language := by rfl + +end BuchiNA diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean index a9f5a85f..b22f31f3 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA.lean @@ -5,6 +5,7 @@ Authors: Fabrizio Montesi -/ import Cslib.Computability.Automata.NA +import Cslib.Foundations.Data.OmegaList.Init /-! # Deterministic Automaton @@ -15,3 +16,11 @@ structure DA (State : Type _) (Symbol : Type _) where start : State /-- The transition function of the automaton. -/ tr : State → Symbol → State + +variable {State : Type _} {Symbol : Type _} + +/-- The (unique) infinite run of a DA on an infinite input `xs`. +-/ +def DA.infRun (da : DA State Symbol) (xs : ωList Symbol) : ωList State + | 0 => da.start + | k + 1 => da.tr (da.infRun xs k) (xs k) diff --git a/Cslib/Computability/Automata/MullerDA.lean b/Cslib/Computability/Automata/MullerDA.lean new file mode 100644 index 00000000..7af9b2fa --- /dev/null +++ b/Cslib/Computability/Automata/MullerDA.lean @@ -0,0 +1,53 @@ +/- +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.Computability.Automata.DA +import Mathlib.Order.Filter.AtTopBot.Defs + +open Filter + +/-! # Deterministic Muller Automata +-/ + +/-- `xs.infOcc` is the set of elements that occurs infinitely many times in `xs`. +TODO: This definition should be be moved to a different file. +-/ +def ωList.infOcc {X : Type*} (xs : ωList X) : Set X := + { x | ∃ᶠ k in atTop, xs k = x } + +/-- A deterministic Muller automaton consists of a labelled transition function +`tr` over finite sets of states and labels (called symbols), a starting state `start`, +and a finite set of finite accepting sets `accept`. -/ +structure MullerDA (State : Type _) (Symbol : Type _) extends DA State Symbol where + /-- The set of accepting sets of the automaton. -/ + accept : Set (Set State) + /-- The automaton is finite-state. -/ + finite_state : Finite State + /-- The type of symbols (also called 'alphabet') is finite. -/ + finite_symbol : Finite Symbol + +namespace MullerDA + +variable {State : Type _} {Symbol : Type _} + +/-- A deterministic Muller automaton `mda` accepts an ω-word `xs` iff the set of states that +occurs infinite often when running `mda` on `xs` is one of the accepting sets. +-/ +@[scoped grind →] +def Accepts (mda : MullerDA State Symbol) (xs : ωList Symbol) := + (mda.infRun xs).infOcc ∈ mda.accept + +/-- The ω-language of a deterministic Muller automaton is the set of ω-words that it accepts. -/ +@[scoped grind =] +def language (mda : MullerDA State Symbol) : Set (ωList Symbol) := + { xs | mda.Accepts xs } + +/-- An ω-word is accepted by a deterministic Muller automaton iff it is in its ω-language. -/ +@[scoped grind _=_] +theorem accepts_mem_language (mda : MullerDA State Symbol) (xs : ωList Symbol) : + mda.Accepts xs ↔ xs ∈ mda.language := by rfl + +end MullerDA diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index 71d5592d..88eb265b 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ +import Cslib.Foundations.Data.OmegaList.Init import Cslib.Foundations.Semantics.LTS.Basic /-! # Nondeterministic Automaton @@ -17,3 +18,8 @@ type `State → Symbol → Set State`; it gets automatically expanded to the for structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where /-- The set of initial states of the automaton. -/ start : Set State + +variable {State : Type _} {Symbol : Type _} + +def NA.InfRun (na : NA State Symbol) (xs : ωList Symbol) (ss : ωList State) := + ss 0 ∈ na.start ∧ ∀ k, na.Tr (ss k) (xs k) (ss (k + 1))