Spec.replicate and transcript operations

Non-dependent n-fold append of the same spec, with Transcript.replicateJoin / replicateSplit, replicated decorations/refinements, and Strategy.iterate. This is the uniform special case of Spec.stateChain (see VCVio.Interaction.Basic.StateChain).

def Interaction.Spec.replicate (spec : Spec) (n : ℕ) : Spec

n-fold dependent append of spec with trivial continuation (fun _ => replicate …).

@[simp]

theorem Interaction.Spec.replicate_zero (spec : Spec) : spec.replicate 0 = done

theorem Interaction.Spec.replicate_succ (spec : Spec) (n : ℕ) : spec.replicate (n + 1) = spec.append fun (x : spec.Transcript) => spec.replicate n

@[reducible, inline]

abbrev Interaction.Spec.Transcript.replicateCons (spec : Spec) (n : ℕ) : spec.Transcript → (spec.replicate n).Transcript → (spec.replicate (n + 1)).Transcript

Prepend one transcript to a length-n replicated tail.

@[reducible, inline]

abbrev Interaction.Spec.Transcript.replicateUncons (spec : Spec) (n : ℕ) : (spec.replicate (n + 1)).Transcript → spec.Transcript × (spec.replicate n).Transcript

Split the head round from a length-(n+1) replicated transcript.

def Interaction.Spec.Transcript.replicateJoin (spec : Spec) (n : ℕ) : (Fin n → spec.Transcript) → (spec.replicate n).Transcript

Combine n transcripts of spec into one of spec.replicate n.

def Interaction.Spec.Transcript.replicateSplit (spec : Spec) (n : ℕ) : (spec.replicate n).Transcript → Fin n → spec.Transcript

Split spec.replicate n into n per-round transcripts.

@[simp]

theorem Interaction.Spec.Transcript.replicateSplit_replicateJoin (spec : Spec) (n : ℕ) (trs : Fin n → spec.Transcript) (i : Fin n) : replicateSplit spec n (replicateJoin spec n trs) i = trs i

theorem Interaction.Spec.Transcript.replicateSplit_join_zero (spec : Spec) (n : ℕ) (hd : spec.Transcript) (tl : (spec.replicate n).Transcript) : replicateSplit spec (n + 1) (append spec (fun (x : spec.Transcript) => spec.replicate n) hd tl) ⟨0, ⋯⟩ = hd

theorem Interaction.Spec.Transcript.replicateSplit_join_succ (spec : Spec) (n : ℕ) (hd : spec.Transcript) (tl : (spec.replicate n).Transcript) (i : Fin n) : replicateSplit spec (n + 1) (append spec (fun (x : spec.Transcript) => spec.replicate n) hd tl) i.succ = replicateSplit spec n tl i

@[simp]

theorem Interaction.Spec.Transcript.replicateJoin_replicateSplit (spec : Spec) (n : ℕ) (tr : (spec.replicate n).Transcript) : replicateJoin spec n (replicateSplit spec n tr) = tr

def Interaction.Spec.Decoration.replicate {S : Type u → Type v} {spec : Spec} (d : Decoration S spec) (n : ℕ) : Decoration S (spec.replicate n)

Replicate a decoration n times along Spec.replicate.

def Interaction.Spec.Decoration.Over.replicate {L : Type u → Type v} {F : (X : Type u) → L X → Type w} {spec : Spec} {d : Decoration L spec} (r : Over F spec d) (n : ℕ) : Over F (spec.replicate n) (d.replicate n)

Replicate a dependent decoration n times along replicated base decorations.

theorem Interaction.Spec.Decoration.map_replicate {S : Type u → Type v} {T : Type u → Type w} (f : (X : Type u) → S X → T X) {spec : Spec} (d : Decoration S spec) (n : ℕ) : map f (spec.replicate n) (d.replicate n) = (map f spec d).replicate n

Decoration.map commutes with Decoration.replicate.

theorem Interaction.Spec.Decoration.Over.map_replicate {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) {spec : Spec} {d : Decoration L spec} (r : Over F spec d) (n : ℕ) : map η (spec.replicate n) (d.replicate n) (r.replicate n) = (map η spec d r).replicate n

Decoration.Over.map commutes with Over.replicate.

def Interaction.Spec.Strategy.iterate {m : Type u → Type u} [Monad m] {spec : Spec} {α : Type u} (n : ℕ) (step : Fin n → α → m (Strategy m spec fun (x : spec.Transcript) => α)) : α → m (Strategy m (spec.replicate n) fun (x : (spec.replicate n).Transcript) => α)

Iterate a strategy n times on spec.replicate n, threading a value of type α.