Kits for the round trips: the file test

The kit wrapping the file-test round trip, by the template of DescriptiveComplexity.Problems.Wide.DrawKit: a phase inductive, a rule inductive with concrete guards, the rules function at a phase embedding, an in-shape separation lemma, and a discharge – any program whose rule set contains the kit's rules satisfies the composite's run theorem (DescriptiveComplexity.Draw.TestKit.reaches_pos/_neg: scan up to the file top, bounce, one question per register on the way down, verdict in the phase, return to the marker).

The verdict phases double as return phases, which is where the cell-coupled forms of the layer earn their keep: the walking rule of the passing phase is guarded rg ≠ one ∧ wk ≠ one, disjoint from the register rules, and the coupled hypotheses of DescriptiveComplexity.Draw.Prog.reaches_fileRoundTrip are exactly what shows it fires wherever the composite needs it. The failing phase hosts no register rule, so its single rule takes the disjunction rg = one ∨ wk ≠ one and serves hold, walk and return at once.

Rules are owned by their source phase: how a program enters the kit (at the scan phase, off the marker) and how it leaves the two verdict phases (at the marker, guarded wk = one ∧ rg ≠ one, disjoint from every rule here) is the caller's business.

The file test's shapes

inductive DescriptiveComplexity.Draw.TestPh : Type

The phases of a test trip: the up-scan, the bounce, and the two verdict phases – the passing one doubling as the descent phase of the pass.

• up : TestPh

  Scanning up to the file top.

• b2 : TestPh

  Bounced off the top, about to re-enter rightwards.

• ty : TestPh

  Every register so far passed (also: returning with verdict yes).

• tn : TestPh

  Some register failed (also: returning with verdict no).

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTestPh : DecidableEq TestPh

Equations

• DescriptiveComplexity.Draw.instDecidableEqTestPh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteTestPh : Finite TestPh

inductive DescriptiveComplexity.Draw.TestRule : Type

The rule families of a test trip, one constructor each.

• up : TestRule

  Scan right while the file-top mark is clear.

• b1 : TestRule

  At the file top: step left into the bounce phase.

• b2go : TestRule

  Bounce: step back right into the pass.

• pass : TestRule

  At a register that passes the question: carry on down.

• fail : TestRule

  At a register that fails it: switch to the failing phase.

• walkY : TestRule

  Walk left over unmarked cells, and return, in the passing phase.

• stayN : TestRule

  Hold at registers, walk and return, in the failing phase.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTestRule : DecidableEq TestRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqTestRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteTestRule : Finite TestRule

structure DescriptiveComplexity.Draw.TestKit (A Q W P : Type) : Type

A file-test kit: the walked track, the three service slots, the per-register question as a predicate of the tracks, and where its phases sit in the program.

• t : W

  The walked track being questioned.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• TestG : (W → A) → Prop

  The per-register question, decided by the tracks.

• emb : TestPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.TestKit.rule {A Q W P : Type} (κ : TestKit A Q W P) (one : A) : TestRule → Rule A Q W P

The kit's rules.

Equations

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

The discharge

theorem DescriptiveComplexity.Draw.TestKit.reaches_pos {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : TestKit A Q W P} {rEmb : TestRule → R} (hrules : ∀ (ρ : TestRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {Test : I → Prop} (hcompat : ∀ (u : I), κ.TestG (PR.passTracksAt F.cell κ.t rest m (F.cell u)) ↔ Test u) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) (hTest : ∀ (u : I), Test u) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb TestPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb TestPh.ty) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs a passing file test, the budget forgotten.

The clear and copy trips

The same itinerary with a writing pass in the middle: one phase runs the descent and the return alike, its register rule rewriting the walked digit and its walking rule – guarded rg ≠ one ∧ wk ≠ one – serving the gaps of the file and the way home.

inductive DescriptiveComplexity.Draw.TrackPh : Type

The phases of a write-pass trip: the up-scan, the bounce, and the one pass-and-return phase.

• up : TrackPh

  Scanning up to the file top.

• b2 : TrackPh

  Bounced off the top, about to re-enter rightwards.

• run : TrackPh

  Running the pass down the file, and returning.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTrackPh : DecidableEq TrackPh

Equations

• DescriptiveComplexity.Draw.instDecidableEqTrackPh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteTrackPh : Finite TrackPh

inductive DescriptiveComplexity.Draw.TrackRule : Type

The rule families of a write-pass trip.

• up : TrackRule

  Scan right while the file-top mark is clear.

• b1 : TrackRule

  At the file top: step left into the bounce phase.

• b2go : TrackRule

  Bounce: step back right into the pass.

• put : TrackRule

  At a register: rewrite the walked digit and carry on down.

• walk : TrackRule

  Walk left over unmarked cells, and return.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqTrackRule : DecidableEq TrackRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqTrackRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteTrackRule : Finite TrackRule

structure DescriptiveComplexity.Draw.ClearKit (A Q W P : Type) : Type

A track-clearing kit: the walked track, the three service slots, and the phases.

• t : W

  The walked track being cleared.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• emb : TrackPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.ClearKit.rule {A Q W P : Type} [DecidableEq W] (κ : ClearKit A Q W P) (zero one : A) : TrackRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.ClearKit.wkOff {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : ClearKit A Q W P} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (k : I → Prop) (r : Univ A R P K dd → Prop) (hbnd : ∃ (x : I), WMSetLe WMLe (F.cell x) r) : PR.passTracksAt F.cell κ.t rest k r κ.wk ≠ PR.one

theorem DescriptiveComplexity.Draw.ClearKit.rgOff {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {κ : ClearKit A Q W P} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hnerg : κ.t ≠ κ.rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (k : I → Prop) (r : Univ A R P K dd → Prop) (hno : ∀ (x : I), r ≠ F.cell x) : PR.passTracksAt F.cell κ.t rest k r κ.rg ≠ PR.one

structure DescriptiveComplexity.Draw.CopyKit (A Q W P : Type) : Type

A track-copying kit: the walked track, the source slot – which must hold a bit at every register – the three service slots, and the phases.

• t : W

  The walked track being overwritten.

• src : W

  The source slot whose digit is copied.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• emb : TrackPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.CopyKit.rule {A Q W P : Type} [DecidableEq W] (κ : CopyKit A Q W P) (one : A) : TrackRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.CopyKit.wkOff {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : CopyKit A Q W P} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (k : I → Prop) (r : Univ A R P K dd → Prop) (hbnd : ∃ (x : I), WMSetLe WMLe (F.cell x) r) : PR.passTracksAt F.cell κ.t rest k r κ.wk ≠ PR.one

theorem DescriptiveComplexity.Draw.CopyKit.rgOff {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {κ : CopyKit A Q W P} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hnerg : κ.t ≠ κ.rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (k : I → Prop) (r : Univ A R P K dd → Prop) (hno : ∀ (x : I), r ≠ F.cell x) : PR.passTracksAt F.cell κ.t rest k r κ.rg ≠ PR.one

structure DescriptiveComplexity.Draw.MapKit (A Q W P : Type) : Type

A track-mapping kit: the walked track is rewritten by a bit the other tracks at each register decide – the pattern writes of the program, a target register loaded from the marks. The function ignoring the walked slot is the discharge's frame hypothesis.

• t : W

  The walked track being overwritten.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• Fb : (W → A) → Prop

  The written bit, computed from the tracks.

• emb : TrackPh → P

  The kit's phases in the program.

noncomputable def DescriptiveComplexity.Draw.MapKit.rule {A Q W P : Type} [DecidableEq W] (κ : MapKit A Q W P) (zero one : A) : TrackRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.MapKit.wkOff {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {κ : MapKit A Q W P} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnewk : κ.wk ≠ κ.t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) (k : I → Prop) (r : Univ A R P K dd → Prop) (hbnd : ∃ (x : I), WMSetLe WMLe (F.cell x) r) : PR.passTracksAt F.cell κ.t rest k r κ.wk ≠ PR.one

theorem DescriptiveComplexity.Draw.MapKit.rgOff {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {κ : MapKit A Q W P} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hnerg : κ.t ≠ κ.rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (k : I → Prop) (r : Univ A R P K dd → Prop) (hno : ∀ (x : I), r ≠ F.cell x) : PR.passTracksAt F.cell κ.t rest k r κ.rg ≠ PR.one