The red-blue pebble game: calculations as sequences indexed by ℕ

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.

HasCompleteCalculation indexes configurations by Fin (t + 1) and charges by Fin t, which is the right shape for reading and the wrong one for proving. This file supplies:

• step_iff, the five moves as a disjunction, and the facts about a single move that the proofs use: a move adds at most one red pebble and at most one blue pebble, never one of each, and the first pebble a non-input receives comes from a computation;
• Trace, a calculation with configurations and charges indexed by ℕ, and the passage to it from HasCompleteCalculation;
• Run, a calculation assembled move by move, which is how calculations are built, and the passage from it back to HasCompleteCalculation;
• the count behind the trivial I/O bound: every input loaded and every output stored at least once costs at least |I| + |O|.

A single move

theorem MiscMath.Computability.RedBluePebbleGame.step_iff {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {s s' : Finset V × Finset V} {c : ℕ} : Step E I s c s' ↔ (∃ v ∈ s.2, v ∉ s.1 ∧ c = 1 ∧ s' = (insert v s.1, s.2)) ∨ (∃ v ∈ s.1, v ∉ s.2 ∧ c = 1 ∧ s' = (s.1, insert v s.2)) ∨ (∃ v ∉ I, v ∉ s.1 ∧ (∀ (u : V), E u v → u ∈ s.1) ∧ c = 0 ∧ s' = (insert v s.1, s.2)) ∨ (∃ v ∈ s.1, c = 0 ∧ s' = (s.1.erase v, s.2)) ∨ ∃ v ∈ s.2, c = 0 ∧ s' = (s.1, s.2.erase v)

The five moves of Step, as a disjunction over the configuration's components.

@[instance_reducible]

instance MiscMath.Computability.RedBluePebbleGame.Step.decidable {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} [Fintype V] [DecidableRel E] {s s' : Finset V × Finset V} {c : ℕ} : Decidable (Step E I s c s')

Whether a move is legal can be decided on a finite graph, which lets concrete calculations be checked by decide.

Equations

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

theorem MiscMath.Computability.RedBluePebbleGame.Step.charge_le_one {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') : c ≤ 1

theorem MiscMath.Computability.RedBluePebbleGame.Step.new_red {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') {v : V} (h₁ : v ∉ s.1) (h₂ : v ∈ s'.1) : s' = (insert v s.1, s.2) ∧ (c = 1 ∧ v ∈ s.2 ∨ c = 0 ∧ v ∉ I ∧ ∀ (u : V), E u v → u ∈ s.1)

A red pebble that appears in a move comes from a load, charged 1, or from a computation, charged 0; either way the move adds exactly that red pebble.

theorem MiscMath.Computability.RedBluePebbleGame.Step.new_blue {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') {v : V} (h₁ : v ∉ s.2) (h₂ : v ∈ s'.2) : s' = (s.1, insert v s.2) ∧ c = 1 ∧ v ∈ s.1

A blue pebble that appears in a move comes from a store, charged 1.

theorem MiscMath.Computability.RedBluePebbleGame.Step.eq_of_new_red {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') {v w : V} (hv₁ : v ∉ s.1) (hv₂ : v ∈ s'.1) (hw₁ : w ∉ s.1) (hw₂ : w ∈ s'.1) : v = w

A move adds at most one red pebble.

theorem MiscMath.Computability.RedBluePebbleGame.Step.eq_of_new_blue {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') {v w : V} (hv₁ : v ∉ s.2) (hv₂ : v ∈ s'.2) (hw₁ : w ∉ s.2) (hw₂ : w ∈ s'.2) : v = w

A move adds at most one blue pebble.

theorem MiscMath.Computability.RedBluePebbleGame.Step.not_new_red_and_blue {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') {v w : V} (hv₁ : v ∉ s.1) (hv₂ : v ∈ s'.1) (hw₁ : w ∉ s.2) (hw₂ : w ∈ s'.2) : False

No move adds both a red pebble and a blue one.

theorem MiscMath.Computability.RedBluePebbleGame.Step.card_sdiff_red_le_one {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') : (s'.1 \ s.1).card ≤ 1

The red pebbles a move adds: at most one.

theorem MiscMath.Computability.RedBluePebbleGame.Step.first_pebble {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') {v : V} (h₁ : v ∉ s.1) (h₂ : v ∉ s.2) (h₃ : v ∈ s'.1 ∨ v ∈ s'.2) : v ∉ I ∧ (∀ (u : V), E u v → u ∈ s.1) ∧ s'.1 = insert v s.1 ∧ c = 0

The first pebble a vertex receives, red or blue, comes from computing it.

Calculations indexed by ℕ

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

A calculation within a red-pebble budget S, with configurations σ j (j ≤ t) and charges c i (i < t) indexed by ℕ. Charges past the end are 0, so that partial sums of charges stop growing at t.

• t : ℕ

  The number of moves.

• σ : ℕ → Finset V × Finset V

  The configurations; only σ 0, …, σ t matter.

• c : ℕ → ℕ

  The charges; only c 0, …, c (t - 1) matter, and the rest are 0.

• budget (j : ℕ) : j ≤ self.t → (self.σ j).1.card ≤ S
• step (i : ℕ) : i < self.t → Step E I (self.σ i) (self.c i) (self.σ (i + 1))
• c_eq_zero (i : ℕ) : self.t ≤ i → self.c i = 0

theorem MiscMath.Computability.RedBluePebbleGame.HasCompleteCalculation.exists_trace {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I O : Finset V} {S q : ℕ} (h : HasCompleteCalculation E I O S q) : ∃ (T : Trace E I S), T.σ 0 = (∅, I) ∧ T.σ T.t = (∅, O) ∧ ∑ i ∈ Finset.range T.t, T.c i = q

Every complete calculation, read as a Trace.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.c_le_one {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) (i : ℕ) : T.c i ≤ 1

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_new_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) (j : ℕ) : v ∈ (T.σ j).1 → ∃ i < j, v ∉ (T.σ i).1 ∧ v ∈ (T.σ (i + 1)).1

If a vertex holds a red pebble at time j but not at time 0, some move before j gave it one.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_new_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) (j : ℕ) : v ∈ (T.σ j).2 → ∃ i < j, v ∉ (T.σ i).2 ∧ v ∈ (T.σ (i + 1)).2

If a vertex holds a blue pebble at time j but not at time 0, some move before j gave it one.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.exists_compute {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (T : Trace E I S) {v : V} (hv : v ∉ I) (h0 : T.σ 0 = (∅, I)) (j : ℕ) : j ≤ T.t → v ∈ (T.σ j).1 ∨ v ∈ (T.σ j).2 → ∃ i < j, v ∉ (T.σ i).1 ∧ (∀ (u : V), E u v → u ∈ (T.σ i).1) ∧ (T.σ (i + 1)).1 = insert v (T.σ i).1

A non-input that holds a pebble at time j ≤ t, in a calculation that starts from the inputs alone, was computed by some move before j: at that move all its predecessors were red and it was not.

theorem MiscMath.Computability.RedBluePebbleGame.Trace.card_add_card_le {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)) (ht : (T.σ T.t).2 = O) (hIO : Disjoint I O) (hred : ∀ x ∈ I, ∃ j ≤ T.t, x ∈ (T.σ j).1) : I.card + O.card ≤ ∑ i ∈ Finset.range T.t, T.c i

The trivial I/O bound. If every input is red at some point and every output ends blue, the inputs and outputs being disjoint, the calculation is charged at least |I| + |O|: each input is loaded, each output stored, and no move does two of these.

Calculations built move by move

inductive MiscMath.Computability.RedBluePebbleGame.Run {V : Type u_1} [DecidableEq V] (E : V → V → Prop) (I : Finset V) (S : ℕ) : Finset V × Finset V → ℕ → Finset V × Finset V → Prop

Run E I S s q s': a sequence of moves from s to s', charged q in total, in which every configuration after the first has at most S red pebbles.

• refl {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (s : Finset V × Finset V) : Run E I S s 0 s
• cons {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {s s' s'' : Finset V × Finset V} {c q : ℕ} : Step E I s c s' → s'.1.card ≤ S → Run E I S s' q s'' → Run E I S s (c + q) s''

theorem MiscMath.Computability.RedBluePebbleGame.Run.trans {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {s s' s'' : Finset V × Finset V} {q q' : ℕ} (h : Run E I S s q s') (h' : Run E I S s' q' s'') : Run E I S s (q + q') s''

theorem MiscMath.Computability.RedBluePebbleGame.Run.cast {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {s s' t t' : Finset V × Finset V} {q q' : ℕ} (h : Run E I S s q s') (hs : s = t) (hq : q = q') (hs' : s' = t') : Run E I S t q' t'

theorem MiscMath.Computability.RedBluePebbleGame.Run.single {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {s s' : Finset V × Finset V} {c : ℕ} (h : Step E I s c s') (hb : s'.1.card ≤ S) : Run E I S s c s'

One move, as a run.

theorem MiscMath.Computability.RedBluePebbleGame.Run.exists_seq {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {s s' : Finset V × Finset V} {q : ℕ} (h : Run E I S s q s') (hs : s.1.card ≤ S) : ∃ (t : ℕ) (σ : Fin (t + 1) → Finset V × Finset V) (c : Fin t → ℕ), σ 0 = s ∧ σ (Fin.last t) = s' ∧ (∀ (j : Fin (t + 1)), (σ j).1.card ≤ S) ∧ (∀ (i : Fin t), Step E I (σ i.castSucc) (c i) (σ i.succ)) ∧ ∑ i : Fin t, c i = q

A run, read as the data of HasCompleteCalculation.

theorem MiscMath.Computability.RedBluePebbleGame.Run.hasCompleteCalculation {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} {O : Finset V} {q : ℕ} (h : Run E I S (∅, I) q (∅, O)) : HasCompleteCalculation E I O S q

A run from the inputs alone to the outputs alone is a complete calculation.