De Bruijn graph genome assembly

DefinitionThe k-mers of a string#✓fully proved

The k-mers of s in order of position: the length-k windows (s.drop i).take k for i + k ≤ |s|.

def kmers {α : Type*} (k : ℕ) (s : List α) : List (List α) :=
  (List.range (s.length + 1 - k)).map fun i => (s.drop i).take k

Used by 5

Used byDe Bruijn multigraph of a string · Every Eulerian trail spells a string with the same k-mer multiset · The (k-1)-mer walk of a string spells the string · The (k-1)-mer walk of s traverses the de Bruijn multigraph in order · The k-mer walk of s is an Eulerian trail

DefinitionEfficient executable computation of k-mers#✓fully proved

Executable form of kmers: the suffixes of s are generated once by List.tails, so the cost is O(|s| · k) rather than the Θ(|s|²) of recomputing s.drop i for every i. The compiler uses it in place of kmers (kmers_eq_kmersImpl).

def kmersImpl {α : Type*} (k : ℕ) (s : List α) : List (List α) :=
  (s.tails.take (s.length + 1 - k)).map (·.take k)

DefinitionDe Bruijn edge of a k-mer#✓fully proved

The edge of the de Bruijn multigraph contributed by a k-mer w: from its prefix (k-1)-mer w.dropLast to its suffix (k-1)-mer w.tail.

def kmerEdge {α : Type*} (w : List α) : List α × List α := (w.dropLast, w.tail)

Used by 3

Used byDe Bruijn multigraph of a string · Every Eulerian trail spells a string with the same k-mer multiset · The (k-1)-mer walk of s traverses the de Bruijn multigraph in order

DefinitionDe Bruijn multigraph of a string#✓fully proved

The de Bruijn multigraph of s (Pevzner–Tang–Waterman 2001) as its list of edge occurrences: one edge per k-mer occurrence, in order of position.

def deBruijnEdges {α : Type*} (k : ℕ) (s : List α) : List (List α × List α) :=
  (kmers k s).map kmerEdge

Uses 2 · Used by 3

Statement usesDe Bruijn edge of a k-mer · The k-mers of a string

Used byEvery Eulerian trail spells a string with the same k-mer multiset · The (k-1)-mer walk of s traverses the de Bruijn multigraph in order · The k-mer walk of s is an Eulerian trail

DefinitionString spelled by a walk of (k-1)-mers#✓fully proved

The string spelled by a walk of (k-1)-mers: the first vertex followed by the last letter of each later vertex.

def spell {α : Type*} : List (List α) → List α
  | [] => []
  | v :: W => v ++ W.flatMap fun u => u.getLast?.toList

Used by 2

Used byEvery Eulerian trail spells a string with the same k-mer multiset · The (k-1)-mer walk of a string spells the string

TheoremThe (k-1)-mer walk of s traverses the de Bruijn multigraph in order#✓fully proved

Its steps are exactly the edges contributed by the k-mers of s, one per occurrence, in order of position.

theorem zip_tail_kmers {α : Type*} (k : ℕ) (hk : 1 ≤ k) (s : List α) :
    (kmers (k - 1) s).zip (kmers (k - 1) s).tail = deBruijnEdges k s

Uses 3 · Used by 1

Statement usesDe Bruijn multigraph of a string · The k-mers of a string

Proof usesDe Bruijn edge of a k-mer

Used byThe k-mer walk of s is an Eulerian trail

TheoremThe k-mer walk of s is an Eulerian trail#✓fully proved

The k-mer walk of s is an Eulerian trail of its de Bruijn multigraph: its steps are a permutation of the edge occurrences, each traversed once.

theorem zip_tail_kmers_perm {α : Type*} (k : ℕ) (hk : 1 ≤ k) (s : List α) :
    ((kmers (k - 1) s).zip (kmers (k - 1) s).tail).Perm (deBruijnEdges k s)

Uses 3

Statement usesDe Bruijn multigraph of a string · The k-mers of a string

Proof usesThe (k-1)-mer walk of s traverses the de Bruijn multigraph in order

TheoremThe (k-1)-mer walk of a string spells the string#✓fully proved

The (k-1)-mer walk of s spells s back (2 ≤ k, k - 1 ≤ |s|).

theorem spell_kmers {α : Type*} (k : ℕ) (hk : 2 ≤ k) (s : List α) (hs : k - 1 ≤ s.length) :
    spell (kmers (k - 1) s) = s

Uses 2

Statement usesThe k-mers of a string · String spelled by a walk of (k-1)-mers

TheoremEvery Eulerian trail spells a string with the same k-mer multiset#✓fully proved

Every Eulerian trail spells a string with the same k-mer multiset (2 ≤ k): if W is a walk of (k-1)-mers whose steps are a permutation of the edge occurrences of the de Bruijn multigraph of s, then the k-mers of the spelled string are a permutation of those of s. (The empty walk is allowed: it is a trail only when s has no k-mers, and spells [].)

theorem kmers_spell_perm {α : Type*} (k : ℕ) (hk : 2 ≤ k) (s : List α) (W : List (List α))
    (hlen : ∀ v ∈ W, v.length + 1 = k)
    (hW : (W.zip W.tail).Perm (deBruijnEdges k s)) :
    (kmers k (spell W)).Perm (kmers k s)

Uses 4

Statement usesDe Bruijn multigraph of a string · The k-mers of a string · String spelled by a walk of (k-1)-mers

Proof usesDe Bruijn edge of a k-mer

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.