Pairwise sequence alignment

AbbreviationAlignment#✓fully proved

An alignment over an alphabet \(\alpha\) is a finite list of columns, where each column is a pair \((u, v)\) and each of \(u\) and \(v\) is either a letter of \(\alpha\) or a gap.

Whether an alignment is valid for two given sequences is a separate condition.

abbrev Alignment (α : Type*) := List (Option α × Option α)

Used by 80

Used byAlignment score is at most minus the number of gap columns · Band check from a starting offset · A passing band check bounds the final offset · An alignment with few gap columns stays in the band from its start · Banded alignment score · Banded alignment is exact when some optimal alignment is banded · The banded optimum is exact · The banded score is at most the Needleman–Wunsch score · No banded score when the lengths differ by more than the band width · The banded score is defined when the lengths are close · Diagonal alignment · Number of gap columns of an alignment · The diagonal alignment is a valid alignment · Banded alignments · Banded alignments force close lengths · An alignment with at most w gap columns is w-banded · The band lemma · Affine-gap alignment score · Affine-gap score from a gap state · Linear gaps as affine gaps, from any gap state · Linear gaps are affine gaps with equal costs · Gotoh is optimal · The table is an upper bound · Gotoh is attained · The table is attained · Gotoh with equal gap scores is Needleman–Wunsch · Prepending a column with a gap in the second sequence · Prepending a column with a gap in the first sequence · Prepending a match column · Removing a leading column with a gap in the second sequence · Removing a leading column with a gap in the first sequence · Removing a leading match column from a valid alignment · Hirschberg reconstruction with enough fuel attains the optimum · The base-case alignment is optimal · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · Hirschberg's alignment algorithm · Hirschberg reconstruction with fuel · Hirschberg reconstruction on lists of length at most one · Hirschberg reconstruction splits the longer first list · Hirschberg recursion step splitting the second sequence · Hirschberg reconstruction with enough fuel is valid · The base-case alignment is valid · Base-case alignment for Hirschberg · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · Score of an induced pairwise alignment · Induced pairwise alignment · Letters of the first row of an induced alignment · Letters of the second row of an induced alignment · Induced pairwise alignments are valid · Induced alignments have no all-gap column · Joint weight of sequences and an alignment's state path · Every alignment weighs at most the Viterbi value · Two-alphabet alignments agree with single-alphabet alignments · The Viterbi value is attained · The pair-HMM recursion computes the total weight · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Score of an alignment · Needleman–Wunsch is optimal · Reversal preserves alignment score · The list of all alignments · Fuel-bounded enumeration of alignments · Needleman–Wunsch is attained · Valid alignment of two sequences · Concatenation of alignments · Extending an alignment by a letter of the second sequence · Extending an alignment by a letter of the first sequence · Reversing an alignment · The enumerated alignments are exactly the valid ones · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Needleman–Wunsch is reversal-invariant · Alignment score is the negated linear-penalty cost · Cost of an alignment under linear gap penalties · Exactness of the wavefront alignment algorithm · The wavefront algorithm computes the optimal alignment cost · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionValid alignment of two sequences#✓fully proved

A list \(A\) of columns, each a pair of optional letters, is an alignment of sequences \(x\) and \(y\) when no column has both entries empty, the letters present in the first entries of the columns, read in order, form \(x\), and the letters present in the second entries, read in order, form \(y\).

def IsAlignment (A : Alignment α) (xs ys : List α) : Prop :=
  (∀ c ∈ A, c ≠ (none, none)) ∧ A.filterMap Prod.fst = xs ∧ A.filterMap Prod.snd = ys

Uses 1 · Used by 44

Statement usesAlignment

Used byBanded alignment is exact when some optimal alignment is banded · The banded optimum is exact · The banded score is at most the Needleman–Wunsch score · No banded score when the lengths differ by more than the band width · The banded score is defined when the lengths are close · The diagonal alignment is a valid alignment · Banded alignments force close lengths · Gotoh is optimal · The table is an upper bound · Gotoh is attained · The table is attained · Gotoh with equal gap scores is Needleman–Wunsch · Prepending a column with a gap in the second sequence · Prepending a column with a gap in the first sequence · Prepending a match column · Removing a leading column with a gap in the second sequence · Removing a leading column with a gap in the first sequence · Removing a leading match column from a valid alignment · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · Hirschberg reconstruction is valid · Hirschberg reconstruction with enough fuel is valid · The base-case alignment is valid · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · Induced pairwise alignments are valid · Every alignment weighs at most the Viterbi value · The Viterbi value is attained · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Needleman–Wunsch is optimal · Needleman–Wunsch is attained · Concatenation of alignments · Extending an alignment by a letter of the second sequence · Extending an alignment by a letter of the first sequence · Reversing an alignment · The enumerated alignments are exactly the valid ones · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Needleman–Wunsch is reversal-invariant · Exactness of the wavefront alignment algorithm · The wavefront algorithm computes the optimal alignment cost · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionScore of an alignment column#✓fully proved

Given a substitution score \(\sigma\), which assigns an integer \(\sigma(a, b)\) to all letters \(a, b \in \alpha\), and a gap score \(g \in \mathbb{Z}\), a column pairing letters \(a\) and \(b\) scores \(\sigma(a, b)\), a column pairing a letter with a gap (on either side) scores \(g\), and a column with a gap on both sides scores \(0\).

def columnScore (σ : α → α → ℤ) (gap : ℤ) : Option α × Option α → ℤ
  | (some a, some b) => σ a b
  | (some _, none) => gap
  | (none, some _) => gap
  | (none, none) => 0

Used by 20

Used byAlignment score is at most minus the number of gap columns · Linear gaps as affine gaps, from any gap state · Hirschberg reconstruction with enough fuel attains the optimum · The base-case alignment is optimal · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · Score of an induced pairwise alignment · Sum-of-pairs score of a column · The SP score is the sum of the induced pairwise scores · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Score of an alignment · Needleman–Wunsch is optimal · Reversal preserves alignment score · Needleman–Wunsch is attained · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Alignment score is the negated linear-penalty cost

DefinitionScore of an alignment#✓fully proved

Given a substitution score \(\sigma\), which assigns an integer \(\sigma(a, b)\) to all letters \(a, b \in \alpha\), and a gap score \(g \in \mathbb{Z}\), the score of an alignment \(A\) over \(\alpha\) is the sum, over all columns of \(A\), of the score of the column with respect to \(\sigma\) and \(g\).

def alignmentScore (σ : α → α → ℤ) (gap : ℤ) (A : Alignment α) : ℤ :=
  (A.map (columnScore σ gap)).sum

Uses 2 · Used by 31

Statement usesAlignment · Score of an alignment column

Used byAlignment score is at most minus the number of gap columns · Banded alignment score · Banded alignment is exact when some optimal alignment is banded · The banded optimum is exact · The banded score is at most the Needleman–Wunsch score · No banded score when the lengths differ by more than the band width · The banded score is defined when the lengths are close · The band lemma · Linear gaps as affine gaps, from any gap state · Linear gaps are affine gaps with equal costs · Gotoh with equal gap scores is Needleman–Wunsch · Hirschberg reconstruction attains the Needleman–Wunsch optimum · Hirschberg reconstruction with enough fuel attains the optimum · The base-case alignment is optimal · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · Score of an induced pairwise alignment · The SP score is the sum of the induced pairwise scores · The sum-of-pairs score is bounded by the pairwise optima · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Needleman–Wunsch is optimal · Reversal preserves alignment score · Needleman–Wunsch is attained · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Needleman–Wunsch is reversal-invariant · Alignment score is the negated linear-penalty cost · The wavefront algorithm computes the optimal alignment cost

TheoremConcatenation of alignments#✓fully proved

If \(A_1\) is an alignment of sequences \(x_1\) and \(y_1\), and \(A_2\) is an alignment of sequences \(x_2\) and \(y_2\), then the concatenation of \(A_1\) and \(A_2\) is an alignment of the concatenation of \(x_1\) and \(x_2\) and the concatenation of \(y_1\) and \(y_2\).

theorem isAlignment_append {A1 A2 : Alignment α} {xs1 ys1 xs2 ys2 : List α}
    (h1 : IsAlignment A1 xs1 ys1) (h2 : IsAlignment A2 xs2 ys2) :
    IsAlignment (A1 ++ A2) (xs1 ++ xs2) (ys1 ++ ys2)

Uses 2 · Used by 3

Statement usesAlignment · Valid alignment of two sequences

Used byHirschberg reconstruction with enough fuel is valid · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum

DefinitionFuel-bounded Needleman–Wunsch recursion#✓fully proved

Fix a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\), and write \(|x|\) for the length of a sequence \(x\) and \(ax\) for the sequence with first element \(a\) followed by \(x\). For a fuel \(n \in \mathbb{N}\) and sequences \(x, y\) over \(\alpha\), the value \(N_n(x, y) \in \mathbb{Z}\) is defined by \(N_0(x, y) = 0\), by \(N_{n+1}(x, y) = g\,|y|\) if \(x\) is empty and \(N_{n+1}(x, y) = g\,|x|\) if \(y\) is empty, and by

\[N_{n+1}(ax, by) = \max\bigl(N_n(x, y) + \sigma(a, b),\ N_n(x, by) + g,\ N_n(ax, y) + g\bigr).\]

The Needleman–Wunsch score of \(x\) and \(y\) is \(N_{|x|+|y|}(x, y)\); this fuel suffices because every recursive call shortens the pair. This is an exponential-time specification, not a memoized table.

def nwScoreAux : ℕ → List α → List α → ℤ
  | 0, _, _ => 0
  | _ + 1, [], [] => 0
  | _ + 1, [], b :: ys => gap * ((b :: ys).length : ℤ)
  | _ + 1, a :: xs, [] => gap * ((a :: xs).length : ℤ)
  | n + 1, a :: xs, b :: ys =>
      max (max (nwScoreAux n xs ys + σ a b) (nwScoreAux n xs (b :: ys) + gap))
        (nwScoreAux n (a :: xs) ys + gap)

Used by 6

Used byNeedleman–Wunsch is optimal · Needleman–Wunsch is attained · Needleman–Wunsch score · The Needleman–Wunsch recurrence · Aligning the empty sequence with a sequence · Aligning a sequence with the empty sequence

DefinitionNeedleman–Wunsch score#✓fully proved

Given a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\), the Needleman–Wunsch score \(\mathrm{NW}(xs, ys)\) of two lists over \(\alpha\) is defined by recursion on their total length: if one of the lists is empty, it is \(g\) times the length of the other; and for lists \(a\,xs\) and \(b\,ys\) with heads \(a\), \(b\) and tails \(xs\), \(ys\),

\[\mathrm{NW}(a\,xs, b\,ys) = \max\bigl(\mathrm{NW}(xs, ys) + \sigma(a, b), \ \mathrm{NW}(xs, b\,ys) + g,\ \mathrm{NW}(a\,xs, ys) + g\bigr).\]

By the Needleman–Wunsch optimality theorem, this is the optimal global alignment score of the two lists.

def nwScore (xs ys : List α) : ℤ := nwScoreAux σ gap (xs.length + ys.length) xs ys

Uses 1 · Used by 56

Statement usesFuel-bounded Needleman–Wunsch recursion

Used byBanded alignment is exact when some optimal alignment is banded · The banded optimum is exact · The banded score is at most the Needleman–Wunsch score · Gotoh with equal gap scores is Needleman–Wunsch · Gotoh table with equal gap costs gives the Needleman–Wunsch score · Hirschberg reconstruction attains the Needleman–Wunsch optimum · Hirschberg reconstruction with enough fuel attains the optimum · The base-case alignment is optimal · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · Hirschberg reconstruction with fuel · Hirschberg reconstruction on lists of length at most one · Hirschberg reconstruction splits the longer first list · Hirschberg recursion step splitting the second sequence · Hirschberg reconstruction with enough fuel is valid · Hirschberg split identity, splitting the first sequence · Hirschberg split identity, splitting the second sequence · Needleman–Wunsch score of two single letters · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · The sum-of-pairs score is bounded by the pairwise optima · Log-odds Viterbi is linear-gap Needleman–Wunsch · Needleman–Wunsch is optimal · Needleman–Wunsch is attained · The suffix maximum is attained · Local alignment score · The local score equals the Smith–Waterman score · Upper bounds on the local score · One row of the table · The last row of the table · The Needleman–Wunsch recurrence · Infix pairs score at most the local score · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Suffix pairs score at most the suffix maximum · Suffix pairs score at most the terminal Smith–Waterman cell · Aligning the empty sequence with a sequence · Aligning a sequence with the empty sequence · Needleman–Wunsch is reversal-invariant · The Needleman–Wunsch recurrence, end-peeling · The table computes the optimal global alignment score · Suffix maximum of Needleman–Wunsch scores · Upper bounds on the suffix maximum · The terminal cell is at most the suffix maximum · The fitting score is attained · The overlap score is attained · Fitting score · Upper bounds on the fitting score · The fitting score is at most the local score · Infix scores are at most the fitting score · Overlap-pair scores are at most the overlap score · Overlap alignment score · Upper bounds for the overlap score · The overlap score is at most the local score · The overlap score is nonnegative · The wavefront algorithm computes the optimal alignment cost

TheoremAligning the empty sequence with a sequence#✓fully proved

For every substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\), gap score \(g \in \mathbb{Z}\) and sequence \(y\) over \(\alpha\) of length \(|y|\), the Needleman–Wunsch score of the empty sequence and \(y\) with respect to \(\sigma\) and \(g\) is \(g\,|y|\): one gap per letter.

theorem nwScore_nil_left (ys : List α) : nwScore σ gap [] ys = gap * ys.length

Uses 2 · Used by 9

Statement usesNeedleman–Wunsch score

Proof usesFuel-bounded Needleman–Wunsch recursion

Used byThe base-case alignment is optimal · Needleman–Wunsch score of two single letters · Needleman–Wunsch is optimal · Needleman–Wunsch is attained · The suffix maximum is attained · Upper bounds on the local score · The last row of the table · Suffix pairs score at most the terminal Smith–Waterman cell · Upper bounds on the suffix maximum

TheoremAligning a sequence with the empty sequence#✓fully proved

For every substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\), gap score \(g \in \mathbb{Z}\) and sequence \(x\) over \(\alpha\) of length \(|x|\), the Needleman–Wunsch score of \(x\) and the empty sequence with respect to \(\sigma\) and \(g\) is \(g\,|x|\): one gap per letter.

theorem nwScore_nil_right (xs : List α) : nwScore σ gap xs [] = gap * xs.length

Uses 2 · Used by 6

Statement usesNeedleman–Wunsch score

Proof usesFuel-bounded Needleman–Wunsch recursion

Used byThe base-case alignment is optimal · Needleman–Wunsch score of two single letters · Needleman–Wunsch is optimal · Needleman–Wunsch is attained · One row of the table · Suffix pairs score at most the terminal Smith–Waterman cell

TheoremThe Needleman–Wunsch recurrence#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \in \mathbb{Z}\) a gap score, and write \(N(x, y)\) for the Needleman–Wunsch score of sequences \(x, y\) over \(\alpha\) with respect to \(\sigma\) and \(g\). For all letters \(a, b \in \alpha\) and sequences \(x, y\), writing \(ax\) for the sequence with first element \(a\) followed by \(x\),

\[N(ax, by) = \max\bigl(N(x, y) + \sigma(a, b),\ N(x, by) + g,\ N(ax, y) + g\bigr).\]

theorem nwScore_eq (a b : α) (xs ys : List α) :
    nwScore σ gap (a :: xs) (b :: ys) =
      max (max (nwScore σ gap xs ys + σ a b) (nwScore σ gap xs (b :: ys) + gap))
        (nwScore σ gap (a :: xs) ys + gap)

Uses 2 · Used by 4

Statement usesNeedleman–Wunsch score

Proof usesFuel-bounded Needleman–Wunsch recursion

Used byNeedleman–Wunsch score of two single letters · Needleman–Wunsch is optimal · Needleman–Wunsch is attained · The Needleman–Wunsch recurrence, end-peeling

DefinitionFuel-bounded enumeration of alignments#✓fully proved

Given a fuel \(n \in \mathbb{N}\) and sequences \(x\) and \(y\) over \(\alpha\), this lists alignments column by column from the front. With fuel \(0\) the list is empty. With fuel \(n + 1\): two empty sequences give the single empty alignment; if only \(y\) is nonempty, with first letter \(b\) and rest \(y'\), each alignment of \(x\) and \(y'\) with fuel \(n\) is preceded by the column pairing a gap with \(b\); if only \(x\) is nonempty, with first letter \(a\) and rest \(x'\), each alignment of \(x'\) and \(y\) with fuel \(n\) is preceded by the column pairing \(a\) with a gap; and if both are nonempty, \(x\) with first letter \(a\) and rest \(x'\) and \(y\) with first letter \(b\) and rest \(y'\), the list consists of the alignments of \(x'\) and \(y'\) preceded by the column \((a, b)\), then those of \(x'\) and \(y\) preceded by the column pairing \(a\) with a gap, then those of \(x\) and \(y'\) preceded by the column pairing a gap with \(b\), each computed with fuel \(n\).

With fuel at least \(|x| + |y| + 1\) the fuel never runs out before both sequences are used up; with less fuel some alignments are missing from the list.

def alignmentsAux : ℕ → List α → List α → List (Alignment α)
  | 0, _, _ => []
  | _ + 1, [], [] => [[]]
  | n + 1, [], b :: ys => (alignmentsAux n [] ys).map fun A => (none, some b) :: A
  | n + 1, a :: xs, [] => (alignmentsAux n xs []).map fun A => (some a, none) :: A
  | n + 1, a :: xs, b :: ys =>
      (alignmentsAux n xs ys).map (fun A => (some a, some b) :: A) ++
        (alignmentsAux n xs (b :: ys)).map (fun A => (some a, none) :: A) ++
        (alignmentsAux n (a :: xs) ys).map (fun A => (none, some b) :: A)

Uses 1 · Used by 3

Statement usesAlignment

Used byTwo-alphabet alignments agree with single-alphabet alignments · The list of all alignments · The enumerated alignments are exactly the valid ones

DefinitionThe list of all alignments#✓fully proved

For sequences \(x\) and \(y\) over \(\alpha\), this is the list produced by the fuel-bounded enumeration of alignments of \(x\) and \(y\) with fuel \(|x| + |y| + 1\).

This fuel suffices: an alignment belongs to the list exactly when it is a valid alignment of \(x\) and \(y\).

def alignments (xs ys : List α) : List (Alignment α) :=
  alignmentsAux (xs.length + ys.length + 1) xs ys

Uses 2 · Used by 10

Statement usesAlignment · Fuel-bounded enumeration of alignments

Used byBanded alignment score · Banded alignment is exact when some optimal alignment is banded · The banded score is at most the Needleman–Wunsch score · No banded score when the lengths differ by more than the band width · The banded score is defined when the lengths are close · Every alignment weighs at most the Viterbi value · Two-alphabet alignments agree with single-alphabet alignments · The Viterbi value is attained · The pair-HMM recursion computes the total weight · The enumerated alignments are exactly the valid ones

TheoremThe enumerated alignments are exactly the valid ones#✓fully proved

For sequences \(x\) and \(y\) and a list \(A\) of columns, \(A\) occurs in the enumerated list of all alignments of \(x\) and \(y\) if and only if \(A\) is an alignment of \(x\) and \(y\).

theorem mem_alignments (xs ys : List α) (A : Alignment α) :
    A ∈ alignments xs ys ↔ IsAlignment A xs ys

Uses 4 · Used by 6

Statement usesAlignment · Valid alignment of two sequences · The list of all alignments

Proof usesFuel-bounded enumeration of alignments

Used byBanded alignment is exact when some optimal alignment is banded · The banded score is at most the Needleman–Wunsch score · No banded score when the lengths differ by more than the band width · The banded score is defined when the lengths are close · Every alignment weighs at most the Viterbi value · The Viterbi value is attained

TheoremNeedleman–Wunsch is optimal#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \in \mathbb{Z}\) a gap score. For all sequences \(x\) and \(y\) over \(\alpha\) and every valid alignment \(A\) of \(x\) and \(y\), the score of \(A\) with respect to \(\sigma\) and \(g\) is at most the Needleman–Wunsch score of \(x\) and \(y\).

theorem alignmentScore_le_nwScore (xs ys : List α) (A : Alignment α)
    (hA : IsAlignment A xs ys) :
    alignmentScore σ gap A ≤ nwScore σ gap xs ys

Uses 9 · Used by 12

Statement usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch score

Proof usesScore of an alignment column · Fuel-bounded Needleman–Wunsch recursion · The Needleman–Wunsch recurrence · Aligning the empty sequence with a sequence · Aligning a sequence with the empty sequence

Used byThe banded score is at most the Needleman–Wunsch score · Gotoh with equal gap scores is Needleman–Wunsch · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · The sum-of-pairs score is bounded by the pairwise optima · Log-odds Viterbi is linear-gap Needleman–Wunsch · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Needleman–Wunsch is reversal-invariant · The wavefront algorithm computes the optimal alignment cost

TheoremNeedleman–Wunsch is attained#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \in \mathbb{Z}\) a gap score. For all sequences \(x\) and \(y\) over \(\alpha\) there is a valid alignment \(A\) of \(x\) and \(y\) whose score with respect to \(\sigma\) and \(g\) equals the Needleman–Wunsch score of \(x\) and \(y\).

theorem exists_alignmentScore_eq_nwScore (xs ys : List α) :
    ∃ A : Alignment α, IsAlignment A xs ys ∧ alignmentScore σ gap A = nwScore σ gap xs ys

Uses 9 · Used by 11

Statement usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch score

Proof usesScore of an alignment column · Fuel-bounded Needleman–Wunsch recursion · The Needleman–Wunsch recurrence · Aligning the empty sequence with a sequence · Aligning a sequence with the empty sequence

Used byThe banded optimum is exact · Gotoh with equal gap scores is Needleman–Wunsch · Every cut of the first list extends to an optimal split · Every cut of the second list extends to an optimal split · A split of the first sequence scores at most the Needleman–Wunsch optimum · A split of the second sequence scores at most the Needleman–Wunsch optimum · Log-odds Viterbi is linear-gap Needleman–Wunsch · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Needleman–Wunsch is reversal-invariant · The wavefront algorithm computes the optimal alignment cost

DefinitionFuel-bounded Smith–Waterman recursion#✓fully proved

Fix a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\), and write \(ax\) for the sequence with first element \(a\) followed by \(x\). For a fuel \(n \in \mathbb{N}\) and sequences \(x, y\) over \(\alpha\), the value \(F_n(x, y) \in \mathbb{Z}\) is defined by \(F_0(x, y) = 0\), by \(F_{n+1}(x, y) = 0\) if \(x\) or \(y\) is empty, and by

\[F_{n+1}(ax, by) = \max\bigl(0,\ F_n(x, y) + \sigma(a, b),\ F_n(x, by) + g, \ F_n(ax, y) + g\bigr).\]

This is an exponential-time specification, not a memoized table.

def swCellFront : ℕ → List α → List α → ℤ
  | 0, _, _ => 0
  | _ + 1, [], _ => 0
  | _ + 1, _, [] => 0
  | n + 1, a :: xs, b :: ys =>
      max 0 (max (max (swCellFront n xs ys + σ a b) (swCellFront n xs (b :: ys) + gap))
        (swCellFront n (a :: xs) ys + gap))

Used by 5

Used byThe terminal Smith–Waterman cell · The Smith–Waterman recurrence · The terminal cell vanishes when the first sequence is empty · The terminal cell vanishes when the second sequence is empty · The terminal Smith–Waterman cell is nonnegative

DefinitionThe terminal Smith–Waterman cell#✓fully proved

Given a substitution score \(\sigma(a, b) \in \mathbb{Z}\) for letters \(a, b\) and a gap score \(g \in \mathbb{Z}\), and writing \(sc\) for a sequence \(s\) followed by a letter \(c\), the terminal Smith–Waterman cell \(H(x, y)\) of two sequences \(x\) and \(y\) is the integer defined by \(H(x, y) = 0\) when \(x\) or \(y\) is empty, and

\[H(xa, yb) = \max\bigl(0,\ H(x, y) + \sigma(a, b),\ H(x, yb) + g,\ H(xa, y) + g\bigr)\]

for all sequences \(x, y\) and letters \(a, b\). It is the entry \(H(|x|, |y|)\) of the Smith–Waterman dynamic-programming table.

For \(g \le 0\) it equals the maximum Needleman–Wunsch score over pairs of suffixes of \(x\) and \(y\); for \(g > 0\) it can be strictly smaller (for one-letter sequences with \(\sigma = -100\) and \(g = 1\) the cell is \(1\), while the alignment with two gap columns scores \(2\)). It is not the optimal local alignment score over all positions; that is the Smith–Waterman score, the maximum of this cell over all pairs of prefixes.

def swCellScore (xs ys : List α) : ℤ :=
  swCellFront σ gap (xs.length + ys.length) xs.reverse ys.reverse

Uses 1 · Used by 14

Statement usesFuel-bounded Smith–Waterman recursion

Used byThe local score equals the Smith–Waterman score · Suffix pairs score at most the terminal Smith–Waterman cell · The suffix maximum is at most the terminal Smith–Waterman cell · The Smith–Waterman recurrence · For nonpositive gaps, the terminal Smith–Waterman cell is the best suffix-pair score · The terminal cell is at most the suffix maximum · Each prefix-pair cell is at most the Smith–Waterman score · The terminal cell vanishes when the first sequence is empty · The terminal cell vanishes when the second sequence is empty · The terminal Smith–Waterman cell is nonnegative · The Smith–Waterman score · Bounding the Smith–Waterman score by its cells · One row of the table · The table computes the Smith–Waterman score

TheoremThe terminal Smith–Waterman cell is nonnegative#✓fully proved

For every substitution score \(\sigma\), every gap score \(g\) and all sequences \(x\) and \(y\), the terminal Smith–Waterman cell \(H(x, y)\) satisfies \(H(x, y) \ge 0\).

theorem swCellScore_nonneg (xs ys : List α) : 0 ≤ swCellScore σ gap xs ys

Uses 2 · Used by 1

Statement usesThe terminal Smith–Waterman cell

Proof usesFuel-bounded Smith–Waterman recursion

Used bySuffix pairs score at most the terminal Smith–Waterman cell

TheoremThe terminal cell vanishes when the first sequence is empty#✓fully proved

For a substitution score \(\sigma\), a gap score \(g\) and every sequence \(y\), the terminal Smith–Waterman cell of the empty sequence and \(y\) is \(0\).

theorem swCellScore_nil_left (ys : List α) : swCellScore σ gap [] ys = 0

Uses 2 · Used by 3

Statement usesThe terminal Smith–Waterman cell

Proof usesFuel-bounded Smith–Waterman recursion

Used byThe terminal cell is at most the suffix maximum · Bounding the Smith–Waterman score by its cells · The table computes the Smith–Waterman score

TheoremThe terminal cell vanishes when the second sequence is empty#✓fully proved

For a substitution score \(\sigma\), a gap score \(g\) and every sequence \(x\), the terminal Smith–Waterman cell of \(x\) and the empty sequence is \(0\).

theorem swCellScore_nil_right (xs : List α) : swCellScore σ gap xs [] = 0

Uses 2 · Used by 2

Statement usesThe terminal Smith–Waterman cell

Proof usesFuel-bounded Smith–Waterman recursion

Used byThe terminal cell is at most the suffix maximum · One row of the table

TheoremThe Smith–Waterman recurrence#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) a gap score, and for a sequence \(s\) and a letter \(c\) write \(sc\) for \(s\) followed by \(c\). For all sequences \(x\) and \(y\) and all letters \(a\) and \(b\), the terminal Smith–Waterman cell \(H\) satisfies

\[H(xa, yb) = \max\bigl(0,\ H(x, y) + \sigma(a, b),\ H(x, yb) + g,\ H(xa, y) + g\bigr).\]

theorem swCellScore_eq (xs ys : List α) (a b : α) :
    swCellScore σ gap (xs ++ [a]) (ys ++ [b]) =
      max 0 (max (max (swCellScore σ gap xs ys + σ a b)
        (swCellScore σ gap xs (ys ++ [b]) + gap))
        (swCellScore σ gap (xs ++ [a]) ys + gap))

Uses 2 · Used by 3

Statement usesThe terminal Smith–Waterman cell

Proof usesFuel-bounded Smith–Waterman recursion

Used bySuffix pairs score at most the terminal Smith–Waterman cell · The terminal cell is at most the suffix maximum · One row of the table

TheoremSuffixes of a list with an element appended#✓fully proved

If \(s\) is a suffix of the list obtained by appending an element \(a\) at the end of a list \(xs\), then either \(s\) is empty, or there is a suffix \(s'\) of \(xs\) such that \(s\) is \(s'\) with \(a\) appended at the end.

theorem suffix_of_snoc {xs : List α} {a : α} {s : List α} (h : s <:+ xs ++ [a]) :
    s = [] ∨ ∃ s', s' <:+ xs ∧ s = s' ++ [a]

Used by 1

Used bySuffix pairs score at most the terminal Smith–Waterman cell

TheoremAppending an element preserves suffixes#✓fully proved

If a list \(s\) is a suffix of a list \(xs\), then for every element \(a\), the list \(s\) with \(a\) appended at the end is a suffix of \(xs\) with \(a\) appended at the end.

theorem suffix_append_snoc {s xs : List α} {a : α} (h : s <:+ xs) : s ++ [a] <:+ xs ++ [a]

Used by 2

Used bySuffix pairs score at most the terminal Smith–Waterman cell · The terminal cell is at most the suffix maximum

TheoremReversing an alignment#✓fully proved

For a list of columns \(A\) and sequences \(x\) and \(y\), \(A\) is an alignment of the reversal of \(x\) and the reversal of \(y\) if and only if the reversal of \(A\) (its columns in reverse order) is an alignment of \(x\) and \(y\).

theorem isAlignment_reverse {A : Alignment α} {xs ys : List α} :
    IsAlignment A xs.reverse ys.reverse ↔ IsAlignment A.reverse xs ys

Uses 2 · Used by 1

Statement usesAlignment · Valid alignment of two sequences

Used byNeedleman–Wunsch is reversal-invariant

TheoremReversal preserves alignment score#✓fully proved

For every substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\), gap score \(g \in \mathbb{Z}\) and alignment \(A\), the alignment obtained by listing the columns of \(A\) in reverse order has the same score as \(A\).

theorem alignmentScore_reverse (A : Alignment α) :
    alignmentScore σ gap A.reverse = alignmentScore σ gap A

Uses 3 · Used by 1

Statement usesAlignment · Score of an alignment

Proof usesScore of an alignment column

Used byNeedleman–Wunsch is reversal-invariant

TheoremNeedleman–Wunsch is reversal-invariant#✓fully proved

Reversing both sequences preserves the optimal global score.

theorem nwScore_reverse (xs ys : List α) :
    nwScore σ gap xs.reverse ys.reverse = nwScore σ gap xs ys

Uses 8 · Used by 1

Statement usesNeedleman–Wunsch score

Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch is optimal · Reversal preserves alignment score · Needleman–Wunsch is attained · Reversing an alignment

Used byThe Needleman–Wunsch recurrence, end-peeling

TheoremThe Needleman–Wunsch recurrence, end-peeling#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \in \mathbb{Z}\) a gap score, and write \(N(x, y)\) for the Needleman–Wunsch score of sequences \(x, y\) over \(\alpha\) with respect to \(\sigma\) and \(g\). For all sequences \(x, y\) and letters \(a, b \in \alpha\), writing \(xa\) for the sequence \(x\) followed by the letter \(a\),

\[N(xa, yb) = \max\bigl(N(x, y) + \sigma(a, b),\ N(x, yb) + g,\ N(xa, y) + g\bigr).\]

theorem nwScore_snoc (xs ys : List α) (a b : α) :
    nwScore σ gap (xs ++ [a]) (ys ++ [b]) =
      max (max (nwScore σ gap xs ys + σ a b) (nwScore σ gap xs (ys ++ [b]) + gap))
        (nwScore σ gap (xs ++ [a]) ys + gap)

Uses 3 · Used by 3

Statement usesNeedleman–Wunsch score

Proof usesThe Needleman–Wunsch recurrence · Needleman–Wunsch is reversal-invariant

Used byOne row of the table · Suffix pairs score at most the terminal Smith–Waterman cell · The terminal cell is at most the suffix maximum

DefinitionMaximum of an integer list with floor zero#✓fully proved

For a list \(l\) of integers, this is the largest of \(0\) and the entries of \(l\); in particular the empty list gives \(0\).

It is used to define the suffix maximum, the local score and the Smith–Waterman score.

def listMax (xs : List ℤ) : ℤ := xs.foldr (max ·) 0

Used by 17

Used byThe suffix maximum is attained · Local alignment score · Upper bounds on the local score · Infix pairs score at most the local score · Suffix pairs score at most the suffix maximum · Suffix maximum of Needleman–Wunsch scores · Upper bounds on the suffix maximum · Each prefix-pair cell is at most the Smith–Waterman score · The Smith–Waterman score · Bounding the Smith–Waterman score by its cells · The overlap score is attained · Overlap-pair scores are at most the overlap score · Overlap alignment score · Upper bounds for the overlap score · The floored list maximum is nonnegative · Row-by-row filling of the Smith–Waterman table · The table computes the Smith–Waterman score

DefinitionPairs of suffixes#✓fully proved

For lists \(xs\) and \(ys\), the list of all pairs \((u, v)\) where \(u\) is a suffix of \(xs\) and \(v\) is a suffix of \(ys\), the empty lists and \(xs\), \(ys\) themselves included.

def suffixPairs (xs ys : List α) : List (List α × List α) :=
  xs.tails.product ys.tails

Used by 8

Used byThe suffix maximum is attained · The local score equals the Smith–Waterman score · Suffix pairs score at most the suffix maximum · Suffix maximum of Needleman–Wunsch scores · Upper bounds on the suffix maximum · The suffix maximum is at most the terminal Smith–Waterman cell · The terminal cell is at most the suffix maximum · The suffix maximum is nonnegative

DefinitionSuffix maximum of Needleman–Wunsch scores#✓fully proved

Given a substitution score \(\sigma\) and an integer gap score \(g\), the suffix maximum of lists \(xs\) and \(ys\) is the maximum of the Needleman–Wunsch scores of all pairs \((u, v)\) with \(u\) a suffix of \(xs\) and \(v\) a suffix of \(ys\).

The maximum is taken with floor \(0\), which changes nothing, since the pair of empty suffixes scores \(0\).

def suffixMax (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) : ℤ :=
  listMax ((suffixPairs xs ys).map (fun p => nwScore σ gap p.1 p.2))

Uses 3 · Used by 8

Statement usesMaximum of an integer list with floor zero · Needleman–Wunsch score · Pairs of suffixes

Used byThe suffix maximum is attained · The local score equals the Smith–Waterman score · Suffix pairs score at most the suffix maximum · Upper bounds on the suffix maximum · The suffix maximum is at most the terminal Smith–Waterman cell · For nonpositive gaps, the terminal Smith–Waterman cell is the best suffix-pair score · The terminal cell is at most the suffix maximum · The suffix maximum is nonnegative

TheoremSuffix pairs score at most the suffix maximum#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \in \mathbb{Z}\) a gap score. If \((x', y')\) is a suffix pair of sequences \(x\) and \(y\) over \(\alpha\), that is, \(x'\) is a suffix of \(x\) and \(y'\) is a suffix of \(y\), then the Needleman–Wunsch score of \(x'\) and \(y'\) is at most the suffix maximum of \(x\) and \(y\), both with respect to \(\sigma\) and \(g\).

theorem nwScore_le_suffixMax {xs' ys' xs ys : List α}
    (h : (xs', ys') ∈ suffixPairs xs ys) :
    nwScore σ gap xs' ys' ≤ suffixMax σ gap xs ys

Uses 4 · Used by 2

Statement usesNeedleman–Wunsch score · Suffix maximum of Needleman–Wunsch scores · Pairs of suffixes

Proof usesMaximum of an integer list with floor zero

Used byThe terminal cell is at most the suffix maximum · The suffix maximum is nonnegative

TheoremUpper bounds on the suffix maximum#✓fully proved

Let \(\sigma\) be a substitution score, \(g\) an integer gap score, \(xs\) and \(ys\) lists and \(y\) an integer. If every pair \((u, v)\) with \(u\) a suffix of \(xs\) and \(v\) a suffix of \(ys\) has Needleman–Wunsch score at most \(y\), then the maximum Needleman–Wunsch score over all such suffix pairs is at most \(y\).

theorem suffixMax_le {xs ys : List α} {y : ℤ}
    (h : ∀ p ∈ suffixPairs xs ys, nwScore σ gap p.1 p.2 ≤ y) :
    suffixMax σ gap xs ys ≤ y

Uses 5 · Used by 1

Statement usesNeedleman–Wunsch score · Suffix maximum of Needleman–Wunsch scores · Pairs of suffixes

Proof usesMaximum of an integer list with floor zero · Aligning the empty sequence with a sequence

Used byThe suffix maximum is at most the terminal Smith–Waterman cell

TheoremThe suffix maximum is attained#✓fully proved

For a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\), a gap score \(g \in \mathbb{Z}\) and sequences \(x\) and \(y\) over \(\alpha\), there is a suffix pair \((x', y')\) of \(x\) and \(y\), that is, a suffix \(x'\) of \(x\) and a suffix \(y'\) of \(y\), whose Needleman–Wunsch score equals the suffix maximum of \(x\) and \(y\).

theorem exists_nwScore_eq_suffixMax (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) :
    ∃ p ∈ suffixPairs xs ys, nwScore σ gap p.1 p.2 = suffixMax σ gap xs ys

Uses 5 · Used by 2

Statement usesNeedleman–Wunsch score · Suffix maximum of Needleman–Wunsch scores · Pairs of suffixes

Proof usesMaximum of an integer list with floor zero · Aligning the empty sequence with a sequence

Used byThe local score equals the Smith–Waterman score · The terminal cell is at most the suffix maximum

TheoremThe suffix maximum is nonnegative#✓fully proved

For every scoring function \(\sigma : \alpha \to \alpha \to \mathbb{Z}\), every gap score \(g \in \mathbb{Z}\) and all lists \(x\) and \(y\) over \(\alpha\), the suffix maximum of \(x\) and \(y\) (the largest Needleman–Wunsch score, under \(\sigma\) and \(g\), of a suffix of \(x\) against a suffix of \(y\)) is at least \(0\), since the pair of empty suffixes scores \(0\).

theorem zero_le_suffixMax (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) :
    0 ≤ suffixMax σ gap xs ys

Uses 3 · Used by 1

Statement usesSuffix maximum of Needleman–Wunsch scores

Proof usesSuffix pairs score at most the suffix maximum · Pairs of suffixes

Used byThe terminal cell is at most the suffix maximum

TheoremExtending an alignment by a letter of the first sequence#✓fully proved

If \(A\) is an alignment of sequences \(x\) and \(y\) and \(a\) is a letter, then \(A\) followed by the column with \(a\) in the first row and a gap in the second row is an alignment of \(x\) followed by \(a\) and of \(y\).

theorem isAlignment_append_some_none {A : Alignment α} {xs ys : List α} {a : α}
    (hA : IsAlignment A xs ys) :
    IsAlignment (A ++ [(some a, none)]) (xs ++ [a]) ys

Uses 2 · Used by 1

Statement usesAlignment · Valid alignment of two sequences

Used byAppending to the first sequence loses at most one gap

TheoremExtending an alignment by a letter of the second sequence#✓fully proved

If \(A\) is an alignment of sequences \(x\) and \(y\) and \(b\) is a letter, then \(A\) followed by the column with a gap in the first row and \(b\) in the second row is an alignment of \(x\) and of \(y\) followed by \(b\).

theorem isAlignment_append_none_some {A : Alignment α} {xs ys : List α} {b : α}
    (hA : IsAlignment A xs ys) :
    IsAlignment (A ++ [(none, some b)]) xs (ys ++ [b])

Uses 2 · Used by 1

Statement usesAlignment · Valid alignment of two sequences

Used byAppending to the second sequence loses at most one gap

TheoremAppending to the first sequence loses at most one gap#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score, \(g \in \mathbb{Z}\) a gap score, and write \(N(x, y)\) for the Needleman–Wunsch score of sequences \(x, y\) over \(\alpha\) with respect to \(\sigma\) and \(g\). For all sequences \(x, y\) and every letter \(a \in \alpha\), writing \(xa\) for \(x\) with \(a\) appended at the end, \(N(x, y) + g \le N(xa, y)\).

An optimal alignment of \(x\) and \(y\) followed by the gap column pairing \(a\) with nothing is an alignment of \(xa\) and \(y\).

theorem nwScore_le_nwScore_snoc_left (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) (a : α) :
    nwScore σ gap xs ys + gap ≤ nwScore σ gap (xs ++ [a]) ys

Uses 8 · Used by 1

Statement usesNeedleman–Wunsch score

Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch is optimal · Score of an alignment column · Needleman–Wunsch is attained · Extending an alignment by a letter of the first sequence

Used byThe terminal cell is at most the suffix maximum

TheoremAppending to the second sequence loses at most one gap#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score, \(g \in \mathbb{Z}\) a gap score, and write \(N(x, y)\) for the Needleman–Wunsch score of sequences \(x, y\) over \(\alpha\) with respect to \(\sigma\) and \(g\). For all sequences \(x, y\) and every letter \(b \in \alpha\), writing \(yb\) for \(y\) with \(b\) appended at the end, \(N(x, y) + g \le N(x, yb)\).

An optimal alignment of \(x\) and \(y\) followed by the gap column pairing nothing with \(b\) is an alignment of \(x\) and \(yb\).

theorem nwScore_le_nwScore_snoc_right (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) (b : α) :
    nwScore σ gap xs ys + gap ≤ nwScore σ gap xs (ys ++ [b])

Uses 8 · Used by 1

Statement usesNeedleman–Wunsch score

Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch is optimal · Score of an alignment column · Needleman–Wunsch is attained · Extending an alignment by a letter of the second sequence

Used byThe terminal cell is at most the suffix maximum

TheoremSuffix pairs score at most the terminal Smith–Waterman cell#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \le 0\) a gap score. If \(x'\) is a suffix of a sequence \(x\) and \(y'\) is a suffix of a sequence \(y\) over \(\alpha\), then the Needleman–Wunsch score of \(x'\) and \(y'\) is at most the terminal Smith–Waterman cell score of \(x\) and \(y\), both with respect to \(\sigma\) and \(g\).

theorem nwScore_le_swCellScore_of_suffix (hgap : gap ≤ 0) {xs' ys' xs ys : List α}
    (hxs : xs' <:+ xs) (hys : ys' <:+ ys) :
    nwScore σ gap xs' ys' ≤ swCellScore σ gap xs ys

Uses 9 · Used by 2

Statement usesNeedleman–Wunsch score · The terminal Smith–Waterman cell

Proof usesAligning the empty sequence with a sequence · Aligning a sequence with the empty sequence · The Needleman–Wunsch recurrence, end-peeling · Appending an element preserves suffixes · Suffixes of a list with an element appended · The Smith–Waterman recurrence · The terminal Smith–Waterman cell is nonnegative

Used byThe local score equals the Smith–Waterman score · The suffix maximum is at most the terminal Smith–Waterman cell

TheoremThe terminal cell is at most the suffix maximum#✓fully proved

For every substitution score \(\sigma\), every gap score \(g\) of either sign and all sequences \(x\) and \(y\), the terminal Smith–Waterman cell \(H(x, y)\) is at most the maximum Needleman–Wunsch score over all pairs of a suffix of \(x\) and a suffix of \(y\).

Only the reverse inequality needs \(g \le 0\).

theorem swCellScore_le_suffixMax (xs ys : List α) :
    swCellScore σ gap xs ys ≤ suffixMax σ gap xs ys

Uses 14 · Used by 1

Statement usesSuffix maximum of Needleman–Wunsch scores · The terminal Smith–Waterman cell

Proof usesThe suffix maximum is attained · Needleman–Wunsch score · Appending to the first sequence loses at most one gap · Appending to the second sequence loses at most one gap · Suffix pairs score at most the suffix maximum · The Needleman–Wunsch recurrence, end-peeling · Pairs of suffixes · Appending an element preserves suffixes · The Smith–Waterman recurrence · The terminal cell vanishes when the first sequence is empty · The terminal cell vanishes when the second sequence is empty · The suffix maximum is nonnegative

Used byFor nonpositive gaps, the terminal Smith–Waterman cell is the best suffix-pair score

TheoremThe suffix maximum is at most the terminal Smith–Waterman cell#✓fully proved

Let \(\sigma\) be a substitution score and \(g \le 0\) an integer gap score. For all lists \(xs\) and \(ys\), the maximum Needleman–Wunsch score over all pairs of a suffix of \(xs\) and a suffix of \(ys\) is at most the terminal Smith–Waterman cell score of \(xs\) and \(ys\).

theorem suffixMax_le_swCellScore (hgap : gap ≤ 0) (xs ys : List α) :
    suffixMax σ gap xs ys ≤ swCellScore σ gap xs ys

Uses 5 · Used by 1

Statement usesSuffix maximum of Needleman–Wunsch scores · The terminal Smith–Waterman cell

Proof usesSuffix pairs score at most the terminal Smith–Waterman cell · Upper bounds on the suffix maximum · Pairs of suffixes

Used byFor nonpositive gaps, the terminal Smith–Waterman cell is the best suffix-pair score

TheoremFor nonpositive gaps, the terminal Smith–Waterman cell is the best suffix-pair score#✓fully proved

For a substitution score \(\sigma\), a gap score \(g \le 0\) and all sequences \(x\) and \(y\), the terminal Smith–Waterman cell \(H(x, y)\) equals the maximum Needleman–Wunsch score over all pairs of a suffix of \(x\) and a suffix of \(y\) (the empty suffixes included).

theorem swCellScore_eq_suffixMax (hgap : gap ≤ 0) (xs ys : List α) :
    swCellScore σ gap xs ys = suffixMax σ gap xs ys

Uses 4 · Used by 1

Statement usesSuffix maximum of Needleman–Wunsch scores · The terminal Smith–Waterman cell

Proof usesThe suffix maximum is at most the terminal Smith–Waterman cell · The terminal cell is at most the suffix maximum

Used byThe local score equals the Smith–Waterman score

DefinitionPairs of prefixes#✓fully proved

For lists \(xs\) and \(ys\), the list of all pairs \((p, q)\) where \(p\) is a prefix of \(xs\) and \(q\) is a prefix of \(ys\), the empty lists and \(xs\), \(ys\) themselves included.

def prefixPairs (xs ys : List α) : List (List α × List α) :=
  xs.inits.product ys.inits

Used by 9

Used byInfix pairs · The local score equals the Smith–Waterman score · Upper bounds on the local score · Each prefix-pair cell is at most the Smith–Waterman score · The Smith–Waterman score · Bounding the Smith–Waterman score by its cells · The fitting score is at most the local score · The overlap score is at most the local score · The table computes the Smith–Waterman score

DefinitionInfix pairs#✓fully proved

For sequences \(x\) and \(y\) over \(\alpha\), the list of infix pairs of \(x\) and \(y\) is obtained by going through each prefix \(p\) of \(x\) and each prefix \(q\) of \(y\) and, for each such \((p, q)\), listing all pairs \((x', y')\) of a suffix \(x'\) of \(p\) and a suffix \(y'\) of \(q\).

So \((x', y')\) occurs in the list exactly when \(x'\) is a contiguous block of \(x\) and \(y'\) is a contiguous block of \(y\); a pair may occur more than once.

def infixPairs (xs ys : List α) : List (List α × List α) :=
  (prefixPairs xs ys).flatMap (fun p => p.1.tails.product p.2.tails)

Uses 1 · Used by 6

Statement usesPairs of prefixes

Used byLocal alignment score · The local score equals the Smith–Waterman score · Upper bounds on the local score · Infix pairs score at most the local score · The fitting score is at most the local score · The overlap score is at most the local score

DefinitionLocal alignment score#✓fully proved

For an integer substitution score \(\sigma\), an integer gap score \(g\) and sequences \(x\) and \(y\), the local score of \(x\) and \(y\) is the maximum of the Needleman–Wunsch score of \((x', y')\) over all pairs of an infix \(x'\) of \(x\) and an infix \(y'\) of \(y\) (contiguous and possibly empty).

def localScore (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) : ℤ :=
  listMax ((infixPairs xs ys).map (fun p => nwScore σ gap p.1 p.2))

Uses 3 · Used by 6

Statement usesInfix pairs · Maximum of an integer list with floor zero · Needleman–Wunsch score

Used byThe local score equals the Smith–Waterman score · Upper bounds on the local score · Infix pairs score at most the local score · The fitting score is at most the local score · The overlap score is at most the local score · The table computes the optimal local alignment score

TheoremInfix pairs score at most the local score#✓fully proved

Let \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) be a substitution score and \(g \in \mathbb{Z}\) a gap score. If \((x', y')\) is an infix pair of sequences \(x\) and \(y\) over \(\alpha\), that is, \(x'\) is a suffix of a prefix of \(x\) and \(y'\) is a suffix of a prefix of \(y\), then the Needleman–Wunsch score of \(x'\) and \(y'\) is at most the local score of \(x\) and \(y\), both with respect to \(\sigma\) and \(g\).

theorem nwScore_le_localScore {xs' ys' xs ys : List α}
    (h : (xs', ys') ∈ infixPairs xs ys) :
    nwScore σ gap xs' ys' ≤ localScore σ gap xs ys

Uses 4 · Used by 3

Statement usesInfix pairs · Local alignment score · Needleman–Wunsch score

Proof usesMaximum of an integer list with floor zero

Used byThe local score equals the Smith–Waterman score · The fitting score is at most the local score · The overlap score is at most the local score

TheoremUpper bounds on the local score#✓fully proved

Let \(\sigma\) be an integer substitution score, \(g\) an integer gap score, \(x\) and \(y\) sequences and \(c\) an integer. If the Needleman–Wunsch score of every pair \((x', y')\) with \(x'\) an infix of \(x\) and \(y'\) an infix of \(y\) is at most \(c\), then the local score of \(x\) and \(y\) is at most \(c\).

theorem localScore_le {xs ys : List α} {y : ℤ}
    (h : ∀ p ∈ infixPairs xs ys, nwScore σ gap p.1 p.2 ≤ y) :
    localScore σ gap xs ys ≤ y

Uses 6 · Used by 1

Statement usesInfix pairs · Local alignment score · Needleman–Wunsch score

Proof usesMaximum of an integer list with floor zero · Aligning the empty sequence with a sequence · Pairs of prefixes

Used byThe local score equals the Smith–Waterman score

DefinitionThe Smith–Waterman score#✓fully proved

Given a substitution score \(\sigma\) and a gap score \(g\), the Smith–Waterman score of two sequences \(x\) and \(y\) is the maximum of the terminal Smith–Waterman cell \(H(p, q)\) over all pairs of a prefix \(p\) of \(x\) and a prefix \(q\) of \(y\) (the empty prefixes included).

For \(g \le 0\) this is the optimal local alignment score, the maximum Needleman–Wunsch score over pairs of infixes; for \(g > 0\) it can be smaller.

def swScore (σ : α → α → ℤ) (gap : ℤ) (xs ys : List α) : ℤ :=
  listMax ((prefixPairs xs ys).map (fun p => swCellScore σ gap p.1 p.2))

Uses 3 · Used by 5

Statement usesMaximum of an integer list with floor zero · Pairs of prefixes · The terminal Smith–Waterman cell

Used byThe local score equals the Smith–Waterman score · Each prefix-pair cell is at most the Smith–Waterman score · Bounding the Smith–Waterman score by its cells · The table computes the optimal local alignment score · The table computes the Smith–Waterman score

TheoremEach prefix-pair cell is at most the Smith–Waterman score#✓fully proved

For a substitution score \(\sigma\), a gap score \(g\), sequences \(x\) and \(y\), a prefix \(p\) of \(x\) and a prefix \(q\) of \(y\), the terminal Smith–Waterman cell \(H(p, q)\) is at most the Smith–Waterman score of \(x\) and \(y\).

theorem swCellScore_le_swScore {px py xs ys : List α}
    (h : (px, py) ∈ prefixPairs xs ys) :
    swCellScore σ gap px py ≤ swScore σ gap xs ys

Uses 4 · Used by 2

Statement usesPairs of prefixes · The terminal Smith–Waterman cell · The Smith–Waterman score

Proof usesMaximum of an integer list with floor zero

Used byThe local score equals the Smith–Waterman score · The table computes the Smith–Waterman score

TheoremBounding the Smith–Waterman score by its cells#✓fully proved

For a substitution score \(\sigma\), a gap score \(g\), sequences \(x\) and \(y\) and an integer \(c\), if the terminal Smith–Waterman cell \(H(p, q)\) is at most \(c\) for every prefix \(p\) of \(x\) and every prefix \(q\) of \(y\), then the Smith–Waterman score of \(x\) and \(y\) is at most \(c\).

theorem swScore_le {xs ys : List α} {y : ℤ}
    (h : ∀ p ∈ prefixPairs xs ys, swCellScore σ gap p.1 p.2 ≤ y) :
    swScore σ gap xs ys ≤ y

Uses 5 · Used by 2

Statement usesPairs of prefixes · The terminal Smith–Waterman cell · The Smith–Waterman score

Proof usesMaximum of an integer list with floor zero · The terminal cell vanishes when the first sequence is empty

Used byThe local score equals the Smith–Waterman score · The table computes the Smith–Waterman score

TheoremThe local score equals the Smith–Waterman score#✓fully proved

Let \(\sigma\) be an integer-valued substitution score on letters and let \(g\) be an integer gap score with \(g \le 0\). Then for all sequences \(x\) and \(y\), the local score of \(x\) and \(y\) (the maximum Needleman–Wunsch score over pairs of infixes) equals their Smith–Waterman score (the maximum terminal-cell score over pairs of prefixes).

The proof uses that an infix is a suffix of a prefix and that the terminal cell is a maximum over pairs of suffixes.

theorem localScore_eq_swScore (hgap : gap ≤ 0) (xs ys : List α) :
    localScore σ gap xs ys = swScore σ gap xs ys

Uses 15 · Used by 1

Statement usesLocal alignment score · The Smith–Waterman score

Proof usesThe suffix maximum is attained · Infix pairs · Upper bounds on the local score · Needleman–Wunsch score · Infix pairs score at most the local score · Suffix pairs score at most the terminal Smith–Waterman cell · Pairs of prefixes · Suffix maximum of Needleman–Wunsch scores · Pairs of suffixes · The terminal Smith–Waterman cell · For nonpositive gaps, the terminal Smith–Waterman cell is the best suffix-pair score · Each prefix-pair cell is at most the Smith–Waterman score · Bounding the Smith–Waterman score by its cells

Used byThe table computes the optimal local alignment score

DefinitionRemaining cells of a Needleman–Wunsch table row#✓fully proved

The cells F[i+1][j+1], F[i+1][j+2], … of a row from the remaining letters b :: ys of the second sequence, the remaining cells up :: prev of the previous row, the previous row's cell diag to the upper left and the cell left just computed. A previous row that is too short ends the row early (this does not happen for rows of the table, nextRow_eq).

def nextRowAux (a : α) : List α → List ℤ → ℤ → ℤ → List ℤ
  | [], _, _, _ => []
  | _ :: _, [], _, _ => []
  | b :: ys, up :: prev, diag, left =>
      max (max (diag + σ a b) (up + gap)) (left + gap) ::
        nextRowAux a ys prev up (max (max (diag + σ a b) (up + gap)) (left + gap))

Used by 2

Used byNext row of the Needleman–Wunsch table · One row of the table

DefinitionNext row of the Needleman–Wunsch table#✓fully proved

The row of the table for the prefix extended by a, from the previous row: the first cell is one more gap than the previous row's first cell, then the recurrence left to right.

def nextRow (a : α) (ys : List α) (prev : List ℤ) : List ℤ :=
  (prev.headD 0 + gap) :: nextRowAux σ gap a ys prev.tail (prev.headD 0) (prev.headD 0 + gap)

Uses 1 · Used by 3

Statement usesRemaining cells of a Needleman–Wunsch table row

Used byOne row of the table · Row-by-row filling of the Needleman–Wunsch table · The last row of the table

DefinitionRow-by-row filling of the Needleman–Wunsch table#✓fully proved

The rows of the table, filled top to bottom over the letters of the first sequence; the result is the last row. Row 0 is F[0][j] = j * gap.

def nwRowsAux (ys : List α) : List α → List ℤ → List ℤ
  | [], row => row
  | a :: xs, row => nwRowsAux ys xs (nextRow σ gap a ys row)

Uses 1 · Used by 2

Statement usesNext row of the Needleman–Wunsch table

Used byLast row of the Needleman–Wunsch table · The last row of the table

DefinitionLast row of the Needleman–Wunsch table#✓fully proved

The last row F[|xs|][·] of the Needleman–Wunsch table.

def nwRows (xs ys : List α) : List ℤ :=
  nwRowsAux σ gap ys xs ((List.range (ys.length + 1)).map fun j : ℕ => gap * (j : ℤ))

Uses 1 · Used by 3

Statement usesRow-by-row filling of the Needleman–Wunsch table

Used byThe last row of the table · The Needleman–Wunsch table · The table computes the optimal global alignment score

DefinitionThe Needleman–Wunsch table#✓fully proved

Its last cell F[|xs|][|ys|].

def nwTab (xs ys : List α) : ℤ :=
  (nwRows σ gap xs ys).getLastD 0

Uses 1 · Used by 1

Statement usesLast row of the Needleman–Wunsch table

Used byThe table computes the optimal global alignment score

TheoremOne row of the table#✓fully proved

From the row of the prefix px, nextRow computes the row of px ++ [a]: the cells nwScore (px ++ [a]) py for the prefixes py of ys, shortest first.

theorem nextRow_eq (a : α) (px ys : List α) :
    nextRow σ gap a ys (ys.inits.map (nwScore σ gap px)) =
      ys.inits.map (nwScore σ gap (px ++ [a]))

Uses 5 · Used by 1

Statement usesNeedleman–Wunsch score · Next row of the Needleman–Wunsch table

Proof usesAligning a sequence with the empty sequence · The Needleman–Wunsch recurrence, end-peeling · Remaining cells of a Needleman–Wunsch table row

Used byThe last row of the table

TheoremThe last row of the table#✓fully proved

The last row of the table is F[|xs|][j] = nwScore xs (ys.take j): the cells nwScore xs py over the prefixes py of ys, shortest first.

theorem nwRows_eq (xs ys : List α) :
    nwRows σ gap xs ys = ys.inits.map (nwScore σ gap xs)

Uses 6 · Used by 1

Statement usesNeedleman–Wunsch score · Last row of the Needleman–Wunsch table

Proof usesAligning the empty sequence with a sequence · Next row of the Needleman–Wunsch table · One row of the table · Row-by-row filling of the Needleman–Wunsch table

Used byThe table computes the optimal global alignment score

TheoremThe table computes the optimal global alignment score#✓fully proved

The table computes the optimal global alignment score (Needleman–Wunsch 1970), for every substitution score σ and gap score gap.

theorem nwTab_eq_nwScore (xs ys : List α) : nwTab σ gap xs ys = nwScore σ gap xs ys

Uses 4

Statement usesNeedleman–Wunsch score · The Needleman–Wunsch table

Proof usesLast row of the Needleman–Wunsch table · The last row of the table

59 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.