The sequencer: heterogeneous stages in a row

The matrix of a step formula is evaluated atom by atom, and the gates block by block: a sequence of machineries of different shapes – a stage atom's random access here, a tag-branched element loop there – with a checkpoint between consecutive ones and an exit after the last. The chain combinator of DescriptiveComplexity.Problems.Wide.DrawChain fixes a single stage family; this file is its dependent sibling: n stages with their own phase and shape types (PA/SA-indexed families), n + 1 checkpoints, the k-th dispatching into stage k's entry and the last leaving.

The per-stage machineries and their separation are parameters, so the matrix instantiates this with the kind-dependent atom machineries and the gates with the per-block gate machinery, and neither needs a new checkpoint proof.

The shapes

inductive DescriptiveComplexity.Draw.SeqPh (n : ℕ) (PA : Fin n → Type) : Type

The phases of a sequence: n + 1 checkpoints and the stages'.

• chk {n : ℕ} {PA : Fin n → Type} : Fin (n + 1) → SeqPh n PA

  The checkpoint before stage k (at k = n: after the last).

• sub {n : ℕ} {PA : Fin n → Type} (a : Fin n) : PA a → SeqPh n PA

  A phase of stage a.

inductive DescriptiveComplexity.Draw.SeqSite (n : ℕ) (SA : Fin n → Type) : Type

The sites of a sequence.

• chk {n : ℕ} {SA : Fin n → Type} : Fin (n + 1) → SeqSite n SA

  A checkpoint site.

• sub {n : ℕ} {SA : Fin n → Type} (a : Fin n) : SA a → SeqSite n SA

  A site of stage a.

def DescriptiveComplexity.Draw.SeqSh (n : ℕ) {SA : Fin n → Type} (ShA : (a : Fin n) → SA a → Type) : SeqSite n SA → Type

The rule shape of each sequence site.

Equations

• DescriptiveComplexity.Draw.SeqSh n ShA (DescriptiveComplexity.Draw.SeqSite.chk a) = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.SeqSh n ShA (DescriptiveComplexity.Draw.SeqSite.sub a s) = ShA a s

def DescriptiveComplexity.Draw.seqOwn {n : ℕ} {PA SA : Fin n → Type} (ownA : (a : Fin n) → PA a → SA a) : SeqPh n PA → SeqSite n SA

The owner of each phase of a sequence, over the stages' owners.

Equations

• DescriptiveComplexity.Draw.seqOwn ownA (DescriptiveComplexity.Draw.SeqPh.chk k) = DescriptiveComplexity.Draw.SeqSite.chk k
• DescriptiveComplexity.Draw.seqOwn ownA (DescriptiveComplexity.Draw.SeqPh.sub a p) = DescriptiveComplexity.Draw.SeqSite.sub a (ownA a p)

def DescriptiveComplexity.Draw.seqRule {A Q W P : Type} {n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} (one : A) (wk rg : W) (emb : SeqPh n PA → P) (ruleA : (a : Fin n) → (s : SA a) → ShA a s → Rule A Q W P) (entry : (a : Fin n) → PA a) (enterSt : Fin n → (Q → A) → (W → A) → Q → A) (exitPh : P) (i : SeqSite n SA) : SeqSh n ShA i → Rule A Q W P

The rules of a sequence: per checkpoint the walk back and the dispatch – into the next stage's entry, or out after the last.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.seqRule one wk rg emb ruleA entry enterSt exitPh (DescriptiveComplexity.Draw.SeqSite.sub a s) ρ = ruleA a s ρ

theorem DescriptiveComplexity.Draw.seqRule_dstIn {A Q W P : Type} {n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} (one : A) (wk rg : W) (emb : SeqPh n PA → P) (ruleA : (a : Fin n) → (s : SA a) → ShA a s → Rule A Q W P) (entry : (a : Fin n) → PA a) (enterSt : Fin n → (Q → A) → (W → A) → Q → A) (exitPh : P) {S : P → Prop} (hemb : ∀ (p : SeqPh n PA), S (emb p)) (hexit : S exitPh) (hA : ∀ (a : Fin n) (s : SA a) (ρ : ShA a s), S (ruleA a s ρ).dstPh) (i : SeqSite n SA) (ρ : SeqSh n ShA i) : S (seqRule one wk rg emb ruleA entry enterSt exitPh i ρ).dstPh

A property of a sequence's phases and its exit holds of every phase it can move to, given it holds of every phase a stage can move to.

theorem DescriptiveComplexity.Draw.seqHosrc {A Q W P : Type} {n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} (one : A) (wk rg : W) (emb : SeqPh n PA → P) (ruleA : (a : Fin n) → (s : SA a) → ShA a s → Rule A Q W P) (entry : (a : Fin n) → PA a) (enterSt : Fin n → (Q → A) → (W → A) → Q → A) (exitPh : P) (ownA : (a : Fin n) → PA a → SA a) (hosrcA : ∀ (a : Fin n) (s : SA a) (ρ : ShA a s), ∃ (p : PA a), (ruleA a s ρ).srcPh = emb (SeqPh.sub a p) ∧ ownA a p = s) (i : SeqSite n SA) (ρ : SeqSh n ShA i) : ∃ (p : SeqPh n PA), (seqRule one wk rg emb ruleA entry enterSt exitPh i ρ).srcPh = emb p ∧ seqOwn ownA p = i

Every rule of a sequence fires from a phase its site owns; the stages' obligation is the parameter.

theorem DescriptiveComplexity.Draw.seqSep {A Q W P : Type} {n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} (one : A) (wk rg : W) (emb : SeqPh n PA → P) (ruleA : (a : Fin n) → (s : SA a) → ShA a s → Rule A Q W P) (entry : (a : Fin n) → PA a) (enterSt : Fin n → (Q → A) → (W → A) → Q → A) (exitPh : P) (hsepA : ∀ (a : Fin n) (s : SA a) (ρ ρ' : ShA a s) (f : Q → A) (g : W → A), (ruleA a s ρ).guard f g → (ruleA a s ρ').guard f g → (ruleA a s ρ).srcPh = (ruleA a s ρ').srcPh → ρ = ρ') (i : SeqSite n SA) (ρ ρ' : SeqSh n ShA i) (f : Q → A) (g : W → A) : (seqRule one wk rg emb ruleA entry enterSt exitPh i ρ).guard f g → (seqRule one wk rg emb ruleA entry enterSt exitPh i ρ').guard f g → (seqRule one wk rg emb ruleA entry enterSt exitPh i ρ).srcPh = (seqRule one wk rg emb ruleA entry enterSt exitPh i ρ').srcPh → ρ = ρ'

A sequence separates in-shape: the checkpoints by the gadget's guards, the stages by their parameter.