Generated control families: the runs, iterated #
The run theorems of the layer take their control evolution as abstract
families over the enumeration – fsOf a j, the pointer before the j-th
read of round a – tied together by per-cover equations. An instantiation
has to produce such a family, and its rounds are defined by iteration: the
next round's entry is a function of the previous round's exit. This file
builds the family once, for every instantiation:
DescriptiveComplexity.Draw.iterOrd– a state iterated along a finite linear order, by recursion onDescriptiveComplexity.orank(the bottom is the base, each cover one step);DescriptiveComplexity.Draw.chainSt– the within-round read chain, each read's stored bit chosen classically;DescriptiveComplexity.Draw.elem_run_iter– the element loop's run at the generated family: the caller supplies only the name guards at the generated states, the exhaustion conditions, and the geometry.
Iteration along a finite linear order #
noncomputable def
DescriptiveComplexity.Draw.iterState
{ι : Type}
{Q' : Type u_1}
[LinearOrder ι]
(init : Q')
(step : ι → Q' → Q')
:
ℕ → Q'
The iterated state at a rank: the base at 0, one step per rank – the
element of that rank supplying the step's index.
Equations
- One or more equations did not get rendered due to their size.
- DescriptiveComplexity.Draw.iterState init step 0 = init
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.iterOrd
{ι : Type}
{Q' : Type u_1}
[LinearOrder ι]
(init : Q')
(step : ι → Q' → Q')
(a : ι)
:
Q'
A state iterated along the order: the base at the bottom, one step per cover.
Equations
- DescriptiveComplexity.Draw.iterOrd init step a = DescriptiveComplexity.Draw.iterState init step (DescriptiveComplexity.orank a)
Instances For
Dependency graph
The within-round read chain #
noncomputable def
DescriptiveComplexity.Draw.chainSt
{Q' : Type}
{nr : ℕ}
(bit : Fin nr → Prop)
(upd : Fin nr → Bool → Q' → Q')
(base : Q')
:
ℕ → Q'
The read chain of one round: the j-th prefix of the reads applied
to the round's entry state, each stored bit the read's.
Equations
- One or more equations did not get rendered due to their size.
- DescriptiveComplexity.Draw.chainSt bit upd base 0 = base
Instances For
Dependency graph
@[simp]
Dependency graph
The element loop's run, at the generated family #
noncomputable def
DescriptiveComplexity.Draw.elemIter
{A R P Q W K : Type}
{dd nr : ℕ}
{I : Type}
(setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A)
(initEl advEl : (Q → A) → (W → A) → Q → A)
{ι : Type}
[LinearOrder ι]
(rest : (Univ A R P K dd → Prop) → W → A)
(v : Univ A R P K dd → Prop)
(m : Fin nr → I → Prop)
(xOf : ι → Fin nr → I)
(f₀ : Q → A)
(a : ι)
:
Q → A
The generated round-entry state: the loop's initEl at the bottom,
each cover the previous round's reads folded and advanced.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.elemFam
{A R P Q W K : Type}
{dd nr : ℕ}
{I : Type}
(setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A)
(initEl advEl : (Q → A) → (W → A) → Q → A)
{ι : Type}
[LinearOrder ι]
(rest : (Univ A R P K dd → Prop) → W → A)
(v : Univ A R P K dd → Prop)
(m : Fin nr → I → Prop)
(xOf : ι → Fin nr → I)
(f₀ : Q → A)
(a : ι)
(j : Fin (nr + 1))
:
Q → A
The generated within-round family: the read chain of round a
applied to its entry state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The background is read at the working cell alone. Both generated
families mention rest only as rest v, so a background that moves
elsewhere – at a register cell, say, where the four register slots live –
generates the same control. This is what makes a loop blind to the two
scratch registers of the state it is run at.
theorem
DescriptiveComplexity.Draw.elemFam_congr_rest
{A R P Q W K : Type}
{dd nr : ℕ}
{I : Type}
{setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A}
{initEl advEl : (Q → A) → (W → A) → Q → A}
{ι : Type}
[LinearOrder ι]
{rest : (Univ A R P K dd → Prop) → W → A}
{v : Univ A R P K dd → Prop}
{m : Fin nr → I → Prop}
{rest' : (Univ A R P K dd → Prop) → W → A}
(h : rest v = rest' v)
(xOf : ι → Fin nr → I)
(f₀ : Q → A)
(a : ι)
(j : Fin (nr + 1))
:
Two backgrounds agreeing at the working cell give one within-round family.
Dependency graph
theorem
DescriptiveComplexity.Draw.elem_run_iter
{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}
{nr : ℕ}
{I : Type}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : ElemPh nr → P}
{rdTrack : Fin nr → W}
{MatchOf : Fin nr → (Q → A) → (W → A) → Prop}
{setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A}
{initEl advEl exitSt : (Q → A) → (W → A) → Q → A}
{IsMaxEl : (Q → A) → Prop}
{exitPh : P}
{rEmb : (i : ElemSite nr) → ElemSh nr i → R}
{ι : Type}
[LinearOrder ι]
[Finite ι]
{rest : (Univ A R P K dd → Prop) → W → A}
{v : Univ A R P K dd → Prop}
{m : Fin nr → I → Prop}
(hrules :
∀ (i : ElemSite nr) (ρ : ElemSh nr i),
PR.rules (rEmb i ρ) = elemRule PR.one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{v' : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
(hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u))
(hm : ∀ (j : Fin nr) (r : Univ A R P K dd → Prop), rest r (rdTrack j) = bitVal PR.zero PR.one (bitAtOf RF.cell (m j) r))
(hnewk : ∀ (j : Fin nr), wk ≠ rdTrack j)
(hnerg : ∀ (j : Fin nr), rg ≠ rdTrack j)
{t₀ : W}
{m₀ : I → Prop}
(hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r))
(hwkt₀ : wk ≠ t₀)
(hrgt₀ : rg ≠ t₀)
{a₀ aT : ι}
(hbotI : ∀ (a : ι), a₀ ≤ a)
(htopI : ∀ (a : ι), a ≤ aT)
(xOf : ι → Fin nr → I)
(f₀ : Q → A)
(hname :
∀ (a : ι) (j : Fin nr),
MatchOf j (elemFam setFlag initEl advEl rest v m xOf f₀ a j.castSucc)
(PR.passTracksAt RF.cell (rdTrack j) rest (m j) (RF.cell (xOf a j))))
(huniq :
∀ (a : ι) (j : Fin nr) (r : Univ A R P K dd → Prop),
MatchOf j (elemFam setFlag initEl advEl rest v m xOf f₀ a j.castSucc)
(PR.passTracksAt RF.cell (rdTrack j) rest (m j) r) →
r = RF.cell (xOf a j))
(hmaxT : IsMaxEl (elemFam setFlag initEl advEl rest v m xOf f₀ aT (Fin.last nr)))
(hmaxF : ∀ a < aT, ¬IsMaxEl (elemFam setFlag initEl advEl rest v m xOf f₀ a (Fin.last nr)))
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt (emb ElemPh.e0) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
{ state :=
Sum.inr (PR.stElt exitPh (exitSt (elemFam setFlag initEl advEl rest v m xOf f₀ aT (Fin.last nr)) (rest v))),
head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
The element loop's run at the generated family, the budget forgotten.
Dependency graph
The tag-branched machinery's run, at the generated families #
noncomputable def
DescriptiveComplexity.Draw.tagFam
{A R P Q W K : Type}
{dd m : ℕ}
{I : Type}
(setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A)
(rest : (Univ A R P K dd → Prop) → W → A)
(v : Univ A R P K dd → Prop)
(mT : Fin m → I → Prop)
(xT : Fin m → I)
(f₀ : Q → A)
(i : Fin (m + 1))
:
Q → A
The generated witness chain: the i-th prefix of the witness reads
applied to the entry control, each one-hot bit the read's.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The tuple loop's run, at the generated families #
noncomputable def
DescriptiveComplexity.Draw.tupleIterD
{I ι : Type}
[LinearOrder ι]
(mSrc : I → Prop)
(xS xD : ι → I)
(mD₀ : I → Prop)
(a : ι)
:
I → Prop
The generated destination track: empty of the loop's bits at the bottom, each cover the round's copy applied.
Equations
- DescriptiveComplexity.Draw.tupleIterD mSrc xS xD mD₀ a = DescriptiveComplexity.Draw.iterOrd mD₀ (fun (a' : ι) (m : I → Prop) (y : I) => y = xD a' ∧ mSrc (xS a') ∨ y ≠ xD a' ∧ m y) a
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.tupleIter0
{A R P Q W K : Type}
{dd : ℕ}
{I : Type}
(setBit : Bool → (Q → A) → (W → A) → Q → A)
(initLv advLv : (Q → A) → (W → A) → Q → A)
{ι : Type}
[LinearOrder ι]
(mSrc : I → Prop)
(v : Univ A R P K dd → Prop)
(restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A)
(xS xD : ι → I)
(mD₀ : I → Prop)
(f₀ : Q → A)
(a : ι)
:
Q → A
The generated pre-store control: the loop's initLv at the bottom,
each cover the previous round folded and advanced, the round's symbol read
from the destination-dependent background.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.tupleIter1
{A R P Q W K : Type}
{dd : ℕ}
{I : Type}
(setBit : Bool → (Q → A) → (W → A) → Q → A)
(initLv advLv : (Q → A) → (W → A) → Q → A)
{ι : Type}
[LinearOrder ι]
(mSrc : I → Prop)
(v : Univ A R P K dd → Prop)
(restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A)
(xS xD : ι → I)
(mD₀ : I → Prop)
(f₀ : Q → A)
(a : ι)
:
Q → A
The generated post-store control: the round's bit stored.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.tuple_run_iter
{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}
{I : Type}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : ChainPh 3 TuplePS → P}
{tSrc tDst : W}
{MatchS MatchD : (Q → A) → (W → A) → Prop}
{bitFlag : (Q → A) → Prop}
{setBit : Bool → (Q → A) → (W → A) → Q → A}
{initLv advLv : (Q → A) → (W → A) → Q → A}
{IsMaxLv : (Q → A) → Prop}
{exitPh : P}
{ι : Type}
[LinearOrder ι]
[Finite ι]
{mSrc : I → Prop}
{v : Univ A R P K dd → Prop}
{restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A}
{rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R}
(hrules :
∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i),
PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{v' : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{a₀ aT : ι}
(hbotI : ∀ (a : ι), a₀ ≤ a)
(htopI : ∀ (a : ι), a ≤ aT)
(xS xD : ι → I)
(mD₀ : I → Prop)
(f₀ : Q → A)
(hwkS : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r wk = bitVal PR.zero PR.one (r = v))
(hrg : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u))
(hsrc :
∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r tSrc = bitVal PR.zero PR.one (bitAtOf RF.cell mSrc r))
(hdst : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r tDst = bitVal PR.zero PR.one (bitAtOf RF.cell m' r))
(hoff : ∀ (m₁ m₂ : I → Prop) (r : Univ A R P K dd → Prop) (s : W), s ≠ tDst → restF m₁ r s = restF m₂ r s)
(hwkSrc : wk ≠ tSrc)
(hwkDst : wk ≠ tDst)
(hrgSrc : rg ≠ tSrc)
(hrgDst : rg ≠ tDst)
(hnameS :
∀ (a : ι),
MatchS (tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a)
(PR.passTracksAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a)) mSrc (RF.cell (xS a))))
(huniqS :
∀ (a : ι) (r : Univ A R P K dd → Prop),
MatchS (tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a)
(PR.passTracksAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a)) mSrc r) →
r = RF.cell (xS a))
(hnameD :
∀ (a : ι),
MatchD (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a)
(PR.passTracksAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ a)) (tupleIterD mSrc xS xD mD₀ a)
(RF.cell (xD a))))
(huniqD :
∀ (a : ι) (r : Univ A R P K dd → Prop),
MatchD (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a)
(PR.passTracksAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ a)) (tupleIterD mSrc xS xD mD₀ a) r) →
r = RF.cell (xD a))
(hbitFlag : ∀ (a : ι), bitFlag (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) ↔ mSrc (xS a))
(hmaxT : IsMaxLv (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ aT))
(hmaxF : ∀ a < aT, ¬IsMaxLv (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a))
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, tuple_run_iter._proof_1⟩)) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a₀)) mSrc) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ aT)),
head := Sum.inl v',
tape :=
wideTape
(PR.trackTapeAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ aT))
(tuplePost mSrc (tupleIterD mSrc xS xD mD₀) xS xD aT))
(PR.syElt PR.blank) }
The tuple loop's run at the generated families, the budget forgotten.