Completeness of the inductive-counting machine #
If no target is reachable from a source, the machine has an accepting run: the honest one, which certifies every node of every layer. The proof builds that run, four nested loops at a time – the certifying walk, the inner scan, the outer scan, and the sequence of stages – each by an induction along the finite linear order of nodes or, for the stages, on how much room the layer still has to grow.
Walking a finite linear order downwards #
theorem
DescriptiveComplexity.InductiveCounting.order_induction_down
{A : Type}
[LinearOrder A]
[Finite A]
{P : A → Prop}
(hmax : ∀ (z : A), (∀ (a : A), a ≤ z) → P z)
(hstep : ∀ (w z : A), w ⋖ z → P z → P w)
(z : A)
:
P z
Induction from the greatest element downwards, one cover at a time.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.exists_covBy_of_orank_pos
{V : Type}
[LinearOrder V]
[Finite V]
{r : WithBot V}
(h : 0 < orank r)
:
A nonzero counter has a predecessor.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.exists_isMin
(V : Type)
[LinearOrder V]
[Finite V]
[Nonempty V]
:
∃ (x : V), ∀ (z : V), x ≤ z
A finite nonempty linear order has a least element.
Dependency graph
Configurations, explicitly #
def
DescriptiveComplexity.InductiveCounting.mkCfg
{V : Type}
(ph : Phase)
(fl : Bool)
(rd rc rc2 rv rcnt ru rw rj : WithBot V)
:
Cfg V
A configuration with its eight registers given one by one.
Equations
Instances For
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
@[simp]
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.stage_mkCfg
{V : Type}
{ph : Phase}
{fl : Bool}
{rd rc rc2 rv rcnt ru rw rj : WithBot V}
[LinearOrder V]
:
Dependency graph
The transitions, one lemma each #
theorem
DescriptiveComplexity.InductiveCounting.step_init_src
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc' rc2 rv rv' rcnt ru rw rj : WithBot V}
(hsrc : PW S rv)
(hc : rc ⋖ rc')
(hv : rv ⋖ rv')
:
CfgStep E S T (mkCfg Phase.initCount fl rd rc rc2 rv rcnt ru rw rj)
(mkCfg Phase.initCount fl rd rc' rc2 rv' rcnt ru rw rj)
Counting a source and moving on.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_init_nsrc
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rv' rcnt ru rw rj : WithBot V}
(hsrc : ¬PW S rv)
(hv : rv ⋖ rv')
:
CfgStep E S T (mkCfg Phase.initCount fl rd rc rc2 rv rcnt ru rw rj)
(mkCfg Phase.initCount fl rd rc rc2 rv' rcnt ru rw rj)
Skipping a non-source and moving on.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_init_last_src
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc' rc2 rv rv' rcnt ru ru' rw rw' rj rj' : WithBot V}
(hsrc : PW S rv)
(hc : rc ⋖ rc')
(htop : PW (fun (p : V) => ∀ (z : V), z ≤ p) rv)
(hv' : PW (fun (p : V) => ∀ (z : V), p ≤ z) rv')
(hu' : PW (fun (p : V) => ∀ (z : V), p ≤ z) ru')
:
CfgStep E S T (mkCfg Phase.initCount fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner false ⊥ rc' ⊥ rv' ⊥ ru' rw' rj')
The last node of the source scan is a source: the first stage begins.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_init_last_nsrc
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rv' rcnt ru ru' rw rw' rj rj' : WithBot V}
(hsrc : ¬PW S rv)
(htop : PW (fun (p : V) => ∀ (z : V), z ≤ p) rv)
(hv' : PW (fun (p : V) => ∀ (z : V), p ≤ z) rv')
(hu' : PW (fun (p : V) => ∀ (z : V), p ≤ z) ru')
:
CfgStep E S T (mkCfg Phase.initCount fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner false ⊥ rc ⊥ rv' ⊥ ru' rw' rj')
The last node of the source scan is not a source: the first stage begins.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_skip
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt ru ru' rw rw' rj rj' : WithBot V}
(hu : ru ⋖ ru')
:
CfgStep E S T (mkCfg Phase.inner fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner fl rd rc rc2 rv rcnt ru' rw' rj')
Skipping a node of the inner scan.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_skip_last
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt ru ru' rw rw' rj rj' : WithBot V}
(hu : PW (fun (p : V) => ∀ (z : V), z ≤ p) ru)
:
CfgStep E S T (mkCfg Phase.inner fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.check fl rd rc rc2 rv rcnt ru' rw' rj')
Skipping the last node of the inner scan.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_certify
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt ru rw rj : WithBot V}
(hu : ¬PW T ru)
:
CfgStep E S T (mkCfg Phase.inner fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.walk fl rd rc rc2 rv rcnt ru ru rd)
Starting to certify the current node of the inner scan.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_walk
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt ru rw rw' rj rj' : WithBot V}
(hj : rj' ⋖ rj)
(hw : EW E rw' rw)
:
CfgStep E S T (mkCfg Phase.walk fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.walk fl rd rc rc2 rv rcnt ru rw' rj')
One edge backwards along the certifying path.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_walk_done
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt ru rw rj : WithBot V}
(hw : PW S rw)
:
CfgStep E S T (mkCfg Phase.walk fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj)
The certifying path has reached a source.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_count_eq
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt rcnt' ru ru' rw rj : WithBot V}
(heq : ru = rv)
(hcnt : rcnt ⋖ rcnt')
(hu : ru ⋖ ru')
:
CfgStep E S T (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner true rd rc rc2 rv rcnt' ru' rw rj)
Counting in a certified node equal to the outer one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_count_edge
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt rcnt' ru ru' rw rj : WithBot V}
(hedge : EW E ru rv)
(hcnt : rcnt ⋖ rcnt')
(hu : ru ⋖ ru')
:
CfgStep E S T (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner true rd rc rc2 rv rcnt' ru' rw rj)
Counting in a certified node with an edge to the outer one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_count_none
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt rcnt' ru ru' rw rj : WithBot V}
(hne : ru ≠ rv)
(hnedge : ¬EW E ru rv)
(hcnt : rcnt ⋖ rcnt')
(hu : ru ⋖ ru')
:
CfgStep E S T (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner fl rd rc rc2 rv rcnt' ru' rw rj)
Counting in a certified node unrelated to the outer one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_count_last_eq
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt rcnt' ru ru' rw rj : WithBot V}
(heq : ru = rv)
(hcnt : rcnt ⋖ rcnt')
(hu : PW (fun (p : V) => ∀ (z : V), z ≤ p) ru)
:
CfgStep E S T (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.check true rd rc rc2 rv rcnt' ru' rw rj)
Counting in the last certified node, equal to the outer one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_count_last_edge
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt rcnt' ru ru' rw rj : WithBot V}
(hedge : EW E ru rv)
(hcnt : rcnt ⋖ rcnt')
(hu : PW (fun (p : V) => ∀ (z : V), z ≤ p) ru)
:
CfgStep E S T (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.check true rd rc rc2 rv rcnt' ru' rw rj)
Counting in the last certified node, with an edge to the outer one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_count_last_none
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt rcnt' ru ru' rw rj : WithBot V}
(hne : ru ≠ rv)
(hnedge : ¬EW E ru rv)
(hcnt : rcnt ⋖ rcnt')
(hu : PW (fun (p : V) => ∀ (z : V), z ≤ p) ru)
:
CfgStep E S T (mkCfg Phase.certDone fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.check fl rd rc rc2 rv rcnt' ru' rw rj)
Counting in the last certified node, unrelated to the outer one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_check_true
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{rd rc rc2 rc2' rv rv' rcnt ru ru' rw rw' rj rj' : WithBot V}
(hc2 : rc2 ⋖ rc2')
(hcnt : rcnt = rc)
(hv : rv ⋖ rv')
(hu' : PW (fun (p : V) => ∀ (z : V), p ≤ z) ru')
:
CfgStep E S T (mkCfg Phase.check true rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner false rd rc rc2' rv' ⊥ ru' rw' rj')
The count checks out and the outer node was in the next layer.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_check_false
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{rd rc rc2 rv rv' rcnt ru ru' rw rw' rj rj' : WithBot V}
(hcnt : rcnt = rc)
(hv : rv ⋖ rv')
(hu' : PW (fun (p : V) => ∀ (z : V), p ≤ z) ru')
:
CfgStep E S T (mkCfg Phase.check false rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner false rd rc rc2 rv' ⊥ ru' rw' rj')
The count checks out and the outer node was not in the next layer.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_check_last_true
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{rd rc rc2 rc2' rv rv' rcnt rcnt' ru ru' rw rw' rj rj' : WithBot V}
(hc2 : rc2 ⋖ rc2')
(hcnt : rcnt = rc)
(hv : PW (fun (p : V) => ∀ (z : V), z ≤ p) rv)
:
CfgStep E S T (mkCfg Phase.check true rd rc rc2 rv rcnt ru rw rj)
(mkCfg Phase.stageEnd false rd rc rc2' rv' rcnt' ru' rw' rj')
The last outer node was in the next layer: the stage ends.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_check_last_false
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{rd rc rc2 rv rv' rcnt rcnt' ru ru' rw rw' rj rj' : WithBot V}
(hcnt : rcnt = rc)
(hv : PW (fun (p : V) => ∀ (z : V), z ≤ p) rv)
:
CfgStep E S T (mkCfg Phase.check false rd rc rc2 rv rcnt ru rw rj)
(mkCfg Phase.stageEnd false rd rc rc2 rv' rcnt' ru' rw' rj')
The last outer node was not in the next layer: the stage ends.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_accept
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl fl' : Bool}
{rd rd' rc rc' rc2 rc2' rv rv' rcnt rcnt' ru ru' rw rw' rj rj' : WithBot V}
(hc2 : rc2 = rc)
:
CfgStep E S T (mkCfg Phase.stageEnd fl rd rc rc2 rv rcnt ru rw rj)
(mkCfg Phase.accept fl' rd' rc' rc2' rv' rcnt' ru' rw' rj')
The two counts agree: the machine accepts.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.step_nextStage
{V : Type}
[LinearOrder V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rd' rc rc2 rv rv' rcnt ru ru' rw rw' rj rj' : WithBot V}
(hd : rd ⋖ rd')
(hv' : PW (fun (p : V) => ∀ (z : V), p ≤ z) rv')
(hu' : PW (fun (p : V) => ∀ (z : V), p ≤ z) ru')
:
CfgStep E S T (mkCfg Phase.stageEnd fl rd rc rc2 rv rcnt ru rw rj) (mkCfg Phase.inner false rd' rc2 ⊥ rv' ⊥ ru' rw' rj')
On to the next stage.
Dependency graph
The certifying walk #
theorem
DescriptiveComplexity.InductiveCounting.reach_certDone
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
{fl : Bool}
{rd rc rc2 rv rcnt : WithBot V}
{uu : V}
(n : ℕ)
(ww : V)
(rj : WithBot V)
:
A node of the current layer can be certified: the machine walks backwards along a witnessing path until it meets a source.
Dependency graph
The inner scan #
theorem
DescriptiveComplexity.InductiveCounting.exists_wit_insert
{V : Type}
{E : V → V → Prop}
{S : V → Prop}
{D : ℕ}
{rv : WithBot V}
{x : V}
{P : Set V}
(hnw : ¬Wit E rv x ∨ x ∉ Rset E S D)
:
Rewriting the witnesses of the outer node when the scan passes a node that is not one.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.reach_check
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
{rd rc rc2 : WithBot V}
{vv : V}
(hnoT : ∀ y ∈ Rset E S (orank rd), ¬T y)
(x : V)
(rcnt rw rj : WithBot V)
(fl : Bool)
:
orank rcnt = (Rset E S (orank rd) ∩ predSet ↑x).ncard →
(fl = true ↔ ∃ y ∈ Rset E S (orank rd) ∩ predSet ↑x, Wit E (↑vv) y) →
∃ (rcnt' : WithBot V) (rw' : WithBot V) (rj' : WithBot V) (ru' : WithBot V) (fl' : Bool),
CfgReach E S T (mkCfg Phase.inner fl rd rc rc2 (↑vv) rcnt (↑x) rw rj)
(mkCfg Phase.check fl' rd rc rc2 (↑vv) rcnt' ru' rw' rj') ∧ orank rcnt' = (Rset E S (orank rd)).ncard ∧ (fl' = true ↔ vv ∈ Rset E S (orank rd + 1))
The inner scan: from any node on, with an honest count and an honest flag, the machine reaches the count check with the exact count of the current layer and with the flag telling whether the outer node has entered the next layer.
Dependency graph
The outer scan, the source count, and the stages #
theorem
DescriptiveComplexity.InductiveCounting.reach_stageEnd
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
[Nonempty V]
{rd rc : WithBot V}
(hnoT : ∀ y ∈ Rset E S (orank rd), ¬T y)
(hc : orank rc = (Rset E S (orank rd)).ncard)
(x : V)
(rc2 rw rj : WithBot V)
(u0 : V)
:
(∀ (z : V), u0 ≤ z) →
orank rc2 = (Rset E S (orank rd + 1) ∩ predSet ↑x).ncard →
∃ (rc2' : WithBot V) (rv' : WithBot V) (rcnt' : WithBot V) (ru' : WithBot V) (rw' : WithBot V) (rj' : WithBot V),
CfgReach E S T (mkCfg Phase.inner false rd rc rc2 ↑x ⊥ (↑u0) rw rj)
(mkCfg Phase.stageEnd false rd rc rc2' rv' rcnt' ru' rw' rj') ∧ orank rc2' = (Rset E S (orank rd + 1)).ncard
The outer scan: with the layer count in hand, the machine runs over every node and reaches the end of the stage with the exact count of the next layer.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.reach_firstStage
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
[Nonempty V]
(x : V)
(fl : Bool)
(rd rc rc2 rcnt ru rw rj : WithBot V)
:
orank rc = ({y : V | S y} ∩ predSet ↑x).ncard →
∃ (rc' : WithBot V) (rw' : WithBot V) (rj' : WithBot V) (v0 : V) (u0 : V),
(∀ (z : V), v0 ≤ z) ∧ (∀ (z : V), u0 ≤ z) ∧ CfgReach E S T (mkCfg Phase.initCount fl rd rc rc2 (↑x) rcnt ru rw rj)
(mkCfg Phase.inner false ⊥ rc' ⊥ ↑v0 ⊥ (↑u0) rw' rj') ∧ orank rc' = (Rset E S 0).ncard
The source scan: the machine counts the sources and enters the first stage.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.reach_accept
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
[Nonempty V]
(hno : ¬∃ (a : V) (b : V), S a ∧ T b ∧ Relation.ReflTransGen E a b)
(m : ℕ)
(rd rc : WithBot V)
(v0 u0 : V)
(rw rj : WithBot V)
:
(∀ (z : V), v0 ≤ z) →
(∀ (z : V), u0 ≤ z) →
orank rc = (Rset E S (orank rd)).ncard →
orank rd + (Rset E S 0).ncard ≤ (Rset E S (orank rd)).ncard →
Nat.card V - (Rset E S (orank rd)).ncard ≤ m →
∃ (s' : Cfg V),
s'.phase = Phase.accept ∧ CfgReach E S T (mkCfg Phase.inner false rd rc ⊥ ↑v0 ⊥ (↑u0) rw rj) s'
The stages: as long as the layer keeps growing the machine starts a new stage; when it stops growing the two counts agree and the machine accepts.
Dependency graph
Completeness #
theorem
DescriptiveComplexity.InductiveCounting.machineAccepts_of_not_reach
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
[Nonempty V]
(hno : ¬∃ (a : V) (b : V), S a ∧ T b ∧ Relation.ReflTransGen E a b)
:
MachineAccepts E S T
Completeness: if no target is reachable from a source, the machine has an accepting run.
Dependency graph
theorem
DescriptiveComplexity.InductiveCounting.machineAccepts_iff
{V : Type}
[LinearOrder V]
[Finite V]
{E : V → V → Prop}
{S T : V → Prop}
[Nonempty V]
:
The machine is correct: it accepts exactly when no target is reachable from a source.