The depth-first search of Krivelevich and Sudakov (EPI-3)

Krivelevich and Sudakov (The phase transition in random graphs: a simple proof, Random Structures & Algorithms 43 (2013), arXiv:1201.6529, Section 2) explore a graph by depth-first search, maintaining three sets: S (exploration complete), U (a stack) and T (unvisited). While U is non-empty, the algorithm queries the pairs between the last vertex v of U and the vertices of T; a positive answer for {v, u} moves u from T to U, and if no pair is left, v moves to S. If U is empty, a vertex of T is pushed into U, starting a new epoch (one per connected component). Once U = T = ∅, the remaining pairs are queried (the paper's completion phase), so that every pair is queried exactly once.

The search is fed with answers: ofAnswers V l is the state reached with the answers l (in order), stopped just before the next query pending. On the edge coins ω, the answers are queryAnswers (nextQuery e₀) ω t; the search then explores perc ⊤ ω (mem_found_iff_of_queryAnswers), and by the principle of deferred decisions the answers are i.i.d. Bernoulli(p) (fresh_nextQuery with prob_queryAnswers).

The paper scans T along a fixed order σ; any deterministic choice works, and we use pick.

Structure of the proofs: State.Inv is an invariant preserved by every move (Inv.move) and answer (Inv.answer); settle reaches a state where a query is due (move_settle), because the potential 2 |S| + |U| ≤ 2 |V| increases with every effective move; a settle starts at most one epoch (epochs_settle_le). The extra field pushes counts the vertices pushed by positive answers.

The properties of the search used in the paper:

• each query is a new pair (fresh_nextQuery, card_queried_ofAnswers);
• all pairs between S and T have been queried and answered negatively (queried_of_mem_done_of_mem_unvisited);
• U spans a path (stack_chain_ofAnswers);
• |U| ≤ 1 + ∑ Xᵢ and, while T ≠ ∅, |S ∪ U| ≥ ∑ Xᵢ (length_stack_le, count_true_le_card);
• the vertices found during one epoch lie in one connected component (reachable_of_mem_comp).

noncomputable def Epidemics.DFS.pick {α : Type u_2} {s : Finset α} (h : s.Nonempty) : α

An element of a nonempty finite set: the deterministic choice that replaces the paper's order σ.

Equations

• Epidemics.DFS.pick h = Classical.choose h

theorem Epidemics.DFS.pick_mem {α : Type u_2} {s : Finset α} (h : s.Nonempty) : pick h ∈ s

structure Epidemics.DFS.State (V : Type u_2) : Type u_2

A state of the depth-first search (Krivelevich–Sudakov, Section 2).

• done : Finset V

  S: the vertices whose exploration is complete.

• stack : List V

  U: the stack, last added vertex first.

• queried : Finset (Sym2 V)

  The pairs queried so far.

• found : Finset (Sym2 V)

  The pairs whose query was answered positively.

• epochs : ℕ

  The number of epochs started so far.

• comp : Finset V

  The vertices discovered in the current epoch.

• pushes : ℕ

  The number of vertices pushed by a positive answer.

def Epidemics.DFS.State.init {V : Type u_1} : State V

The initial state: S = U = ∅, T = V.

Equations

• Epidemics.DFS.State.init = { done := ∅, stack := [], queried := ∅, found := ∅, epochs := 0, comp := ∅, pushes := 0 }

def Epidemics.DFS.State.unvisited {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : Finset V

T: the unvisited vertices.

Equations

• s.unvisited = Finset.univ \ (s.done ∪ s.stack.toFinset)

def Epidemics.DFS.State.candidates {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) (v : V) : Finset V

The unvisited vertices u such that the pair {v, u} has not been queried yet.

Equations

• s.candidates v = {u ∈ s.unvisited | s(v, u) ∉ s.queried}

def Epidemics.DFS.State.unqueried {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : Finset (Sym2 V)

The pairs of distinct vertices not queried yet.

Equations

• s.unqueried = {e : Sym2 V | ¬e.IsDiag ∧ e ∉ s.queried}

def Epidemics.DFS.State.Finished {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : Prop

The exploration is over: U = T = ∅ (only the completion phase is left).

Equations

• s.Finished = (s.stack = [] ∧ s.unvisited = ∅)

noncomputable def Epidemics.DFS.State.pending {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : Option (Sym2 V)

The pair queried next, if any: {v, u} for the last vertex v of U and a candidate u; once U = T = ∅, an unqueried pair (completion phase). none if a move without query is due or every pair has been queried.

Equations

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

noncomputable def Epidemics.DFS.State.move {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : State V

A move without query: the last vertex of U moves to S if it has no candidate left; if U is empty, a vertex of T is pushed, starting a new epoch. Otherwise the state is unchanged.

Equations

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

noncomputable def Epidemics.DFS.State.answer {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) (b : Bool) : State V

Record the answer b to the pending query; a positive answer for {v, u} (with v the last vertex of U) pushes u.

Equations

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

noncomputable def Epidemics.DFS.State.settle {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : State V

Perform the moves without query until a query is due (2 |V| moves always suffice, as 2 |S| + |U| ≤ 2 |V| increases with each effective move).

Equations

• s.settle = Epidemics.DFS.State.move^[2 * Fintype.card V] s

def Epidemics.DFS.State.potential {V : Type u_1} (s : State V) : ℕ

The potential 2 |S| + |U|, increased by every effective move.

Equations

• s.potential = 2 * s.done.card + s.stack.length

@[simp]

theorem Epidemics.DFS.State.mem_unvisited {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {x : V} : x ∈ s.unvisited ↔ x ∉ s.done ∧ x ∉ s.stack

theorem Epidemics.DFS.State.mem_candidates {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v u : V} : u ∈ s.candidates v ↔ u ∈ s.unvisited ∧ s(v, u) ∉ s.queried

theorem Epidemics.DFS.State.mem_unqueried {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {e : Sym2 V} : e ∈ s.unqueried ↔ ¬e.IsDiag ∧ e ∉ s.queried

The cases of move, answer and pending

theorem Epidemics.DFS.State.move_cons_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hs : s.stack = v :: rest) (h : (s.candidates v).Nonempty) : s.move = s

theorem Epidemics.DFS.State.move_cons_neg {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hs : s.stack = v :: rest) (h : ¬(s.candidates v).Nonempty) : s.move = { done := insert v s.done, stack := rest, queried := s.queried, found := s.found, epochs := s.epochs, comp := s.comp, pushes := s.pushes }

theorem Epidemics.DFS.State.move_nil_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (h : s.unvisited.Nonempty) : s.move = { done := s.done, stack := [pick h], queried := s.queried, found := s.found, epochs := s.epochs + 1, comp := {pick h}, pushes := s.pushes }

theorem Epidemics.DFS.State.move_nil_neg {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (h : ¬s.unvisited.Nonempty) : s.move = s

theorem Epidemics.DFS.State.answer_cons_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hs : s.stack = v :: rest) (h : (s.candidates v).Nonempty) (b : Bool) : s.answer b = { done := s.done, stack := if b = true then pick h :: s.stack else s.stack, queried := insert s(v, pick h) s.queried, found := if b = true then insert s(v, pick h) s.found else s.found, epochs := s.epochs, comp := if b = true then insert (pick h) s.comp else s.comp, pushes := if b = true then s.pushes + 1 else s.pushes }

theorem Epidemics.DFS.State.answer_cons_neg {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hs : s.stack = v :: rest) (h : ¬(s.candidates v).Nonempty) (b : Bool) : s.answer b = s

theorem Epidemics.DFS.State.answer_nil_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (h : s.unvisited.Nonempty) (b : Bool) : s.answer b = s

theorem Epidemics.DFS.State.answer_nil_pad {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (hT : ¬s.unvisited.Nonempty) (h : s.unqueried.Nonempty) (b : Bool) : s.answer b = { done := s.done, stack := s.stack, queried := insert (pick h) s.queried, found := if b = true then insert (pick h) s.found else s.found, epochs := s.epochs, comp := s.comp, pushes := s.pushes }

theorem Epidemics.DFS.State.answer_nil_none {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (hT : ¬s.unvisited.Nonempty) (h : ¬s.unqueried.Nonempty) (b : Bool) : s.answer b = s

theorem Epidemics.DFS.State.pending_cons_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hs : s.stack = v :: rest) (h : (s.candidates v).Nonempty) : s.pending = some s(v, pick h)

theorem Epidemics.DFS.State.pending_cons_neg {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hs : s.stack = v :: rest) (h : ¬(s.candidates v).Nonempty) : s.pending = none

theorem Epidemics.DFS.State.pending_nil_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (h : s.unvisited.Nonempty) : s.pending = none

theorem Epidemics.DFS.State.pending_nil_pad {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (hT : ¬s.unvisited.Nonempty) (h : s.unqueried.Nonempty) : s.pending = some (pick h)

theorem Epidemics.DFS.State.pending_nil_none {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.stack = []) (hT : ¬s.unvisited.Nonempty) (h : ¬s.unqueried.Nonempty) : s.pending = none

The invariant

structure Epidemics.DFS.State.Inv {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : Prop

The invariant of the search (Krivelevich–Sudakov, Section 2, and the bookkeeping of epochs).

• disj : Disjoint s.done s.stack.toFinset
• nodup : s.stack.Nodup
• chain : List.IsChain (fun (u v : V) => s(u, v) ∈ s.found) s.stack
• done_unvisited (a : V) : a ∈ s.done → ∀ b ∈ s.unvisited, s(a, b) ∈ s.queried
• found_unvisited (e : Sym2 V) : e ∈ s.found → ∀ x ∈ e, x ∉ s.unvisited
• found_queried : s.found ⊆ s.queried
• not_diag (e : Sym2 V) : e ∈ s.queried → ¬e.IsDiag
• queried_unvisited (e : Sym2 V) : e ∈ s.queried → ∃ x ∈ e, x ∉ s.unvisited
• comp_sub : s.comp ⊆ s.done ∪ s.stack.toFinset
• stack_comp (v : V) : v ∈ s.stack → v ∈ s.comp
• comp_conn (u : V) : u ∈ s.comp → ∀ v ∈ s.comp, (SimpleGraph.fromEdgeSet ↑s.found).Reachable u v
• base (a : V) : a ∈ (s.done ∪ s.stack.toFinset) \ s.comp → ∀ c ∉ (s.done ∪ s.stack.toFinset) \ s.comp, s(a, c) ∈ s.queried
• card_eq : (s.done ∪ s.stack.toFinset).card = s.pushes + s.epochs
• card_comp : s.comp.card ≤ s.pushes + 1
• pushes_le : s.pushes ≤ s.found.card
• pushes_eq : ¬s.Finished → s.found.card = s.pushes

theorem Epidemics.DFS.State.inv_init {V : Type u_1} [Fintype V] [DecidableEq V] : init.Inv

theorem Epidemics.DFS.State.reachable_mono {V : Type u_1} {F F' : Finset (Sym2 V)} (h : F ⊆ F') {u v : V} (huv : (SimpleGraph.fromEdgeSet ↑F).Reachable u v) : (SimpleGraph.fromEdgeSet ↑F').Reachable u v

theorem Epidemics.DFS.State.Inv.move_nil_pos {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (hst : s.stack = []) (hT : s.unvisited.Nonempty) : { done := s.done, stack := [pick hT], queried := s.queried, found := s.found, epochs := s.epochs + 1, comp := {pick hT}, pushes := s.pushes }.Inv

Root push.

theorem Epidemics.DFS.State.not_finished_of_cons {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} {v : V} {rest : List V} (hst : s.stack = v :: rest) : ¬s.Finished

theorem Epidemics.DFS.State.Inv.move_cons_neg {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) {v : V} {rest : List V} (hst : s.stack = v :: rest) (hc : ¬(s.candidates v).Nonempty) : { done := insert v s.done, stack := rest, queried := s.queried, found := s.found, epochs := s.epochs, comp := s.comp, pushes := s.pushes }.Inv

Pop: the last vertex of U moves to S.

theorem Epidemics.DFS.State.Inv.answer_cons_false {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) {v : V} {rest : List V} (hst : s.stack = v :: rest) (hc : (s.candidates v).Nonempty) : { done := s.done, stack := s.stack, queried := insert s(v, pick hc) s.queried, found := s.found, epochs := s.epochs, comp := s.comp, pushes := s.pushes }.Inv

A negative answer to a query of the search.

theorem Epidemics.DFS.State.Inv.answer_cons_true {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) {v : V} {rest : List V} (hst : s.stack = v :: rest) (hc : (s.candidates v).Nonempty) : { done := s.done, stack := pick hc :: s.stack, queried := insert s(v, pick hc) s.queried, found := insert s(v, pick hc) s.found, epochs := s.epochs, comp := insert (pick hc) s.comp, pushes := s.pushes + 1 }.Inv

A positive answer to a query of the search: u is pushed.

theorem Epidemics.DFS.State.Inv.answer_pad {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (hst : s.stack = []) (hT : ¬s.unvisited.Nonempty) (hq : s.unqueried.Nonempty) (b : Bool) : { done := s.done, stack := s.stack, queried := insert (pick hq) s.queried, found := if b = true then insert (pick hq) s.found else s.found, epochs := s.epochs, comp := s.comp, pushes := s.pushes }.Inv

A query of the completion phase.

theorem Epidemics.DFS.State.Inv.move {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) : s.move.Inv

theorem Epidemics.DFS.State.Inv.answer {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (b : Bool) : (s.answer b).Inv

theorem Epidemics.DFS.State.Inv.iterate_move {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (k : ℕ) : (State.move^[k] s).Inv

theorem Epidemics.DFS.State.Inv.settle {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) : s.settle.Inv

Frame lemmas

theorem Epidemics.DFS.State.move_frame {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} : s.move.queried = s.queried ∧ s.move.found = s.found ∧ s.move.pushes = s.pushes

theorem Epidemics.DFS.State.iterate_move_frame {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (k : ℕ) : (move^[k] s).queried = s.queried ∧ (move^[k] s).found = s.found ∧ (move^[k] s).pushes = s.pushes

theorem Epidemics.DFS.State.settle_queried {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} : s.settle.queried = s.queried

theorem Epidemics.DFS.State.settle_found {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} : s.settle.found = s.found

theorem Epidemics.DFS.State.settle_pushes {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} : s.settle.pushes = s.pushes

theorem Epidemics.DFS.State.move_epochs_comp {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} : s.move.epochs = s.epochs ∧ s.move.comp = s.comp ∨ s.move.epochs = s.epochs + 1 ∧ ∃ (x : V), s.move.comp = {x}

A move either keeps the epoch (and its vertices) or starts a new one with a single vertex.

theorem Epidemics.DFS.State.answer_epochs {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (b : Bool) : (s.answer b).epochs = s.epochs

theorem Epidemics.DFS.State.pending_answer {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (b : Bool) : s.pending = none ∧ s.answer b = s ∨ ∃ (e : Sym2 V), s.pending = some e ∧ e ∉ s.queried ∧ (s.answer b).queried = insert e s.queried ∧ (s.answer b).found = if b = true then insert e s.found else s.found

The answer to the pending query, if any, adds that pair to the queried ones (and to the found ones if positive); without pending query, the answer changes nothing.

Monotonicity

structure Epidemics.DFS.State.Le {V : Type u_1} [Fintype V] [DecidableEq V] (s t : State V) : Prop

t extends s: more pairs queried and found, S and S ∪ U larger (so T smaller), more epochs and pushes.

• queried : s.queried ⊆ t.queried
• found : s.found ⊆ t.found
• done : s.done ⊆ t.done
• unvisited : t.unvisited ⊆ s.unvisited
• epochs : s.epochs ≤ t.epochs
• pushes : s.pushes ≤ t.pushes

theorem Epidemics.DFS.State.Le.refl {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : s.Le s

theorem Epidemics.DFS.State.Le.trans {V : Type u_1} [Fintype V] [DecidableEq V] {s t u : State V} (h₁ : s.Le t) (h₂ : t.Le u) : s.Le u

theorem Epidemics.DFS.State.le_move {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : s.Le s.move

theorem Epidemics.DFS.State.le_answer {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) (b : Bool) : s.Le (s.answer b)

theorem Epidemics.DFS.State.le_iterate_move {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) (k : ℕ) : s.Le (move^[k] s)

theorem Epidemics.DFS.State.le_settle {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : s.Le s.settle

Termination of settle

theorem Epidemics.DFS.State.potential_move {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) : s.move = s ∨ s.move.potential = s.potential + 1

theorem Epidemics.DFS.State.potential_le {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) : s.potential ≤ 2 * Fintype.card V

theorem Epidemics.DFS.State.move_settle {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) : s.settle.move = s.settle

After settle, no move without query is due.

theorem Epidemics.DFS.State.exists_cons_of_move_eq {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hfix : s.move = s) (hnf : ¬s.Finished) : ∃ (v : V) (rest : List V), s.stack = v :: rest ∧ (s.candidates v).Nonempty

A state where no move is due is either at a query of the search or finished.

theorem Epidemics.DFS.State.move_of_finished {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (h : s.Finished) : s.move = s

theorem Epidemics.DFS.State.settle_of_finished {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (h : s.Finished) : s.settle = s

theorem Epidemics.DFS.State.answer_finished {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (h : s.Finished) (b : Bool) : (s.answer b).Finished

Epochs within one settle

theorem Epidemics.DFS.State.move_of_not_root {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (h : ¬(s.stack = [] ∧ s.unvisited.Nonempty)) : s.move.epochs = s.epochs ∧ s.move.comp = s.comp

theorem Epidemics.DFS.State.epochs_iterate_after_root {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (hst : s.stack = []) (hT : s.unvisited.Nonempty) (m : ℕ) : (move^[m] s.move).epochs = s.move.epochs

After a new epoch starts, settle starts no other one: either the new root has a candidate (pairs inside T are never queried), or it was the last unvisited vertex.

theorem Epidemics.DFS.State.epochs_settle_le {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) : s.settle.epochs ≤ s.epochs + 1

settle starts at most one epoch.

theorem Epidemics.DFS.State.comp_settle_of_epochs_eq {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (h : s.settle.epochs = s.epochs) : s.settle.comp = s.comp

If settle starts no epoch, the current epoch keeps its vertices.

theorem Epidemics.DFS.State.comp_settle_of_lt {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (h : s.epochs < s.settle.epochs) : ∃ (x : V), s.settle.comp = {x}

If settle starts an epoch, the current epoch has a single vertex.

theorem Epidemics.DFS.State.answer_pushes_le {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (b : Bool) : (s.answer b).pushes ≤ s.pushes + 1

theorem Epidemics.DFS.State.answer_of_not_finished {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (hfix : s.move = s) (hnf : ¬s.Finished) (b : Bool) : ((s.answer b).pushes = s.pushes + if b = true then 1 else 0) ∧ ((s.answer b).comp.card = s.comp.card + if b = true then 1 else 0) ∧ ¬(s.answer b).Finished

A query of the search proper (not of the completion phase): a positive answer pushes a new vertex, which joins the current epoch.

theorem Epidemics.DFS.State.exists_pending {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hs : s.Inv) (hfix : s.move = s) (hq : s.queried.card < (Fintype.card V).choose 2) : ∃ (e : Sym2 V), s.pending = some e

Where a query is due, the pending pair exists as long as some pair is unqueried.

noncomputable def Epidemics.DFS.ofAnswers (V : Type u_2) [Fintype V] [DecidableEq V] (l : List Bool) : State V

The search fed with the answers l, in order, stopped just before its next query.

Equations

• Epidemics.DFS.ofAnswers V l = List.foldl (fun (s : Epidemics.DFS.State V) (b : Bool) => (s.answer b).settle) Epidemics.DFS.State.init.settle l

noncomputable def Epidemics.DFS.nextQuery {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) (l : List Bool) : Sym2 V

The search as an adaptive strategy on the edge coins: after the answers l, query the pending pair of ofAnswers V l (or e₀ once every pair has been queried).

Equations

• Epidemics.DFS.nextQuery e₀ l = (Epidemics.DFS.ofAnswers V l).pending.getD e₀

theorem Epidemics.DFS.ofAnswers_nil {V : Type u_1} [Fintype V] [DecidableEq V] : ofAnswers V [] = State.init.settle

theorem Epidemics.DFS.ofAnswers_append_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (b : Bool) : ofAnswers V (l ++ [b]) = ((ofAnswers V l).answer b).settle

theorem Epidemics.DFS.inv_ofAnswers {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : (ofAnswers V l).Inv

theorem Epidemics.DFS.move_ofAnswers {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : (ofAnswers V l).move = ofAnswers V l

The search is always stopped at a query (or finished).

theorem Epidemics.DFS.le_ofAnswers_append {V : Type u_1} [Fintype V] [DecidableEq V] (l l' : List Bool) : (ofAnswers V l).Le (ofAnswers V (l ++ l'))

theorem Epidemics.DFS.le_ofAnswers_take {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (j : ℕ) : (ofAnswers V (List.take j l)).Le (ofAnswers V l)

theorem Epidemics.DFS.finished_ofAnswers_append {V : Type u_1} [Fintype V] [DecidableEq V] (l l' : List Bool) (h : (ofAnswers V l).Finished) : (ofAnswers V (l ++ l')).Finished

theorem Epidemics.DFS.card_step {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (b : Bool) {e : Sym2 V} (hp : (ofAnswers V l).pending = some e) : (ofAnswers V (l ++ [b])).queried.card = (ofAnswers V l).queried.card + 1 ∧ (ofAnswers V (l ++ [b])).found.card = (ofAnswers V l).found.card + if b = true then 1 else 0

One query: the pending pair is queried, and found iff the answer is positive.

theorem Epidemics.DFS.card_queried_found_of_not_finished {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (h : ¬(ofAnswers V l).Finished) : (ofAnswers V l).queried.card = l.length ∧ (ofAnswers V l).found.card = List.count true l

theorem Epidemics.DFS.card_queried_found {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hl : l.length ≤ (Fintype.card V).choose 2) : (ofAnswers V l).queried.card = l.length ∧ (ofAnswers V l).found.card = List.count true l

Each answer is the answer to a new query: after t ≤ n (n - 1) / 2 answers, exactly t pairs have been queried, and the found pairs are the positive answers.

theorem Epidemics.DFS.card_found_le {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : (ofAnswers V l).found.card ≤ List.count true l

Queries

theorem Epidemics.DFS.fresh_nextQuery {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) : FreshUpTo (nextQuery e₀) ((Fintype.card V).choose 2)

Every pair is queried at most once: the search is a fresh strategy for all the n (n - 1) / 2 pairs of distinct vertices.

theorem Epidemics.DFS.card_queried_ofAnswers {V : Type u_1} [Fintype V] [DecidableEq V] {l : List Bool} (hl : l.length ≤ (Fintype.card V).choose 2) : (ofAnswers V l).queried.card = l.length

Each answer is the answer to a new query: after t ≤ n (n - 1) / 2 answers, exactly t pairs have been queried.

theorem Epidemics.DFS.not_isDiag_of_mem_queried {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) {e : Sym2 V} (he : e ∈ (ofAnswers V l).queried) : ¬e.IsDiag

Only pairs of distinct vertices are queried.

theorem Epidemics.DFS.mem_found_iff_of_queryAnswers {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) (ω : Sym2 V → Bool) (t : ℕ) {e : Sym2 V} (he : e ∈ (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).queried) : e ∈ (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).found ↔ ω e = true

On the coins ω, the search learns ω on the queried pairs: a queried pair has been found iff its coin is true.

theorem Epidemics.DFS.found_subset_queried {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : (ofAnswers V l).found ⊆ (ofAnswers V l).queried

The found pairs have been queried.

The sets S, U, T

theorem Epidemics.DFS.disjoint_done_stack {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : Disjoint (ofAnswers V l).done (ofAnswers V l).stack.toFinset ∧ (ofAnswers V l).stack.Nodup

S and U are disjoint and U has no repetition.

theorem Epidemics.DFS.stack_chain_ofAnswers {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : List.IsChain (fun (u v : V) => s(u, v) ∈ (ofAnswers V l).found) (ofAnswers V l).stack

U spans a path of found pairs: consecutive vertices of the stack form found pairs.

theorem Epidemics.DFS.queried_of_mem_done_of_mem_unvisited {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) {a b : V} (ha : a ∈ (ofAnswers V l).done) (hb : b ∈ (ofAnswers V l).unvisited) : s(a, b) ∈ (ofAnswers V l).queried ∧ s(a, b) ∉ (ofAnswers V l).found

All pairs between S and T have been queried and answered negatively.

theorem Epidemics.DFS.length_stack_le {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : (ofAnswers V l).stack.length ≤ 1 + List.count true l

|U| ≤ 1 + ∑ Xᵢ: every vertex of the stack but the first one of its epoch was pushed by a positive answer.

theorem Epidemics.DFS.not_finished_of_unvisited {V : Type u_1} [Fintype V] [DecidableEq V] {s : State V} (hT : s.unvisited.Nonempty) : ¬s.Finished

theorem Epidemics.DFS.count_true_add_epochs {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hT : (ofAnswers V l).unvisited.Nonempty) : List.count true l + (ofAnswers V l).epochs = ((ofAnswers V l).done ∪ (ofAnswers V l).stack.toFinset).card

While T ≠ ∅, every positive answer has moved a new vertex from T to U: |S ∪ U| is the number of positive answers plus the number of epochs.

theorem Epidemics.DFS.count_true_le_card {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hT : (ofAnswers V l).unvisited.Nonempty) : List.count true l ≤ ((ofAnswers V l).done ∪ (ofAnswers V l).stack.toFinset).card

While T ≠ ∅: ∑ Xᵢ ≤ |S ∪ U|.

theorem Epidemics.DFS.card_union_append_le {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (b : Bool) : ((ofAnswers V (l ++ [b])).done ∪ (ofAnswers V (l ++ [b])).stack.toFinset).card ≤ ((ofAnswers V l).done ∪ (ofAnswers V l).stack.toFinset).card + 2

Between two consecutive queries, |S ∪ U| grows by at most 2 (one push by a positive answer, one new epoch).

theorem Epidemics.DFS.card_union_nil_le {V : Type u_1} [Fintype V] [DecidableEq V] : ((ofAnswers V []).done ∪ (ofAnswers V []).stack.toFinset).card ≤ 1

At the start, |S ∪ U| ≤ 1.

Epochs

theorem Epidemics.DFS.reachable_of_mem_comp {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) {u v : V} (hu : u ∈ (ofAnswers V l).comp) (hv : v ∈ (ofAnswers V l).comp) : (SimpleGraph.fromEdgeSet ↑(ofAnswers V l).found).Reachable u v

The vertices discovered in the current epoch are connected by found pairs.

theorem Epidemics.DFS.card_comp_append {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (b : Bool) (hep : (ofAnswers V (l ++ [b])).epochs = (ofAnswers V l).epochs) (hnf : ¬(ofAnswers V l).Finished) : (ofAnswers V (l ++ [b])).comp.card = (ofAnswers V l).comp.card + if b = true then 1 else 0

One query in the same epoch, while T ≠ ∅: a positive answer adds a vertex to the epoch.

theorem Epidemics.DFS.count_drop_le_card_comp {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) {j : ℕ} (hj : j ≤ l.length) (hep : (ofAnswers V (List.take j l)).epochs = (ofAnswers V l).epochs) (hT : (ofAnswers V l).unvisited.Nonempty) : List.count true (List.drop j l) + (ofAnswers V (List.take j l)).comp.card ≤ (ofAnswers V l).comp.card

Within one epoch, while T ≠ ∅, each positive answer adds a vertex to the current epoch.

theorem Epidemics.DFS.exists_of_epochs_lt {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (b : Bool) (hep : (ofAnswers V l).epochs < (ofAnswers V (l ++ [b])).epochs) : ∃ D ⊆ (ofAnswers V (l ++ [b])).done, List.count true (l ++ [b]) ≤ D.card ∧ ∀ a ∈ D, ∀ c ∉ D, s(a, c) ∈ (ofAnswers V (l ++ [b])).queried

When a new epoch starts, U has just been emptied: the previously explored set D has all its pairs with V ∖ D queried; it contains a vertex for each positive answer, and it is contained in the current S.