Omnitigs and safe walks in genome assembly

StructureDirected multigraph#✓fully proved

A directed multigraph given by the source and target of each edge.

structure Multigraph (V : Type*) (E : Type*) where
  /-- The source (tail) of an edge. -/
  src : E → V
  /-- The target (head) of an edge. -/
  tgt : E → V

Used by 7

Used byCircular edge-covering walk · Omnitig · Safe walks are omnitigs · Path in a directed multigraph · Safe walk in a multigraph · Omnitigs are safe walks · Walk in a directed multigraph

DefinitionWalk in a directed multigraph#✓fully proved

A list of edges is a walk when consecutive edges are incident (head to tail).

def IsWalk (w : List E) : Prop := w.IsChain (fun e f => G.tgt e = G.src f)

Uses 1 · Used by 5

Statement usesDirected multigraph

Used byCircular edge-covering walk · Omnitig · Safe walks are omnitigs · Path in a directed multigraph · Omnitigs are safe walks

DefinitionPath in a directed multigraph#✓fully proved

A path: a nonempty walk whose nodes src e₀, tgt e₀, …, tgt e_ℓ are distinct, except that the first and last node may coincide.

def IsPath (p : List E) : Prop :=
  p ≠ [] ∧ IsWalk G p ∧ (p.map G.tgt).Nodup ∧
    ∀ e₀ ∈ p.head?, G.src e₀ ∉ (p.map G.tgt).dropLast

Uses 2 · Used by 3

Statement usesWalk in a directed multigraph · Directed multigraph

Used byOmnitig · Safe walks are omnitigs · Omnitigs are safe walks

DefinitionCircular edge-covering walk#✓fully proved

A circular edge-covering walk: a nonempty closed walk through every edge.

def IsCircularCovering (A : List E) : Prop :=
  A ≠ [] ∧ IsWalk G A ∧ (∀ a ∈ A.getLast?, ∀ b ∈ A.head?, G.tgt a = G.src b) ∧ ∀ e, e ∈ A

Uses 2 · Used by 3

Statement usesWalk in a directed multigraph · Directed multigraph

Used bySafe walks are omnitigs · Safe walk in a multigraph · Omnitigs are safe walks

DefinitionSubwalk of a circular walk#✓fully proved

w is a subwalk of the circular walk A: it is read off A from some start position, wrapping around (possibly several times).

def IsCircularSubwalk (w A : List E) : Prop :=
  ∃ p : ℕ, ∀ (i : ℕ) (hi : i < w.length), A[(p + i) % A.length]? = some w[i]

Used by 3

Used bySafe walks are omnitigs · Safe walk in a multigraph · Omnitigs are safe walks

DefinitionSafe walk in a multigraph#✓fully proved

Safe walk: a subwalk of every circular edge-covering walk.

def IsSafe (w : List E) : Prop :=
  ∀ A, IsCircularCovering G A → IsCircularSubwalk w A

Uses 3 · Used by 2

Statement usesCircular edge-covering walk · Subwalk of a circular walk · Directed multigraph

Used bySafe walks are omnitigs · Omnitigs are safe walks

DefinitionOmnitig#✓fully proved

Omnitig (Tomescu–Medvedev, Definition 5): for all 1 ≤ i ≤ j ≤ t (t + 1 = w.length), no path from v_j = src e_j to v_i = src e_i has first edge ≠ e_j and last edge ≠ e_{i-1}.

def IsOmnitig (w : List E) : Prop :=
  w ≠ [] ∧ IsWalk G w ∧
    ∀ (i j : ℕ) (hi : 1 ≤ i) (hij : i ≤ j) (hj : j < w.length) (p : List E), IsPath G p →
      ∀ f ∈ p.head?, ∀ l ∈ p.getLast?,
        G.src f = G.src w[j] → G.tgt l = G.src w[i] → f ≠ w[j] → l ≠ w[i - 1] → False

Uses 3 · Used by 2

Statement usesPath in a directed multigraph · Walk in a directed multigraph · Directed multigraph

Used bySafe walks are omnitigs · Omnitigs are safe walks

TheoremOmnitigs are safe walks#✓fully proved

Omnitigs are safe (Theorem 1, (2) ⇒ (1)).

theorem IsOmnitig.isSafe {w : List E} (hw : IsOmnitig G w) : IsSafe G w

Uses 7

Statement usesOmnitig · Safe walk in a multigraph · Directed multigraph

Proof usesCircular edge-covering walk · Subwalk of a circular walk · Path in a directed multigraph · Walk in a directed multigraph

TheoremSafe walks are omnitigs#✓fully proved

Safe walks are omnitigs (Theorem 1, (1) ⇒ (2)), when a circular edge-covering walk exists (otherwise every walk is vacuously safe).

theorem isOmnitig_of_isSafe {w : List E} (hne : w ≠ []) (hwalk : IsWalk G w)
    (hA : ∃ A, IsCircularCovering G A) (hs : IsSafe G w) : IsOmnitig G w

Uses 7

Statement usesCircular edge-covering walk · Omnitig · Safe walk in a multigraph · Walk in a directed multigraph · Directed multigraph

Proof usesSubwalk of a circular walk · Path in a directed multigraph

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.