Registers as counters and as loop positions

The registers of DescriptiveComplexity.InductiveCounting.Cfg hold values in WithBot V, read in two ways: as a count, through DescriptiveComplexity.orank (so ⊥ is 0 and each cover adds one), and as a loop position, through DescriptiveComplexity.InductiveCounting.predSet (the set of nodes already scanned). This file collects the arithmetic of the two readings: how a cover moves a loop past one more node, how the count of a set restricted to the scanned part grows, and when a counter still has room to be incremented.

instance DescriptiveComplexity.InductiveCounting.instFiniteWithBot {V : Type} [Finite V] : Finite (WithBot V)

Covers in a finite linear order

theorem DescriptiveComplexity.InductiveCounting.exists_covBy_of_not_max {A : Type} [LinearOrder A] [Finite A] {z : A} (hz : ¬∀ (a : A), a ≤ z) : ∃ (w : A), z ⋖ w

In a finite linear order, an element that is not a maximum is covered by some element.

Counts

@[simp]

theorem DescriptiveComplexity.InductiveCounting.orank_bot {V : Type} [LinearOrder V] : orank ⊥ = 0

theorem DescriptiveComplexity.InductiveCounting.orank_lt_orank {A : Type} [LinearOrder A] [Finite A] {a b : A} (h : a < b) : orank a < orank b

The rank is strictly monotone.

theorem DescriptiveComplexity.InductiveCounting.orank_inj {A : Type} [LinearOrder A] [Finite A] {a b : A} (h : orank a = orank b) : a = b

The rank determines the element.

theorem DescriptiveComplexity.InductiveCounting.exists_covBy_of_orank_lt {V : Type} [LinearOrder V] [Finite V] {r : WithBot V} (h : orank r < Nat.card V) : ∃ (r' : WithBot V), r ⋖ r'

A counter whose value is still below the number of nodes can be incremented.

Loop positions

def DescriptiveComplexity.InductiveCounting.predSet {V : Type} [LinearOrder V] (r : WithBot V) : Set V

The set of nodes strictly below the value of a register: the nodes a loop holding that value has already scanned.

Equations

• DescriptiveComplexity.InductiveCounting.predSet r = {y : V | ↑y < r}

@[simp]

theorem DescriptiveComplexity.InductiveCounting.predSet_bot {V : Type} [LinearOrder V] : predSet ⊥ = ∅

theorem DescriptiveComplexity.InductiveCounting.predSet_coe {V : Type} [LinearOrder V] (x : V) : predSet ↑x = {y : V | y < x}

theorem DescriptiveComplexity.InductiveCounting.mem_predSet_coe {V : Type} [LinearOrder V] {x y : V} : y ∈ predSet ↑x ↔ y < x

theorem DescriptiveComplexity.InductiveCounting.notMem_predSet_self {V : Type} [LinearOrder V] (x : V) : x ∉ predSet ↑x

theorem DescriptiveComplexity.InductiveCounting.predSet_of_isMin {V : Type} [LinearOrder V] {x : V} (h : ∀ (z : V), x ≤ z) : predSet ↑x = ∅

At the least node, nothing has been scanned.

theorem DescriptiveComplexity.InductiveCounting.insert_predSet_of_isMax {V : Type} [LinearOrder V] {x : V} (h : ∀ (z : V), z ≤ x) : insert x (predSet ↑x) = Set.univ

Past the greatest node, everything has been scanned.

theorem DescriptiveComplexity.InductiveCounting.predSet_of_covBy {V : Type} [LinearOrder V] {x : V} {r : WithBot V} (h : ↑x ⋖ r) : predSet r = insert x (predSet ↑x)

A cover of a register value holding a node advances the scan past exactly that node.

theorem DescriptiveComplexity.InductiveCounting.exists_coe_of_covBy {V : Type} [LinearOrder V] {x : V} {r : WithBot V} (h : ↑x ⋖ r) : ∃ (x' : V), r = ↑x' ∧ x ⋖ x'

A cover of a register value holding a node holds a node again.

theorem DescriptiveComplexity.InductiveCounting.isMin_of_bot_covBy {V : Type} [LinearOrder V] {r : WithBot V} (h : ⊥ ⋖ r) : ∃ (x : V), r = ↑x ∧ ∀ (z : V), x ≤ z

The value covering ⊥ is the least node.

Counting the scanned part of a set

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_predSet_le {V : Type} [LinearOrder V] [Finite V] {P : Set V} (r : WithBot V) : (P ∩ predSet r).ncard ≤ P.ncard

theorem DescriptiveComplexity.InductiveCounting.ncard_le_card {V : Type} [Finite V] (P : Set V) : P.ncard ≤ Nat.card V

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_insert_of_mem {V : Type} [Finite V] {Q P : Set V} {uu : V} (huP : uu ∉ P) (h : uu ∈ Q) : (Q ∩ insert uu P).ncard = (Q ∩ P).ncard + 1

Scanning one more node, of the set: its scanned count goes up by one.

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_insert_of_notMem {V : Type} {Q P : Set V} {uu : V} (h : uu ∉ Q) : (Q ∩ insert uu P).ncard = (Q ∩ P).ncard

Scanning one more node, outside the set: its scanned count is unchanged.

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_insert_le {V : Type} [Finite V] {Q P : Set V} {uu : V} : (Q ∩ P).ncard ≤ (Q ∩ insert uu P).ncard

Scanning one more node can only grow the scanned part of a set.

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_predSet_covBy_of_mem {V : Type} [LinearOrder V] [Finite V] {P : Set V} {x : V} {r : WithBot V} (h : ↑x ⋖ r) (hx : x ∈ P) : (P ∩ predSet r).ncard = (P ∩ predSet ↑x).ncard + 1

Scanning past a node of the set increases its scanned count by one.

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_predSet_covBy_of_notMem {V : Type} [LinearOrder V] {P : Set V} {x : V} {r : WithBot V} (h : ↑x ⋖ r) (hx : x ∉ P) : (P ∩ predSet r).ncard = (P ∩ predSet ↑x).ncard

Scanning past a node outside the set leaves its scanned count alone.

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_predSet_isMax_of_mem {V : Type} [LinearOrder V] [Finite V] {P : Set V} {x : V} (h : ∀ (z : V), z ≤ x) (hx : x ∈ P) : (P ∩ predSet ↑x).ncard + 1 = P.ncard

At the greatest node, the scanned count of the set is one short of its total, if the node belongs to it.

theorem DescriptiveComplexity.InductiveCounting.ncard_inter_predSet_isMax_of_notMem {V : Type} [LinearOrder V] {P : Set V} {x : V} (h : ∀ (z : V), z ≤ x) (hx : x ∉ P) : (P ∩ predSet ↑x).ncard = P.ncard

At the greatest node, the scanned count of the set is its total, if the node lies outside it.