Stream'.Seq as a trace monoid

Traces are possibly-infinite: a diverging algorithm that keeps sending emits forever, and a finite trace type cannot hold what it emits. Stream'.Seq is the coinductive possibly-finite sequence, and concatenation makes it a monoid unconditionally — including append_nil, which holds because appending to an infinite sequence absorbs the right operand rather than failing.

That absorption is the reason this is a monoid at all, and it is worth stating plainly since it is the one law a reader expects to break: for infinite s, s * t = s for every t, so s * 1 = s is a special case of absorption rather than a genuine right identity. Nothing downstream depends on cancellativity, so the collapse is harmless — see VerifiedCompiler/Trace.lean, whose SCPrefix lemmas are all introduction and elimination on ∃ δ.

Mathlib proves the three laws but registers no algebraic instance, so they are bundled here.

@[implicit_reducible]

instance Stream'.Seq.instOne_extra {α : Type u_1} : One (Seq α)

The empty trace.

Equations

• Stream'.Seq.instOne_extra = { one := Stream'.Seq.nil }

@[implicit_reducible]

instance Stream'.Seq.instMul_extra {α : Type u_1} : Mul (Seq α)

Concatenation of traces.

Equations

• Stream'.Seq.instMul_extra = { mul := Stream'.Seq.append }

@[implicit_reducible]

instance Stream'.Seq.instMonoid_extra {α : Type u_1} : Monoid (Seq α)

Equations

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

Bridging the algebraic and the Seq APIs

Deliberately not @[simp], in either direction. Mathlib's Seq lemmas are stated with append/nil and are largely @[simp]; this development's trace algebra is stated with */1 (Trace.τ, Relation.lcomp₁, every scPrefix_* lemma). Normalizing either way would leave one of the two sets unable to fire, so the normal form stays */1 — matching the rest of the development — and reaching for Mathlib's Seq API is an explicit rw.

theorem Stream'.Seq.one_eq_nil {α : Type u_1} : 1 = nil

1 is the empty sequence.

theorem Stream'.Seq.mul_eq_append {α : Type u_1} (s t : Seq α) : s * t = s.append t

Multiplication is concatenation.

Absorption

An infinite sequence swallows whatever is appended to it. Mathlib proves append_nil unconditionally but states no general absorption law, so it is proved here: the header's claim that right identity holds because of absorption rather than despite it should not rest on an unverified assertion.

theorem Stream'.Seq.append_eq_left_of_not_terminates {α : Type u_1} {s : Seq α} (h : ¬s.Terminates) (t : Seq α) : s.append t = s

Appending to a non-terminating sequence changes nothing.

theorem Stream'.Seq.mul_eq_left_of_not_terminates {α : Type u_1} {s : Seq α} (h : ¬s.Terminates) (t : Seq α) : s * t = s

append_eq_left_of_not_terminates in the algebraic vocabulary: a non-terminating trace is a left zero. This is why Seq is only a monoid and never cancellative — a product whose left factor is infinite tells you nothing about its right factor.

Infinite products

The trace of an execution that takes infinitely many steps: each step contributes a finite (in general, arbitrary) trace, and the whole is their infinite concatenation.

Corecursion is not available for this. A corecursive concatenation has to decide whether the result is empty before producing anything, and with possibly-empty pieces that decision depends on all of them — the definition would not be productive. So the product is built the other way round: as the sup of the finite partial products, taken index by index. Index k of the product is whatever index k of some partial product is, if any partial product has one; the pieces only ever extend each other, so it does not matter which.

This is total — every e : ℕ → Seq α has a product, with no side condition on the pieces being nonempty and no fairness or productivity assumption. That matters: the refinement lemma for divergence quantifies over an arbitrary step sequence, including one that emits nothing forever, and the trace it must produce there is 1.

theorem Stream'.Seq.get?_mul_of_get? {α : Type u_1} {s : Seq α} {k : ℕ} {a : α} (u : Seq α) (h : s.get? k = some a) : (s * u).get? k = some a

Appending on the right never disturbs an index the left operand already defines.

theorem Stream'.Seq.get?_partialProd_of_le {α : Type u_1} {e : ℕ → Seq α} {m n k : ℕ} {a : α} (hmn : m ≤ n) (h : (Monoid.partialProd e m).get? k = some a) : (Monoid.partialProd e n).get? k = some a

Partial products only ever grow: an index defined by one is defined, identically, by every later one.

noncomputable def Stream'.Seq.ωFun {α : Type u_1} (e : ℕ → Seq α) (k : ℕ) : Option α

Index k of the infinite product: whatever some partial product holds there, if any does. Split out of ωProduct so that the IsSeq obligation and the characterization below are stated against a name rather than against a lambda buried in an anonymous constructor.

Equations

• Stream'.Seq.ωFun e k = if h : ∃ (n : ℕ), ((Monoid.partialProd e n).get? k).isSome = true then (Monoid.partialProd e (Nat.find h)).get? k else none

theorem Stream'.Seq.ωFun_eq_some {α : Type u_1} {e : ℕ → Seq α} {k : ℕ} {a : α} : ωFun e k = some a ↔ ∃ (n : ℕ), (Monoid.partialProd e n).get? k = some a

theorem Stream'.Seq.ωFun_eq_none {α : Type u_1} {e : ℕ → Seq α} {k : ℕ} : ωFun e k = none ↔ ∀ (n : ℕ), (Monoid.partialProd e n).get? k = none

noncomputable def Stream'.Seq.ωProduct {α : Type u_1} (e : ℕ → Seq α) : Seq α

The infinite product e 0 * e 1 * ⋯, as the sup of the partial products.

Total: no hypothesis on e whatsoever.

Equations

• Stream'.Seq.ωProduct e = ⟨Stream'.Seq.ωFun e, ⋯⟩

@[simp]

theorem Stream'.Seq.get?_ωProduct_eq_ωFun {α : Type u_1} {e : ℕ → Seq α} {k : ℕ} : (ωProduct e).get? k = ωFun e k

theorem Stream'.Seq.get?_ωProduct {α : Type u_1} {e : ℕ → Seq α} {k : ℕ} {a : α} : (ωProduct e).get? k = some a ↔ ∃ (n : ℕ), (Monoid.partialProd e n).get? k = some a

What the product holds at each index: exactly what some partial product holds there.

@[simp]

theorem Stream'.Seq.ωProduct_const_one {α : Type u_1} : (ωProduct fun (x : ℕ) => 1) = 1

A step sequence that never emits has the empty trace, with no productivity assumption anywhere. The case a corecursive definition could not have produced.

Factoring out a prefix

What the aborting branch of a divergence refinement needs: the trace emitted before the abort is a factor of the whole product, so that a ≼ obligation against the product can be discharged against that factor.

The terminating case is an induction on the index at which the prefix terminates — deliberately not on its length, since relating Seq.take/Seq.drop to append would need lemmas Mathlib does not have. The non-terminating case is absorption: nothing after an infinite prefix is observable, so the product is the prefix.

theorem Stream'.Seq.exists_mul_of_get? {α : Type u_1} {n : ℕ} {s u : Seq α} : s.TerminatedAt n → (∀ (k : ℕ) (a : α), s.get? k = some a → u.get? k = some a) → ∃ (r : Seq α), u = s * r

A terminating prefix can be factored out. s terminating and defining nothing that u disagrees with means u continues s.

theorem Stream'.Seq.ωProduct_eq_of_not_terminates {α : Type u_1} {e : ℕ → Seq α} {n : ℕ} (h : ¬(Monoid.partialProd e n).Terminates) : ωProduct e = Monoid.partialProd e n

Once a partial product is infinite, every later one equals it and the whole product stops there.

theorem Stream'.Seq.exists_mul_ωProduct {α : Type u_1} (e : ℕ → Seq α) (n : ℕ) : ∃ (r : Seq α), ωProduct e = Monoid.partialProd e n * r

Every finite prefix of a Seq product is a left factor of it.

Stated without naming ωMonoid.partialProd_dvd: the law belongs to the refinement framework (VerifiedCompiler/ClosedForm.lean), which discharges it from this lemma. Keeping the mathematics predicate-free is what stops Extra/ from importing that library.

Reading past a finite left factor

get?_mul_of_get? says a concatenation agrees with its left operand wherever that operand is defined. The complementary law — what the concatenation holds after the left operand runs out — is what the unfolding law below needs, and Mathlib has neither it nor the append/take/drop lemmas one would derive it from. It is proved here directly, by recursion on the index at which the left operand terminates.

The minimality hypothesis is not decoration: without it the left operand may terminate strictly earlier than the stated index, and the two sides are then offset by the difference.

theorem Stream'.Seq.get?_mul_of_terminatedAt {α : Type u_1} {n : ℕ} {s : Seq α} : (∀ k < n, ¬s.TerminatedAt k) → s.TerminatedAt n → ∀ (t : Seq α) (j : ℕ), (s * t).get? (n + j) = t.get? j

Past its last index, a concatenation is its right operand.

theorem Stream'.Seq.exists_get?_zero_of_ne_one {α : Type u_1} {s : Seq α} (h : s ≠ 1) : ∃ (a : α), s.get? 0 = some a

A nonempty trace has a first element.

theorem Stream'.Seq.ωProduct_succ {α : Type u_1} (e : ℕ → Seq α) : ωProduct e = e 0 * ωProduct fun (i : ℕ) => e (i + 1)

The first factor comes out in front of an infinite product.

Both cases are decided by whether the first factor is finite. If it is not, absorption settles everything: the product stops there and so does the right-hand side. If it is, the two sides are compared index by index on either side of its last index — before it both are that factor, after it both are the product of the remaining factors.

Products of a sequence that keeps emitting

The converse half of the closed form needs the infinite product to be determined by its partial products, which it is only when those keep growing. Each nonempty factor extends the partial product by at least one index, so infinitely many of them reach every index — and an element sharing every partial product as a left factor then agrees with the product everywhere.

theorem Stream'.Seq.exists_get?_partialProd {α : Type u_1} {e : ℕ → Seq α} (hne : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ m ∧ e m ≠ 1) (k : ℕ) : ∃ (n : ℕ) (a : α), (Monoid.partialProd e n).get? k = some a

Infinitely many nonempty factors define every index of some partial product.

theorem Stream'.Seq.ωProduct_comp_of_ones {α : Type u_1} {e : ℕ → Seq α} {n : ℕ → ℕ} (hmono : StrictMono n) (hone : ∀ (i : ℕ), (∀ (j : ℕ), n j ≠ i) → e i = 1) : ωProduct e = ωProduct (e ∘ n)

Deleting factors that are 1 does not change the infinite product.

The fact a stuttering divergence refinement turns on. There the source moves only at a sparse set of the target's indices, so its trace sequence is the target's reindexed — while Trace.Rτ_omega relates two sequences pointwise, at the same index. This says the two products agree anyway, provided every index the reindexing skips carries 1.

Not a corollary of ωProduct_eq_of_forall_dvd: that one assumes infinitely many non-1 factors, and a silently diverging source has none at all.

The whole content is partialProd e (n j) = partialProd (e ∘ n) j, by induction on j over Monoid.partialProd_eq_of_ones; the products then agree index by index because n is cofinal (j ≤ n j) and partial products only grow.

theorem Stream'.Seq.ωProduct_eq_of_forall_dvd {α : Type u_1} {e : ℕ → Seq α} {x : Seq α} (hx : ∀ (n : ℕ), ∃ (r : Seq α), x = Monoid.partialProd e n * r) (hne : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ m ∧ e m ≠ 1) : x = ωProduct e

A Seq having every partial product as a left factor is the product, once the factors keep coming. Predicate-free for the same reason as exists_mul_ωProduct.

@[implicit_reducible]

noncomputable instance Stream'.Seq.instωMonoid {α : Type u_1} : ωMonoid (Seq α)

Seq products, with the laws refinement proofs consume.

Equations

• Stream'.Seq.instωMonoid = { ωProd := Stream'.Seq.ωProduct, partialProd_dvd := ⋯, unfold := ⋯, productLimit := ⋯, ωProd_comp := ⋯ }

@[simp]

theorem Stream'.Seq.ωProd_eq_ωProduct {α : Type u_1} {e : ℕ → Seq α} : ωMonoid.ωProd e = ωProduct e