|
| 1 | +/- |
| 2 | +Copyright (c) 2025-present Ching-Tsun Chou All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Ching-Tsun Chou |
| 5 | +-/ |
| 6 | +import Mathlib.Data.Nat.Notation |
| 7 | + |
| 8 | +/-! |
| 9 | +# Definition of `ωList` and functions on infinite lists |
| 10 | +
|
| 11 | +An `ωList α` is an infinite sequence of elements of `α`. It is |
| 12 | +basically a wrapper around the type `ℕ → α` which supports the |
| 13 | +dot-notation and the analogues of many familiar API functions of |
| 14 | +`List α`. In this file we define `ωList` and some functions that |
| 15 | +take and/or return ω-lists. |
| 16 | +
|
| 17 | +Most code below is inherited from Mathlib.Data.Stream.Defs. |
| 18 | +-/ |
| 19 | + |
| 20 | +universe u v w |
| 21 | +variable {α : Type u} {β : Type v} {δ : Type w} |
| 22 | + |
| 23 | +/-- An `ωList α` is an infinite sequence of elements of `α`. -/ |
| 24 | +def ωList (α : Type u) := ℕ → α |
| 25 | + |
| 26 | +namespace ωList |
| 27 | + |
| 28 | +/-- Prepend an element to an ω-list. -/ |
| 29 | +def cons (a : α) (s : ωList α) : ωList α |
| 30 | + | 0 => a |
| 31 | + | n + 1 => s n |
| 32 | + |
| 33 | +@[inherit_doc] scoped infixr:67 " :: " => cons |
| 34 | + |
| 35 | +/-- Get the `n`-th element of an ω-list. -/ |
| 36 | +def get (s : ωList α) (n : ℕ) : α := s n |
| 37 | + |
| 38 | +/-- Head of an ω-list: `ωList.head s = ωList.get s 0`. -/ |
| 39 | +abbrev head (s : ωList α) : α := s.get 0 |
| 40 | + |
| 41 | +/-- Tail of an ω-list: `ωList.tail (h :: t) = t`. -/ |
| 42 | +def tail (s : ωList α) : ωList α := fun i => s.get (i + 1) |
| 43 | + |
| 44 | +/-- Drop first `n` elements of an ω-list. -/ |
| 45 | +def drop (n : ℕ) (s : ωList α) : ωList α := fun i => s.get (i + n) |
| 46 | + |
| 47 | +/-- Proposition saying that all elements of an ω-list satisfy a predicate. -/ |
| 48 | +def All (p : α → Prop) (s : ωList α) := ∀ n, p (get s n) |
| 49 | + |
| 50 | +/-- Proposition saying that at least one element of an ω-list satisfies a predicate. -/ |
| 51 | +def Any (p : α → Prop) (s : ωList α) := ∃ n, p (get s n) |
| 52 | + |
| 53 | +/-- `a ∈ s` means that `a = ωList.get n s` for some `n`. -/ |
| 54 | +instance : Membership α (ωList α) := |
| 55 | + ⟨fun s a => Any (fun b => a = b) s⟩ |
| 56 | + |
| 57 | +/-- Apply a function `f` to all elements of an ω-list `s`. -/ |
| 58 | +def map (f : α → β) (s : ωList α) : ωList β := fun n => f (get s n) |
| 59 | + |
| 60 | +/-- Zip two ω-lists using a binary operation: |
| 61 | +`ωList.get n (ωList.zip f s₁ s₂) = f (ωList.get s₁) (ωList.get s₂)`. -/ |
| 62 | +def zip (f : α → β → δ) (s₁ : ωList α) (s₂ : ωList β) : ωList δ := |
| 63 | + fun n => f (get s₁ n) (get s₂ n) |
| 64 | + |
| 65 | +/-- Enumerate an ω-list by tagging each element with its index. -/ |
| 66 | +def enum (s : ωList α) : ωList (ℕ × α) := fun n => (n, s.get n) |
| 67 | + |
| 68 | +/-- The constant ω-list: `ωList.get n (ωList.const a) = a`. -/ |
| 69 | +def const (a : α) : ωList α := fun _ => a |
| 70 | + |
| 71 | +/-- Iterates of a function as an ω-list. -/ |
| 72 | +def iterate (f : α → α) (a : α) : ωList α |
| 73 | + | 0 => a |
| 74 | + | n + 1 => f (iterate f a n) |
| 75 | + |
| 76 | +/-- Given functions `f : α → β` and `g : α → α`, `corec f g` creates an ω-list by: |
| 77 | +1. Starting with an initial value `a : α` |
| 78 | +2. Applying `g` repeatedly to get an ω-list of α values |
| 79 | +3. Applying `f` to each value to convert them to β |
| 80 | +-/ |
| 81 | +def corec (f : α → β) (g : α → α) : α → ωList β := fun a => map f (iterate g a) |
| 82 | + |
| 83 | +/-- Given an initial value `a : α` and functions `f : α → β` and `g : α → α`, |
| 84 | +`corecOn a f g` creates an ω-list by repeatedly: |
| 85 | +1. Applying `f` to the current value to get the next ω-list element |
| 86 | +2. Applying `g` to get the next value to process |
| 87 | +This is equivalent to `corec f g a`. -/ |
| 88 | +def corecOn (a : α) (f : α → β) (g : α → α) : ωList β := |
| 89 | + corec f g a |
| 90 | + |
| 91 | +/-- Given a function `f : α → β × α`, `corec' f` creates an ω-list by repeatedly: |
| 92 | +1. Starting with an initial value `a : α` |
| 93 | +2. Applying `f` to get both the next ω-list element (β) and next state value (α) |
| 94 | +This is a more convenient form when the next element and state are computed together. -/ |
| 95 | +def corec' (f : α → β × α) : α → ωList β := |
| 96 | + corec (Prod.fst ∘ f) (Prod.snd ∘ f) |
| 97 | + |
| 98 | +/-- Use a state monad to generate an ω-list through corecursion -/ |
| 99 | +def corecState {σ α} (cmd : StateM σ α) (s : σ) : ωList α := |
| 100 | + corec Prod.fst (cmd.run ∘ Prod.snd) (cmd.run s) |
| 101 | + |
| 102 | +-- corec is also known as unfolds |
| 103 | +abbrev unfolds (g : α → β) (f : α → α) (a : α) : ωList β := |
| 104 | + corec g f a |
| 105 | + |
| 106 | +/-- Interleave two ω-lists. -/ |
| 107 | +def interleave (s₁ s₂ : ωList α) : ωList α := |
| 108 | + corecOn (s₁, s₂) (fun ⟨s₁, _⟩ => head s₁) fun ⟨s₁, s₂⟩ => (s₂, tail s₁) |
| 109 | + |
| 110 | +@[inherit_doc] infixl:65 " ⋈ " => interleave |
| 111 | + |
| 112 | +/-- Elements of an ω-list with even indices. -/ |
| 113 | +def even (s : ωList α) : ωList α := |
| 114 | + corec head (fun s => tail (tail s)) s |
| 115 | + |
| 116 | +/-- Elements of an ω-list with odd indices. -/ |
| 117 | +def odd (s : ωList α) : ωList α := |
| 118 | + even (tail s) |
| 119 | + |
| 120 | +/-- Append an ω-list to a list. -/ |
| 121 | +def appendωList : List α → ωList α → ωList α |
| 122 | + | [], s => s |
| 123 | + | List.cons a l, s => a::appendωList l s |
| 124 | + |
| 125 | +@[inherit_doc] infixl:65 " ++ₛ " => appendωList |
| 126 | + |
| 127 | +/-- `take n s` returns a list of the `n` first elements of ω-list `s` -/ |
| 128 | +def take : ℕ → ωList α → List α |
| 129 | + | 0, _ => [] |
| 130 | + | n + 1, s => List.cons (head s) (take n (tail s)) |
| 131 | + |
| 132 | +/-- An auxiliary definition for `ωList.cycle` corecursive def -/ |
| 133 | +protected def cycleF : α × List α × α × List α → α |
| 134 | + | (v, _, _, _) => v |
| 135 | + |
| 136 | +/-- An auxiliary definition for `ωList.cycle` corecursive def -/ |
| 137 | +protected def cycleG : α × List α × α × List α → α × List α × α × List α |
| 138 | + | (_, [], v₀, l₀) => (v₀, l₀, v₀, l₀) |
| 139 | + | (_, List.cons v₂ l₂, v₀, l₀) => (v₂, l₂, v₀, l₀) |
| 140 | + |
| 141 | +/-- Interpret a nonempty list as a cyclic ω-list. -/ |
| 142 | +def cycle : ∀ l : List α, l ≠ [] → ωList α |
| 143 | + | [], h => absurd rfl h |
| 144 | + | List.cons a l, _ => corec ωList.cycleF ωList.cycleG (a, l, a, l) |
| 145 | + |
| 146 | +/-- Tails of an ω-list, starting with `ωList.tail s`. -/ |
| 147 | +def tails (s : ωList α) : ωList (ωList α) := |
| 148 | + corec id tail (tail s) |
| 149 | + |
| 150 | +/-- An auxiliary definition for `ωList.inits`. -/ |
| 151 | +def initsCore (l : List α) (s : ωList α) : ωList (List α) := |
| 152 | + corecOn (l, s) (fun ⟨a, _⟩ => a) fun p => |
| 153 | + match p with |
| 154 | + | (l', s') => (l' ++ [head s'], tail s') |
| 155 | + |
| 156 | +/-- Nonempty initial segments of an ω-list. -/ |
| 157 | +def inits (s : ωList α) : ωList (List α) := |
| 158 | + initsCore [head s] (tail s) |
| 159 | + |
| 160 | +/-- A constant ω-list, same as `ωList.const`. -/ |
| 161 | +def pure (a : α) : ωList α := |
| 162 | + const a |
| 163 | + |
| 164 | +/-- Given an ω-list of functions and an ω-list of values, apply `n`-th function to `n`-th value. -/ |
| 165 | +def apply (f : ωList (α → β)) (s : ωList α) : ωList β := fun n => (get f n) (get s n) |
| 166 | + |
| 167 | +@[inherit_doc] infixl:75 " ⊛ " => apply -- input as `\circledast` |
| 168 | + |
| 169 | +/-- The ω-list of natural numbers: `ωList.get n ωList.nats = n`. -/ |
| 170 | +def nats : ωList ℕ := fun n => n |
| 171 | + |
| 172 | +end ωList |
0 commit comments