Soundness of the inductive-counting machine

Every accepting run of DescriptiveComplexity.InductiveCounting.CfgStep proves what it claims: no target is reachable from a source. The proof is a phase-indexed invariant, DescriptiveComplexity.InductiveCounting.Inv, preserved by every transition.

The delicate part is the inner loop, where the machine guesses which nodes belong to the current layer. A guess is certified, so the guessed set is always a subset of the layer; what rules out a guess that is too small is the count: the invariant records that the counter is at most the number of layer nodes already scanned, and that it is strictly below that number as soon as a node that would have mattered – a target, or a node putting the outer node into the next layer – has been skipped (DescriptiveComplexity.InductiveCounting.InnerInv, last clause). At the end of the scan the counter is checked against |Rset d|, which leaves no room for a skipped node.

Reading a configuration

noncomputable def DescriptiveComplexity.InductiveCounting.stage {V : Type} [LinearOrder V] (s : Cfg V) : ℕ

The layer index recorded by the stage register.

Equations

• DescriptiveComplexity.InductiveCounting.stage s = DescriptiveComplexity.orank (s.regs DescriptiveComplexity.InductiveCounting.Reg.d)

def DescriptiveComplexity.InductiveCounting.Wit {V : Type} (E : V → V → Prop) (r : WithBot V) (y : V) : Prop

A node y witnessing that the outer register's node lies in the next layer: it is that node, or has an edge to it.

Equations

• DescriptiveComplexity.InductiveCounting.Wit E r y = (↑y = r ∨ DescriptiveComplexity.InductiveCounting.EW E (↑y) r)

@[simp]

theorem DescriptiveComplexity.InductiveCounting.eW_coe_coe {V : Type} {E : V → V → Prop} {p q : V} : EW E ↑p ↑q ↔ E p q

@[simp]

theorem DescriptiveComplexity.InductiveCounting.pW_coe {V : Type} {S : V → Prop} {p : V} : PW S ↑p ↔ S p

theorem DescriptiveComplexity.InductiveCounting.mem_rset_succ_iff_wit {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} {vv : V} : vv ∈ Rset E S (d + 1) ↔ ∃ y ∈ Rset E S d, Wit E (↑vv) y

The next layer is exactly the nodes witnessed by the current one.

The invariant

def DescriptiveComplexity.InductiveCounting.InnerInv {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (s : Cfg V) (P : Set V) : Prop

The invariant of the inner loop, relative to the set P of nodes already scanned by it: the stage count is exact, the outer count is exact for the part of the next layer already scanned, and the inner count is at most – and, as soon as something was skipped that should not have been, strictly below – the number of layer nodes scanned.

Equations

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

def DescriptiveComplexity.InductiveCounting.PhaseInv {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (ph : Phase) (s : Cfg V) : Prop

The invariant, phase by phase.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.InductiveCounting.PhaseInv E S T DescriptiveComplexity.InductiveCounting.Phase.check s = DescriptiveComplexity.InductiveCounting.InnerInv E S T s Set.univ
• DescriptiveComplexity.InductiveCounting.PhaseInv E S T DescriptiveComplexity.InductiveCounting.Phase.accept s = ¬∃ (a : V) (b : V), S a ∧ T b ∧ Relation.ReflTransGen E a b

def DescriptiveComplexity.InductiveCounting.Inv {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (s : Cfg V) : Prop

The invariant of a configuration.

Equations

• DescriptiveComplexity.InductiveCounting.Inv E S T s = DescriptiveComplexity.InductiveCounting.PhaseInv E S T s.phase s

Two steps of the inner loop

theorem DescriptiveComplexity.InductiveCounting.innerInv_skip {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} {uu : V} {P : Set V} (hinv : InnerInv E S T s P) (huP : uu ∉ P) (hstage : stage s' = stage s) (hc : s'.regs Reg.c = s.regs Reg.c) (hc2 : s'.regs Reg.c2 = s.regs Reg.c2) (hv : s'.regs Reg.v = s.regs Reg.v) (hcnt : s'.regs Reg.cnt = s.regs Reg.cnt) (hflag : s'.flag = s.flag) : InnerInv E S T s' (insert uu P)

Scanning one more node without certifying it.

theorem DescriptiveComplexity.InductiveCounting.innerInv_certify {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} {uu : V} {P : Set V} (hinv : InnerInv E S T s P) (huP : uu ∉ P) (huR : uu ∈ Rset E S (stage s)) (huT : ¬T uu) (hstage : stage s' = stage s) (hc : s'.regs Reg.c = s.regs Reg.c) (hc2 : s'.regs Reg.c2 = s.regs Reg.c2) (hv : s'.regs Reg.v = s.regs Reg.v) (hcnt : s.regs Reg.cnt ⋖ s'.regs Reg.cnt) (hflag : Wit E (s.regs Reg.v) uu ∧ s'.flag = true ∨ ¬Wit E (s.regs Reg.v) uu ∧ s'.flag = s.flag) : InnerInv E S T s' (insert uu P)

Scanning one more node and certifying it: the count goes up, and the flag goes up exactly when the node witnesses the outer node.

Preservation, phase by phase

theorem DescriptiveComplexity.InductiveCounting.innerInv_congr {V : Type} [LinearOrder V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} {P : Set V} (hinv : InnerInv E S T s P) (hstage : stage s' = stage s) (hc : s'.regs Reg.c = s.regs Reg.c) (hc2 : s'.regs Reg.c2 = s.regs Reg.c2) (hv : s'.regs Reg.v = s.regs Reg.v) (hcnt : s'.regs Reg.cnt = s.regs Reg.cnt) (hflag : s'.flag = s.flag) : InnerInv E S T s' P

The inner invariant only reads the registers named here.

theorem DescriptiveComplexity.InductiveCounting.inv_step_initCount {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.initCount) (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

Counting the sources, one node at a time.

theorem DescriptiveComplexity.InductiveCounting.inv_step_inner {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.inner) (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

The inner loop: skipping a node, certifying a node, or ending the scan.

theorem DescriptiveComplexity.InductiveCounting.inv_step_walk {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.walk) (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

The certifying walk: one more edge backwards, or a source is reached.

theorem DescriptiveComplexity.InductiveCounting.inv_step_stageEnd {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.stageEnd) (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

The end of a stage: either the counts agree, and the reachable set is the current layer, or the machine moves on to the next layer.

theorem DescriptiveComplexity.InductiveCounting.check_exact {V : Type} [LinearOrder V] {E : V → V → Prop} {S T : V → Prop} {s : Cfg V} (hinv : InnerInv E S T s Set.univ) (hcnt : s.regs Reg.cnt = s.regs Reg.c) : (∀ y ∈ Rset E S (stage s), ¬T y) ∧ ∀ (vv : V), s.regs Reg.v = ↑vv → (s.flag = true ↔ vv ∈ Rset E S (stage s + 1))

At the end of the inner scan the count check leaves no room: the certified nodes are exactly the layer, so no target lies in it and the flag says exactly whether the outer node has entered the next layer.

theorem DescriptiveComplexity.InductiveCounting.inv_step_certDone {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.certDone) (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

A certified node is counted in, and tested against the outer node.

theorem DescriptiveComplexity.InductiveCounting.inv_step_check {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.check) (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

The count check: the outer count is updated and the scan restarts, or the stage is over.

theorem DescriptiveComplexity.InductiveCounting.inv_step_accept {V : Type} [LinearOrder V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hp : s.phase = Phase.accept) (_hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

Nothing leaves the accepting phase.

Soundness

theorem DescriptiveComplexity.InductiveCounting.inv_step {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hinv : Inv E S T s) (hstep : CfgStep E S T s s') : Inv E S T s'

The invariant is preserved by every transition.

theorem DescriptiveComplexity.InductiveCounting.inv_of_isSrc {V : Type} [LinearOrder V] {E : V → V → Prop} {S T : V → Prop} {s : Cfg V} (h : CfgIsSrc s) : Inv E S T s

The invariant holds at every initial configuration.

theorem DescriptiveComplexity.InductiveCounting.inv_reach {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} {s s' : Cfg V} (hinv : Inv E S T s) (h : CfgReach E S T s s') : Inv E S T s'

The invariant survives any number of transitions.

theorem DescriptiveComplexity.InductiveCounting.not_reach_of_machineAccepts {V : Type} [LinearOrder V] [Finite V] {E : V → V → Prop} {S T : V → Prop} (h : MachineAccepts E S T) : ¬∃ (a : V) (b : V), S a ∧ T b ∧ Relation.ReflTransGen E a b

Soundness: if the machine accepts, no target is reachable from a source.