State-indexed dependent chains (Spec.stateChain)

An n-stage state-indexed composition: at each stage i, the interaction is spec i s where s : Stage i is the current state. After the stage completes with transcript tr, the state advances to advance i s tr : Stage (i + 1).

This file provides the spec-level state chain (Spec.stateChain), a transcript telescope type (Transcript.stateChain), flattening operations (Transcript.stateChainJoin / stateChainUnjoin), type-level lifting (Transcript.stateChainLiftJoin, Transcript.stateChainFamily), decorations, and strategy composition along state chains.

For the primary (stateless, continuation-style) chain API see Spec.Chain in VCVio.Interaction.Basic.Chain.

def Interaction.Spec.stateChain (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (n i : ℕ) : Stage i → Spec

n-stage dependent composition: run spec i s, then advance to state advance i s tr and repeat for n total stages.

@[simp]

theorem Interaction.Spec.stateChain_zero (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (i : ℕ) (s : Stage i) : stateChain Stage spec advance 0 i s = done

theorem Interaction.Spec.stateChain_succ (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (n i : ℕ) (s : Stage i) : stateChain Stage spec advance (n + 1) i s = (spec i s).append fun (tr : (spec i s).Transcript) => stateChain Stage spec advance n (i + 1) (advance i s tr)

theorem Interaction.Spec.replicate_eq_stateChain (spec : Spec) (n i : ℕ) : spec.replicate n = stateChain (fun (x : ℕ) => PUnit) (fun (x : ℕ) (x_1 : (fun (x : ℕ) => PUnit) x) => spec) (fun (x : ℕ) (x_1 : (fun (x : ℕ) => PUnit) x) (x_2 : ((fun (x : ℕ) (x_2 : (fun (x : ℕ) => PUnit) x) => spec) x x_1).Transcript) => PUnit.unit) n i PUnit.unit

replicate is stateChain with trivial state PUnit.

def Interaction.Spec.Transcript.stateChainSplit {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (n i : ℕ) (s : Stage i) : (Spec.stateChain Stage spec advance (n + 1) i s).Transcript → (tr₁ : (spec i s).Transcript) × (Spec.stateChain Stage spec advance n (i + 1) (advance i s tr₁)).Transcript

Decompose a (n+1)-stage state chain transcript into the first-stage transcript and the remainder. Specialization of Transcript.split to the state chain structure.

def Interaction.Spec.Transcript.stateChainAppend {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (n i : ℕ) (s : Stage i) (tr₁ : (spec i s).Transcript) (tr₂ : (Spec.stateChain Stage spec advance n (i + 1) (advance i s tr₁)).Transcript) : (Spec.stateChain Stage spec advance (n + 1) i s).Transcript

Combine a first-stage transcript with a remainder state chain transcript into a (n+1)-stage state chain transcript. Specialization of Transcript.append to state chains.

@[simp]

theorem Interaction.Spec.Transcript.stateChainSplit_stateChainAppend {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (n i : ℕ) (s : Stage i) (tr₁ : (spec i s).Transcript) (tr₂ : (Spec.stateChain Stage spec advance n (i + 1) (advance i s tr₁)).Transcript) : stateChainSplit n i s (stateChainAppend n i s tr₁ tr₂) = ⟨tr₁, tr₂⟩

Splitting after appending at the state chain level recovers the components.

N-ary transcript operations

def Interaction.Spec.Transcript.stateChain (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (n i : ℕ) (s : Stage i) : Type u

Dependent telescope of per-stage transcripts: a sequence of individual-stage transcripts where each stage determines the next via advance. Mirrors Spec.stateChain at the transcript level.

def Interaction.Spec.Transcript.stateChainJoin (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (n i : ℕ) (s : Stage i) : stateChain Stage spec advance n i s → (Spec.stateChain Stage spec advance n i s).Transcript

Flatten a transcript telescope into the combined state chain transcript, concatenating each per-stage transcript via Transcript.stateChainAppend. The n-ary analog of Transcript.append, mirroring List.join.

def Interaction.Spec.Transcript.stateChainUnjoin (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (n i : ℕ) (s : Stage i) : (Spec.stateChain Stage spec advance n i s).Transcript → stateChain Stage spec advance n i s

Decompose a combined state chain transcript into a telescope of per-stage transcripts. Inverse of Transcript.stateChainJoin.

@[simp]

theorem Interaction.Spec.Transcript.stateChainUnjoin_join {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (n i : ℕ) (s : Stage i) (trs : stateChain Stage spec advance n i s) : stateChainUnjoin Stage spec advance n i s (stateChainJoin Stage spec advance n i s trs) = trs

stateChainUnjoin after stateChainJoin is the identity on telescope transcripts.

@[simp]

theorem Interaction.Spec.Transcript.stateChainJoin_unjoin {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (n i : ℕ) (s : Stage i) (tr : (Spec.stateChain Stage spec advance n i s).Transcript) : stateChainJoin Stage spec advance n i s (stateChainUnjoin Stage spec advance n i s tr) = tr

stateChainJoin after stateChainUnjoin is the identity on combined state chain transcripts.

def Interaction.Spec.Transcript.stateChainLiftJoin (Stage : ℕ → Type u) (spec : (i : ℕ) → Stage i → Spec) (advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)) (n i : ℕ) (s : Stage i) : (stateChain Stage spec advance n i s → Type u) → (Spec.stateChain Stage spec advance n i s).Transcript → Type u

Lift a family indexed by the transcript telescope to a family on the combined state chain transcript. Uses Transcript.liftAppend at each stage, ensuring that stateChainLiftJoin ... F (stateChainJoin ... trs) reduces definitionally to F trs.

def Interaction.Spec.Decoration.stateChain {S : Type u → Type v} {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (deco : (i : ℕ) → (s : Stage i) → Decoration S (spec i s)) (n i : ℕ) (s : Stage i) : Decoration S (Spec.stateChain Stage spec advance n i s)

Per-node labels along a state chain: at each stage, use deco i s.

def Interaction.Spec.Decoration.Over.stateChain {L : Type u → Type v} {F : (X : Type u) → L X → Type w} {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {deco : (i : ℕ) → (s : Stage i) → Decoration L (spec i s)} (rDeco : (i : ℕ) → (s : Stage i) → Over F (spec i s) (deco i s)) (n i : ℕ) (s : Stage i) : Over F (Spec.stateChain Stage spec advance n i s) (Decoration.stateChain deco n i s)

Dependent decoration layer along a state chain, fibered over Decoration.stateChain.

theorem Interaction.Spec.Decoration.Over.map_stateChain {L : Type u → Type v} {F G : (X : Type u) → L X → Type w} (η : (X : Type u) → (l : L X) → F X l → G X l) {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {deco : (i : ℕ) → (s : Stage i) → Decoration L (spec i s)} (rDeco : (i : ℕ) → (s : Stage i) → Over F (spec i s) (deco i s)) (n i : ℕ) (s : Stage i) : map η (Spec.stateChain Stage spec advance n i s) (Decoration.stateChain deco n i s) (stateChain rDeco n i s) = stateChain (fun (j : ℕ) (t : Stage j) => map η (spec j t) (deco j t) (rDeco j t)) n i s

Over.map commutes with Over.stateChain.

State chain families

def Interaction.Spec.Transcript.stateChainFamily {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (Family : (i : ℕ) → Stage i → Type u) (n i : ℕ) (stage : Stage i) : (Spec.stateChain Stage spec advance n i stage).Transcript → Type u

The output type of state chain composition. Given a per-stage family Family i s, this computes the type at the terminal stage by threading through Transcript.liftAppend at each step. Reduces definitionally when the transcript is built via Transcript.append, avoiding Nat-arithmetic casts.

This is the canonical output type for Strategy.stateChainComp and Counterpart.stateChainComp.

@[simp]

theorem Interaction.Spec.Transcript.stateChainFamily_zero {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (Family : (i : ℕ) → Stage i → Type u) (i : ℕ) (s : Stage i) (tr : PUnit) : stateChainFamily Family 0 i s tr = Family i s

theorem Interaction.Spec.Transcript.stateChainFamily_const {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} (α : Type u) (n i : ℕ) (s : Stage i) (tr : (Spec.stateChain Stage spec advance n i s).Transcript) : stateChainFamily (fun (x : ℕ) (x_1 : Stage x) => α) n i s tr = α

A constant family is unaffected by stateChainFamily.

Strategy composition along state chains

def Interaction.Spec.Strategy.stateChainComp {m : Type u → Type u} [Monad m] {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {Family : (i : ℕ) → Stage i → Type u} (step : (i : ℕ) → (s : Stage i) → Family i s → m (Strategy m (spec i s) fun (tr : (spec i s).Transcript) => Family (i + 1) (advance i s tr))) (n i : ℕ) (s : Stage i) : Family i s → m (Strategy m (stateChain Stage spec advance n i s) (Transcript.stateChainFamily Family n i s))

Compose per-stage strategies along a state chain. At each stage, the step function transforms Family i s into a strategy whose output is Family (i+1) (advance i s tr). The full state chain output is Transcript.stateChainFamily Family.