Counting on a block of heads

A deterministic machine cannot guess a tuple: it has to walk the tuples one at a time. This file gives it the odometer.

DescriptiveComplexity.HeadProgram.lexNextP replaces the tuple held on a block of heads by its lexicographic successor, and exits false when there is none – when the tuple is the greatest. It is the same chain a schoolchild uses to add one: walk the positions from the last, and at the first position that is not at its greatest value, step that head and reset the ones after it.

The one thing a machine cannot do directly is ask whether a head is at the greatest element: that is not a quantifier-free fact of one head. So the block comes with a marker head parked at the greatest element, and the test is the atom "these two heads are equal" – the same device the quantifier sweep of DescriptiveComplexity.HeadEval uses, here shared by every position of the block.

Accordingly the relation DescriptiveComplexity.HeadProgram.lexRel that the gadget runs is stated in terms of the marker's value, not of maximality: it is an honest description of what the machine does whatever the marker holds. Where the marker is known to be at the greatest element, DescriptiveComplexity.HeadProgram.tupSucc_of_lexRel turns it into DescriptiveComplexity.TupSucc, the coordinatewise description of covering in Lex (Fin n → A), and the walk becomes a walk along a finite linear order like any other.

The control graph of an increment

inductive DescriptiveComplexity.HeadProgram.LexNode (n : ℕ) : Type

The control nodes of a lexicographic increment on a block of n heads: test j has found the positions from j on to be at the marker and is about to look at position j - 1; bump j steps position j and resets the rest.

• test {n : ℕ} (j : Fin (n + 1)) : LexNode n

  Positions from j on are at the marker; about to test position j - 1.

• bump {n : ℕ} (j : Fin n) : LexNode n

  Step position j, and reset the positions after it.

instance DescriptiveComplexity.HeadProgram.instFiniteLexNode {n : ℕ} : Finite (LexNode n)

def DescriptiveComplexity.HeadProgram.testPos {n : ℕ} (j : Fin (n + 1)) : Option (Fin n)

The position a test node is about to look at, if it has not run out.

Equations

• DescriptiveComplexity.HeadProgram.testPos j = if h : 0 < ↑j then some ⟨↑j - 1, ⋯⟩ else none

def DescriptiveComplexity.HeadProgram.testDown {n : ℕ} (j : Fin (n + 1)) : Fin (n + 1)

The test node that follows, one position down.

Equations

• DescriptiveComplexity.HeadProgram.testDown j = ⟨↑j - 1, ⋯⟩

theorem DescriptiveComplexity.HeadProgram.testPos_eq_none {n : ℕ} {j : Fin (n + 1)} (h : ↑j = 0) : testPos j = none

theorem DescriptiveComplexity.HeadProgram.testPos_eq_some {n : ℕ} {j : Fin (n + 1)} {p : ℕ} (h : ↑j = p + 1) (hp : p < n) : testPos j = some ⟨p, hp⟩

theorem DescriptiveComplexity.HeadProgram.testDown_val {n : ℕ} {j : Fin (n + 1)} {p : ℕ} (h : ↑j = p + 1) : ↑(testDown j) = p

def DescriptiveComplexity.HeadProgram.lexWire {n : ℕ} : LexNode n → Bool → LexNode n ⊕ Bool

The wiring of an increment: at the marker, look one position down; away from it, step that position.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.lexWire (DescriptiveComplexity.HeadProgram.LexNode.bump j) x✝ = Sum.inr true

noncomputable def DescriptiveComplexity.HeadProgram.bumpMoves {K n : ℕ} (blk : Fin n → Fin K) (j : Fin n) : Fin K → HeadMove K

The moves of an increment: step position j of the block and send the positions after it to the least element.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.lexFam {L : FirstOrder.Language} {K n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) : LexNode n → HeadProgram L K

The fragments of an increment.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.lexFam blk mk (DescriptiveComplexity.HeadProgram.LexNode.bump j) = DescriptiveComplexity.HeadProgram.moveP (DescriptiveComplexity.HeadProgram.bumpMoves blk j)

noncomputable def DescriptiveComplexity.HeadProgram.lexNextP {L : FirstOrder.Language} {K n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) : HeadProgram L K

The odometer: replace the tuple on the block by its lexicographic successor, exiting false when every position is at the marker.

Equations

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

def DescriptiveComplexity.HeadProgram.lexRel {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) : (Fin K → A) → Bool → (Fin K → A) → Prop

What an increment runs, stated by the marker's value rather than by maximality: either some position is away from the marker – the last such one is stepped and the positions after it are reset – or all of them are at it and the increment fails.

Equations

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

def DescriptiveComplexity.HeadProgram.lexFamRel {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) : LexNode n → (Fin K → A) → Bool → (Fin K → A) → Prop

The relations the fragments of an increment run.

Equations

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

What the increment runs

theorem DescriptiveComplexity.HeadProgram.runs_lexFam {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) (hblk : ∀ (i : Fin n), ↑(blk i) < prot) (c : LexNode n) : (lexFam blk mk c).Runs A prot (lexFamRel blk mk prot c)

theorem DescriptiveComplexity.HeadProgram.headLocal2_lexFamRel {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) (hblk : ∀ (i : Fin n), ↑(blk i) < prot) (hmk : ↑mk < prot) (c : LexNode n) : HeadLocal2 prot (lexFamRel blk mk prot c)

theorem DescriptiveComplexity.HeadProgram.lexRel_local {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) (hblk : ∀ (i : Fin n), ↑(blk i) < prot) (hmk : ↑mk < prot) : HeadLocal2 prot (lexRel blk mk prot)

The walk of an increment

def DescriptiveComplexity.HeadProgram.lexRelFrom {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot jj : ℕ) : (Fin K → A) → Bool → (Fin K → A) → Prop

What the increment runs once the positions from jj on are known to be at the marker: the stepped position is one of those left.

Equations

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

theorem DescriptiveComplexity.HeadProgram.lexRelFrom_all {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) {x : Fin K → A} {b : Bool} {y : Fin K → A} : lexRelFrom blk mk prot n x b y ↔ lexRel blk mk prot x b y

theorem DescriptiveComplexity.HeadProgram.lexRelFrom_mono {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) {jj jj' : ℕ} (h : jj ≤ jj') {x : Fin K → A} {b : Bool} {y : Fin K → A} (hr : lexRelFrom blk mk prot jj x b y) : lexRelFrom blk mk prot jj' x b y

theorem DescriptiveComplexity.HeadProgram.lexRelFrom_local {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot : ℕ) (hblk : ∀ (i : Fin n), ↑(blk i) < prot) (hmk : ↑mk < prot) (jj : ℕ) : HeadLocal2 prot (lexRelFrom blk mk prot jj)

def DescriptiveComplexity.HeadProgram.LexExit {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} (blk : Fin n → Fin K) (mk : Fin K) (prot jj : ℕ) (hjj : jj < n + 1) (x : Fin K → A) (b : Bool) (y : Fin K → A) : Prop

Abbreviation for the walk of an increment.

Equations

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

theorem DescriptiveComplexity.HeadProgram.lexSound {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} (hinj : Function.Injective blk) (hblk : ∀ (i : Fin n), ↑(blk i) < prot) (hmk : ↑mk < prot) (jj : ℕ) (hjj : jj < n + 1) (x : Fin K → A) : (∀ (i : Fin n), jj ≤ ↑i → x (blk i) = x mk) → ∀ (b : Bool) (y : Fin K → A), LexExit blk mk prot jj hjj x b y → lexRelFrom blk mk prot jj x b y

Soundness of the increment: every exit is the one the relation describes.

noncomputable def DescriptiveComplexity.HeadProgram.bumpTuple {K : ℕ} {A : Type} {n : ℕ} (blk : Fin n → Fin K) (p : Fin n) (x y : Fin K → A) : Fin K → A

The tuple an increment produces at position p: the stepped and reset positions taken from the outcome, everything else left where it was.

Equations

• DescriptiveComplexity.HeadProgram.bumpTuple blk p x y h = if h = blk p then y (blk p) else if ∃ (i : Fin n), p < i ∧ h = blk i then y h else x h

theorem DescriptiveComplexity.HeadProgram.bumpTuple_at {K : ℕ} {A : Type} {n : ℕ} (blk : Fin n → Fin K) (p : Fin n) (x y : Fin K → A) : bumpTuple blk p x y (blk p) = y (blk p)

theorem DescriptiveComplexity.HeadProgram.bumpTuple_after {K : ℕ} {A : Type} {n : ℕ} (blk : Fin n → Fin K) {p i : Fin n} (hi : p < i) (x y : Fin K → A) (hinj : Function.Injective blk) : bumpTuple blk p x y (blk i) = y (blk i)

theorem DescriptiveComplexity.HeadProgram.bumpTuple_before {K : ℕ} {A : Type} {n : ℕ} (blk : Fin n → Fin K) {p i : Fin n} (hi : i < p) (x y : Fin K → A) (hinj : Function.Injective blk) : bumpTuple blk p x y (blk i) = x (blk i)

theorem DescriptiveComplexity.HeadProgram.bumpTuple_out {K : ℕ} {A : Type} {n : ℕ} (blk : Fin n → Fin K) (p : Fin n) (x y : Fin K → A) {h : Fin K} (hh : ∀ (i : Fin n), h ≠ blk i) : bumpTuple blk p x y h = x h

theorem DescriptiveComplexity.HeadProgram.lexComplete {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} (hinj : Function.Injective blk) (_hblk : ∀ (i : Fin n), ↑(blk i) < prot) (_hmk : ↑mk < prot) (jj : ℕ) (hjj : jj < n + 1) (x : Fin K → A) : (∀ (i : Fin n), jj ≤ ↑i → x (blk i) = x mk) → ∀ (b : Bool) (y : Fin K → A), lexRelFrom blk mk prot jj x b y → ∃ (y' : Fin K → A), HeadAgree prot y y' ∧ LexExit blk mk prot jj hjj x b y'

Completeness of the increment: the outcome the relation describes is reached.

The odometer

theorem DescriptiveComplexity.HeadProgram.runs_lexNextP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} (hinj : Function.Injective blk) (hblk : ∀ (i : Fin n), ↑(blk i) < prot) (hmk : ↑mk < prot) : (lexNextP blk mk).Runs A prot (lexRel blk mk prot)

What the odometer runs: the lexicographic successor of the tuple on the block, read through the marker.

theorem DescriptiveComplexity.HeadProgram.deterministic_lexNextP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} : (lexNextP blk mk).Deterministic A

Reading the increment as a lexicographic step

theorem DescriptiveComplexity.HeadProgram.tupSucc_of_lexRel {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} {x y : Fin K → A} (hmax : ∀ (a : A), a ≤ x mk) (h : lexRel blk mk prot x true y) : TupSucc (fun (i : Fin n) => x (blk i)) fun (i : Fin n) => y (blk i)

Where the marker holds the greatest element, a successful increment is the lexicographic successor.

theorem DescriptiveComplexity.HeadProgram.isTop_of_lexRel {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} {x y : Fin K → A} (hmax : ∀ (a : A), a ≤ x mk) (h : lexRel blk mk prot x false y) (i : Fin n) (a : A) : a ≤ x (blk i)

Where the marker holds the greatest element, a failed increment says the tuple was the greatest.

theorem DescriptiveComplexity.HeadProgram.exists_lexRel_succ {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} {x : Fin K → A} [Finite A] (hinj : Function.Injective blk) (hmax : ∀ (a : A), a ≤ x mk) (hnotTop : ¬∀ (i : Fin n) (a : A), a ≤ x (blk i)) : ∃ (y : Fin K → A), lexRel blk mk prot x true y ∧ (TupSucc (fun (i : Fin n) => x (blk i)) fun (i : Fin n) => y (blk i)) ∧ ∀ (j : Fin K), ↑j < prot → (∀ (i : Fin n), j ≠ blk i) → y j = x j

The increment can always be taken where the tuple is not the greatest: the outcome the relation describes exists.

theorem DescriptiveComplexity.HeadProgram.lexRel_top {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} {x : Fin K → A} (hmax : ∀ (a : A), a ≤ x mk) (hall : ∀ (i : Fin n) (a : A), a ≤ x (blk i)) : lexRel blk mk prot x false x

The increment fails exactly at the greatest tuple, and then leaves everything alone.

theorem DescriptiveComplexity.HeadProgram.agree_of_lexRel {K : ℕ} {A : Type} [LinearOrder A] {n : ℕ} {blk : Fin n → Fin K} {mk : Fin K} {prot : ℕ} {x y : Fin K → A} (h : lexRel blk mk prot x false y) : HeadAgree prot x y

A failed increment leaves the heads where they were.