Finite-branching ornament on interaction specs

Interaction.Spec.Fintype spec is the recursive typeclass-level ornament asserting that every move space appearing in spec : Spec.{0} carries Fintype and Nonempty instances.

This is the tree-shaped analog of OracleSpec.Fintype extends PFunctor.Fintype: OracleSpec has one layer of positions (a single polynomial functor), so a single PFunctor.Fintype witness suffices. Spec is a tree of nodes, so the ornament recurses into every subtree.

A Spec.Fintype spec instance is the data needed to derive a canonical uniform sampler Spec.Sampler.uniform : Sampler ProbComp spec built by uniform selection at each node (see VCVio.Interaction.UC.Runtime).

class inductive Interaction.Spec.Fintype : Spec → Type 1

Recursive finite-branching ornament on an interaction spec.

The .done case holds vacuously. At a .node X rest the ornament bundles Fintype and Nonempty witnesses for the move space X together with a per-branch ornament on every continuation rest x. Typeclass synthesis builds these up structurally from concrete spec trees via the companion instances below, the same way OracleSpec.Fintype synthesizes from PFunctor.Fintype.

• done : Spec.done.Fintype
• node {X : Type} (hFin : Fintype X) (hNon : Nonempty X) {rest : X → Spec} (hRec : (x : X) → (rest x).Fintype) : (Spec.node X rest).Fintype

@[implicit_reducible]

instance Interaction.Spec.Fintype.instDone : Spec.done.Fintype

Canonical Spec.Fintype instance for the terminal spec.

@[implicit_reducible]

instance Interaction.Spec.Fintype.instNode {X : Type} [hFin : Fintype X] [hNon : Nonempty X] {rest : X → Spec} [hRec : (x : X) → (rest x).Fintype] : (Spec.node X rest).Fintype

Canonical Spec.Fintype instance for a node: synthesizes from Fintype X, Nonempty X, and a per-branch ornament.

@[reducible]

def Interaction.Spec.Fintype.rootFintype {X : Type} {rest : X → Spec} (h : (Spec.node X rest).Fintype) : Fintype X

Extract the Fintype instance for the move space of the root node.

@[reducible]

def Interaction.Spec.Fintype.rootNonempty {X : Type} {rest : X → Spec} (h : (Spec.node X rest).Fintype) : Nonempty X

Extract the Nonempty instance for the move space of the root node.

@[reducible]

def Interaction.Spec.Fintype.tail {X : Type} {rest : X → Spec} (h : (Spec.node X rest).Fintype) (x : X) : (rest x).Fintype

Extract the ornament for every continuation of the root node.