The red-blue pebble game: the partition a calculation defines

Support module of MiscMath.Computability.RedBluePebbleGame, where the results are stated and where the reader should start. Nothing here is a result on its own.

This is the construction behind Hong and Kung's Theorem 3.1, corrected. A calculation charged q with at most S red pebbles is cut into q / S + 1 windows, move i lying in window charges i / S, so that each window makes at most S loads and stores. Window m contributes the part part m: the vertices given a red pebble in the window and not already in an earlier part, from which a path through such vertices leads to one that is red when the window ends or is stored during it. These parts form a 2S-partition (exists_isPartition).

The argument follows the source's, with two repairs:

• The case split in the cover argument is on red, not on any pebble. A predecessor of a vertex computed in window m is either red when the window starts, and so already in a part, or is given a red pebble during the window. An input holding its initial blue pebble need not be in any earlier part, and the source's case split puts it on the wrong side.
• The terminal condition asks for a store during the window, not for a blue pebble still there when it ends. Either works; this one is simpler to use.

It also records the facts about the graph that the argument needs: under IsComputationDAG every vertex reaches an output (IsComputationDAG.exists_output), and a calculation with no red pebbles exists only on the empty graph (IsComputationDAG.isEmpty_of_hasCompleteCalculation_zero).

Domination, set by set

theorem MiscMath.Computability.RedBluePebbleGame.dominates_iff {V : Type u_1} {E : V → V → Prop} {I D W : Finset V} : Dominates E I D W ↔ ∀ w ∈ W, Dominated E I D w

theorem MiscMath.Computability.RedBluePebbleGame.dominates_of_subset {V : Type u_1} {E : V → V → Prop} {I D W : Finset V} (h : W ⊆ D) : Dominates E I D W

The graphs of the key lemma

theorem MiscMath.Computability.RedBluePebbleGame.exists_sink_of_acyclic {V : Type u_1} {E : V → V → Prop} [Finite V] (hE : ∀ (v : V), ¬Relation.TransGen E v v) (v : V) : ∃ (w : V), Relation.ReflTransGen E v w ∧ ∀ (w' : V), ¬E w w'

In a finite graph with no cycle, every vertex reaches a vertex with no successor.

theorem MiscMath.Computability.RedBluePebbleGame.IsComputationDAG.exists_output {V : Type u_1} {E : V → V → Prop} {I : Finset V} [Finite V] {O : Finset V} (hG : IsComputationDAG E I O) (v : V) : ∃ o ∈ O, Relation.ReflTransGen E v o

Every vertex of a computation DAG reaches an output.

theorem MiscMath.Computability.RedBluePebbleGame.IsComputationDAG.not_mem_inputs {V : Type u_1} {E : V → V → Prop} {I O : Finset V} (hG : IsComputationDAG E I O) {u v : V} (h : E u v) : v ∉ I

A vertex with a predecessor is not an input.

Calculations, move by move

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_last_red {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} (h0 : v ∉ (T.σ 0).1) (τ : ℕ) : v ∈ (T.σ τ).1 → ∃ i < τ, v ∉ (T.σ i).1 ∧ ∀ (j : ℕ), i < j → j ≤ τ → v ∈ (T.σ j).1

The last time before τ a vertex red at τ was given its red pebble: it has stayed red since.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_last_blue {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} (h0 : v ∉ (T.σ 0).2) (τ : ℕ) : v ∈ (T.σ τ).2 → ∃ i < τ, v ∉ (T.σ i).2 ∧ ∀ (j : ℕ), i < j → j ≤ τ → v ∈ (T.σ j).2

The last time before τ a vertex blue at τ was given its blue pebble: it has stayed blue since.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_compute_between {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {a : ℕ} (hR : v ∉ (T.σ a).1) (hB : v ∉ (T.σ a).2) (b : ℕ) : a ≤ b → b ≤ T.t → v ∈ (T.σ b).1 ∨ v ∈ (T.σ b).2 → ∃ (i : ℕ), a ≤ i ∧ i < b ∧ v ∉ (T.σ i).1 ∧ ∀ (u : V), E u v → u ∈ (T.σ i).1

A vertex with no pebble at time a and a pebble at time b was computed in between: at some move i ∈ [a, b) it was not red and all its predecessors were.

def MiscMath.Computability.RedBluePebbleGame.Trace.newBlues {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (j e : ℕ) : Finset V

The vertices given a blue pebble by moves j, …, e - 1: those it stores.

Equations

• T.newBlues j e = (Finset.Ico j e).biUnion fun (i : ℕ) => (T.σ (i + 1)).2 \ (T.σ i).2

theorem MiscMath.Computability.RedBluePebbleGame.Trace.card_newBlues_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {j e : ℕ} (he : e ≤ T.t) : (T.newBlues j e).card ≤ ∑ i ∈ Finset.Ico j e, T.c i

Windows

def MiscMath.Computability.RedBluePebbleGame.Trace.win {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (i : ℕ) : ℕ

The window of move i: the number of complete blocks of S loads and stores before it.

Equations

• T.win i = T.charges i / S

theorem MiscMath.Computability.RedBluePebbleGame.Trace.win_mono {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) : Monotone T.win

def MiscMath.Computability.RedBluePebbleGame.Trace.cut {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (m : ℕ) : ℕ

The time at which window m starts: the first time that is the end of the calculation or lies in window m or a later one.

Equations

• T.cut m = Nat.find ⋯

theorem MiscMath.Computability.RedBluePebbleGame.Trace.cut_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (m : ℕ) : T.cut m ≤ T.t

theorem MiscMath.Computability.RedBluePebbleGame.Trace.cut_spec {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (m : ℕ) : T.cut m = T.t ∨ m ≤ T.win (T.cut m)

theorem MiscMath.Computability.RedBluePebbleGame.Trace.lt_cut_iff {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {i m : ℕ} (hi : i < T.t) : i < T.cut m ↔ T.win i < m

A move before the end lies before the start of window m exactly when its window is earlier.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.cut_zero {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) : T.cut 0 = 0

theorem MiscMath.Computability.RedBluePebbleGame.Trace.cut_mono {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) : Monotone T.cut

theorem MiscMath.Computability.RedBluePebbleGame.Trace.cut_win_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {i : ℕ} (hi : i < T.t) : T.cut (T.win i) ≤ i

Move i lies in the window win i, between its start and the next window's.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.lt_cut_win_succ {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {i : ℕ} (hi : i < T.t) : i < T.cut (T.win i + 1)

theorem MiscMath.Computability.RedBluePebbleGame.Trace.cut_last {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) : T.cut (T.charges T.t / S + 1) = T.t

Every move lies in one of the first charges t / S + 1 windows.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.sum_window_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (hS : 1 ≤ S) (m : ℕ) : ∑ i ∈ Finset.Ico (T.cut m) (T.cut (m + 1)), T.c i ≤ S

A window makes at most S loads and stores.

The parts

def MiscMath.Computability.RedBluePebbleGame.Trace.terminal {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (m : ℕ) : Finset V

The vertices a window m must account for when it ends: those red then, and those it stored.

Equations

• T.terminal m = (T.σ (T.cut (m + 1))).1 ∪ T.newBlues (T.cut m) (T.cut (m + 1))

def MiscMath.Computability.RedBluePebbleGame.Trace.cand {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (U : Finset V) (m : ℕ) : Finset V

The candidates of window m, given the vertices U already placed in earlier parts: those given a red pebble in the window and not in U.

Equations

• T.cand U m = T.newReds (T.cut m) (T.cut (m + 1)) \ U

noncomputable def MiscMath.Computability.RedBluePebbleGame.Trace.partOf {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (U : Finset V) (m : ℕ) : Finset V

The part of window m, given the vertices U already placed: the candidates from which a path through candidates leads to a terminal vertex.

Equations

• T.partOf U m = {v ∈ T.cand U m | ∃ w ∈ T.terminal m, Relation.ReflTransGen (fun (a b : V) => E a b ∧ a ∈ T.cand U m ∧ b ∈ T.cand U m) v w}

noncomputable def MiscMath.Computability.RedBluePebbleGame.Trace.assigned {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) : ℕ → Finset V

The vertices placed in the parts of windows 0, …, m - 1.

Equations

• T.assigned 0 = ∅
• T.assigned m.succ = T.assigned m ∪ T.partOf (T.assigned m) m

noncomputable def MiscMath.Computability.RedBluePebbleGame.Trace.part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (m : ℕ) : Finset V

The part of window m.

Equations

• T.part m = T.partOf (T.assigned m) m

theorem MiscMath.Computability.RedBluePebbleGame.Trace.assigned_succ {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (m : ℕ) : T.assigned (m + 1) = T.assigned m ∪ T.part m

theorem MiscMath.Computability.RedBluePebbleGame.Trace.assigned_mono {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) : Monotone T.assigned

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_assigned_iff {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} : v ∈ T.assigned m ↔ ∃ m' < m, v ∈ T.part m'

theorem MiscMath.Computability.RedBluePebbleGame.Trace.part_subset_assigned {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {m m' : ℕ} (h : m < m') : T.part m ⊆ T.assigned m'

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_part_iff {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} : v ∈ T.part m ↔ v ∈ T.cand (T.assigned m) m ∧ ∃ w ∈ T.terminal m, Relation.ReflTransGen (fun (a b : V) => E a b ∧ a ∈ T.cand (T.assigned m) m ∧ b ∈ T.cand (T.assigned m) m) v w

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_cand_of_mem_part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} (hv : v ∈ T.part m) : v ∈ T.cand (T.assigned m) m

theorem MiscMath.Computability.RedBluePebbleGame.Trace.not_mem_assigned_of_mem_part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} (hv : v ∈ T.part m) : v ∉ T.assigned m

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_newReds_of_mem_part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} (hv : v ∈ T.part m) : v ∈ T.newReds (T.cut m) (T.cut (m + 1))

theorem MiscMath.Computability.RedBluePebbleGame.Trace.disjoint_part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {m m' : ℕ} (h : m ≠ m') : Disjoint (T.part m) (T.part m')

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_part_of_terminal {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} (hc : v ∈ T.cand (T.assigned m) m) (ht : v ∈ T.terminal m) : v ∈ T.part m

A terminal candidate is in the part.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_part_of_edge {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {u v : V} {m : ℕ} (hu : u ∈ T.cand (T.assigned m) m) (huv : E u v) (hv : v ∈ T.part m) : u ∈ T.part m

A candidate with a successor in the part is in the part.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_terminal_of_mem_part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} {m : ℕ} (hv : v ∈ T.part m) (hmin : ∀ w ∈ T.part m, ¬E v w) : v ∈ T.terminal m

A vertex of the part with no successor in it is terminal.

The key claims

theorem MiscMath.Computability.RedBluePebbleGame.Trace.not_mem_red_zero {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (h0 : T.σ 0 = (∅, I)) (v : V) : v ∉ (T.σ 0).1

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_assigned_of_red {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (h0 : T.σ 0 = (∅, I)) {v : V} {m : ℕ} (hv : v ∈ (T.σ (T.cut (m + 1))).1) : v ∈ T.assigned (m + 1)

A vertex red when a window ends is in its part or an earlier one.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_assigned_of_stored {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (h0 : T.σ 0 = (∅, I)) {v : V} {m : ℕ} (hv : v ∈ T.newBlues (T.cut m) (T.cut (m + 1))) : v ∈ T.assigned (m + 1)

A vertex stored in a window is in its part or an earlier one.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.not_pebbled_of_mem_part {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (h0 : T.σ 0 = (∅, I)) {v : V} {m : ℕ} (hv : v ∈ T.part m) (hvI : v ∉ I) : v ∉ (T.σ (T.cut m)).1 ∧ v ∉ (T.σ (T.cut m)).2

A non-input in a part has no pebble when its window starts.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_assigned_of_pred {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (h0 : T.σ 0 = (∅, I)) {u v : V} {m : ℕ} (hv : v ∈ T.part m) (hvI : v ∉ I) (huv : E u v) : u ∈ T.assigned (m + 1)

A predecessor of a non-input in a part is in that part or an earlier one.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.mem_assigned_last {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {O : Finset V} (h0 : T.σ 0 = (∅, I)) [Finite V] (hG : IsComputationDAG E I O) (ht : T.σ T.t = (∅, O)) (v : V) : v ∈ T.assigned (T.charges T.t / S + 1)

Every vertex is in one of the first charges t / S + 1 parts.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.card_windowDom_part_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (hS : 1 ≤ S) (m : ℕ) : (T.windowDom (T.cut m) (T.cut (m + 1))).card ≤ 2 * S

The dominator of a part: the red pebbles when its window starts, and the vertices it loads.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.card_terminal_le {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (hS : 1 ≤ S) (m : ℕ) : (T.terminal m).card ≤ 2 * S

theorem MiscMath.Computability.RedBluePebbleGame.Trace.isPartition {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {O : Finset V} (h0 : T.σ 0 = (∅, I)) [Finite V] (hS : 1 ≤ S) (hG : IsComputationDAG E I O) (ht : T.σ T.t = (∅, O)) : IsPartition E I (2 * S) fun (i : Fin (T.charges T.t / S + 1)) => T.part ↑i

The parts form a 2S-partition.

theorem MiscMath.Computability.RedBluePebbleGame.Step.nonempty {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {s s' : Finset V × Finset V} {c : ℕ} (h : Step E I s c s') : Nonempty V

Every move is made on some vertex.

theorem MiscMath.Computability.RedBluePebbleGame.HasCompleteCalculation.eq_zero_of_isEmpty {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} [IsEmpty V] {O : Finset V} {S q : ℕ} (h : HasCompleteCalculation E I O S q) : q = 0

So on the empty type no move can be made, and a complete calculation costs nothing.

theorem MiscMath.Computability.RedBluePebbleGame.IsComputationDAG.isEmpty_of_hasCompleteCalculation_zero {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} [Finite V] {O : Finset V} {q : ℕ} (hG : IsComputationDAG E I O) (h : HasCompleteCalculation E I O 0 q) : IsEmpty V

With no red pebbles nothing can be loaded, computed or stored, so a complete calculation exists only on the empty graph.

theorem MiscMath.Computability.RedBluePebbleGame.exists_isPartition {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} [Finite V] {O : Finset V} {S q : ℕ} (hG : IsComputationDAG E I O) (hq : HasCompleteCalculation E I O S q) : ∃ (h : ℕ) (P : Fin h → Finset V), IsPartition E I (2 * S) P ∧ q ≤ S * h ∧ S * h ≤ q + S

Hong and Kung's Theorem 3.1, corrected. A complete calculation of a computation DAG with at most S red pebbles, charged q, comes with a 2S-partition into h parts, q ≤ S h ≤ q + S.