Banded sequence alignment

DefinitionBand check from a starting offset#✓fully proved

Let \(w \in \mathbb{N}\) be a band width. For natural numbers \(i\), \(j\) and an alignment \(A\), the band check of \(A\) with width \(w\) from offset \((i, j)\) is true exactly when every prefix \(P\) of \(A\) (including the empty prefix and \(A\) itself) satisfies \(|(i + p) - (j + q)| \le w\), where \(p\) and \(q\) are the numbers of columns of \(P\) whose first, respectively second, entry is present.

def bandedFrom : ℕ → ℕ → Alignment α → Bool
  | i, j, [] => decide (|(i : ℤ) - (j : ℤ)| ≤ (w : ℤ))
  | i, j, (some _, some _) :: A =>
      decide (|(i : ℤ) - (j : ℤ)| ≤ (w : ℤ)) && bandedFrom (i + 1) (j + 1) A
  | i, j, (some _, none) :: A =>
      decide (|(i : ℤ) - (j : ℤ)| ≤ (w : ℤ)) && bandedFrom (i + 1) j A
  | i, j, (none, some _) :: A =>
      decide (|(i : ℤ) - (j : ℤ)| ≤ (w : ℤ)) && bandedFrom i (j + 1) A
  | i, j, (none, none) :: A =>
      decide (|(i : ℤ) - (j : ℤ)| ≤ (w : ℤ)) && bandedFrom i j A

Uses 1 · Used by 11

Statement usesAlignment

Used byThe diagonal alignment stays in the band · A passing band check bounds the final offset · Columns using only the first sequence stay in the band · Columns using only the second sequence stay in the band · 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 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 · Banded alignments

DefinitionBanded alignments#✓fully proved

Let \(w \in \mathbb{N}\). An alignment \(A\) is banded with width \(w\) when, for every prefix of \(A\) (including the empty prefix and \(A\) itself), the number of columns of that prefix with a letter in the first row and the number with a letter in the second row differ by at most \(w\).

def IsBanded (A : Alignment α) : Prop := bandedFrom w 0 0 A = true

Uses 2 · Used by 6

Statement usesAlignment · Band check from a starting offset

Used byBanded alignment is exact when some optimal alignment is banded · The banded optimum is exact · The diagonal alignment is banded · Banded alignments force close lengths · An alignment with at most w gap columns is w-banded · The band lemma

TheoremBound at an intermediate point, difference form#✓fully proved

For integers \(a\), \(d\), \(t\) and \(w\), if \(|a| \le w\), \(|a - d| \le w\) and \(0 \le t \le d\), then \(|a - t| \le w\).

Used for the gap phases of an alignment, where the offset difference interpolates between its start and end values.

theorem abs_le_of_between {a d t w : ℤ} (h0 : |a| ≤ w) (hd : |a - d| ≤ w)
    (ht0 : 0 ≤ t) (htd : t ≤ d) : |a - t| ≤ w

Used by 1

Used byColumns using only the second sequence stay in the band

TheoremBound at an intermediate point, sum form#✓fully proved

For integers \(a\), \(d\), \(t\) and \(w\), if \(|a| \le w\), \(|a + d| \le w\) and \(0 \le t \le d\), then \(|a + t| \le w\).

Used for runs of alignment columns that consume only letters of the first sequence, where the offset difference grows.

theorem abs_le_of_between_add {a d t w : ℤ} (h0 : |a| ≤ w) (hd : |a + d| ≤ w)
    (ht0 : 0 ≤ t) (htd : t ≤ d) : |a + t| ≤ w

Used by 1

Used byColumns using only the first sequence stay in the band

TheoremA passing band check bounds the final offset#✓fully proved

Let \(w, i, j \in \mathbb{N}\) and let \(A\) be an alignment. If the band check of \(A\) with width \(w\) from offset \((i, j)\) is true, then \(|(i + p) - (j + q)| \le w\), where \(p\) and \(q\) are the numbers of columns of \(A\) whose first, respectively second, entry is present.

theorem bandedFrom_final : ∀ (A : Alignment α) (i j : ℕ),
    bandedFrom w i j A = true →

Uses 2 · Used by 1

Statement usesAlignment · Band check from a starting offset

Used byBanded alignments force close lengths

TheoremBanded alignments force close lengths#✓fully proved

Let \(w \in \mathbb{N}\). If \(A\) is a valid alignment of sequences \(x\) and \(y\) and \(A\) is banded with width \(w\), then the lengths of \(x\) and \(y\) differ by at most \(w\), that is \(\bigl| |x| - |y| \bigr| \le w\).

theorem isBanded_length_diff {A : Alignment α} {xs ys : List α}
    (hA : IsAlignment A xs ys) (hb : IsBanded w A) :
    |(xs.length : ℤ) - (ys.length : ℤ)| ≤ (w : ℤ)

Uses 4 · Used by 1

Statement usesAlignment · Valid alignment of two sequences · Banded alignments

Proof usesA passing band check bounds the final offset

Used byNo banded score when the lengths differ by more than the band width

DefinitionDiagonal alignment#✓fully proved

For sequences \(x = x_1 \dots x_m\) and \(y = y_1 \dots y_n\), let \(k = \min(m, n)\). The diagonal alignment of \(x\) and \(y\) consists of the columns \((x_1, y_1), \dots, (x_k, y_k)\), which pair letters by position whether or not they are equal, followed by one column for each remaining letter of the longer sequence, in order, pairing that letter with a gap.

def diagAlign : List α → List α → Alignment α
  | [], ys => ys.map (fun b => (none, some b))
  | a :: xs, [] => (a :: xs).map (fun a => (some a, none))
  | a :: xs, b :: ys => (some a, some b) :: diagAlign xs ys

Uses 1 · Used by 4

Statement usesAlignment

Used byThe diagonal alignment stays in the band · The banded score is defined when the lengths are close · The diagonal alignment is a valid alignment · The diagonal alignment is banded

TheoremThe diagonal alignment is a valid alignment#✓fully proved

For all sequences \(x\) and \(y\), the diagonal alignment of \(x\) and \(y\) is a valid alignment of \(x\) and \(y\): none of its columns consists of two gaps, and deleting the gaps from its first and second rows gives \(x\) and \(y\) respectively.

theorem isAlignment_diagAlign (xs ys : List α) :
    IsAlignment (diagAlign xs ys) xs ys

Uses 3 · Used by 1

Statement usesValid alignment of two sequences · Diagonal alignment

Proof usesAlignment

Used byThe banded score is defined when the lengths are close

TheoremColumns using only the second sequence stay in the band#✓fully proved

Let \(w, i, j \in \mathbb{N}\), let \(y\) be a list of length \(n\), and let \(A\) be the alignment with one column for each element \(b\) of \(y\), in order, with empty first entry and second entry \(b\). If \(|i - j| \le w\) and \(|i - (j + n)| \le w\), then the band check of \(A\) with width \(w\) from offset \((i, j)\) is true.

theorem bandedFrom_map_gapY : ∀ (ys : List α) (i j : ℕ),

Uses 2 · Used by 1

Statement usesBand check from a starting offset

Proof usesBound at an intermediate point, difference form

Used byThe diagonal alignment stays in the band

TheoremColumns using only the first sequence stay in the band#✓fully proved

Let \(w, i, j \in \mathbb{N}\), let \(x\) be a list of length \(n\), and let \(A\) be the alignment with one column for each element \(a\) of \(x\), in order, with first entry \(a\) and empty second entry. If \(|i - j| \le w\) and \(|(i + n) - j| \le w\), then the band check of \(A\) with width \(w\) from offset \((i, j)\) is true.

theorem bandedFrom_map_gapX : ∀ (xs : List α) (i j : ℕ),

Uses 2 · Used by 1

Statement usesBand check from a starting offset

Proof usesBound at an intermediate point, sum form

Used byThe diagonal alignment stays in the band

TheoremThe diagonal alignment stays in the band#✓fully proved

Let \(w, i, j \in \mathbb{N}\) and let \(x\), \(y\) be lists of lengths \(m\) and \(n\). If \(|i - j| \le w\) and \(|(i + m) - (j + n)| \le w\), then the band check of the diagonal alignment of \(x\) and \(y\) with width \(w\) from offset \((i, j)\) is true.

The match phase keeps the offset difference and the gap phases interpolate it.

theorem bandedFrom_diagAlign : ∀ (i j : ℕ) (xs ys : List α),

Uses 4 · Used by 1

Statement usesBand check from a starting offset · Diagonal alignment

Proof usesColumns using only the first sequence stay in the band · Columns using only the second sequence stay in the band

Used byThe diagonal alignment is banded

TheoremThe diagonal alignment is banded#✓fully proved

Let \(w \in \mathbb{N}\). If two sequences \(x\) and \(y\) have lengths differing by at most \(w\), that is \(\bigl| |x| - |y| \bigr| \le w\), then the diagonal alignment of \(x\) and \(y\) is banded with width \(w\).

theorem isBanded_diagAlign {xs ys : List α}
    (h : |(xs.length : ℤ) - (ys.length : ℤ)| ≤ (w : ℤ)) :
    IsBanded w (diagAlign xs ys)

Uses 3 · Used by 1

Statement usesBanded alignments · Diagonal alignment

Proof usesThe diagonal alignment stays in the band

Used byThe banded score is defined when the lengths are close

DefinitionBanded alignment score#✓fully proved

Fix a substitution score \(\sigma\), assigning an integer \(\sigma(a, b)\) to each pair of letters \(a\), \(b\), an integer gap score \(g\) and a band width \(w \in \mathbb{N}\). The banded alignment score of two sequences \(x\) and \(y\) is the maximum, over all valid alignments of \(x\) and \(y\) that are banded with width \(w\), of the (integer) alignment score with respect to \(\sigma\) and \(g\). It has no value (it is the empty optional value) when no such alignment exists.

def bandedScore (xs ys : List α) : Option ℤ :=
  List.argmax id (((alignments xs ys).filter (fun A => bandedFrom w 0 0 A)).map
    (alignmentScore σ gap))

Uses 4 · Used by 5

Statement usesAlignment · Score of an alignment · The list of all alignments · Band check from a starting offset

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

TheoremThe banded score is at most the Needleman–Wunsch score#✓fully proved

Let \(\sigma\) be an integer substitution score on an alphabet, \(g\) an integer gap score and \(w \in \mathbb{N}\) a band width. For sequences \(x\) and \(y\) over the alphabet and an integer \(s\), if the banded score of \(x\) and \(y\) (under \(\sigma\), \(g\) and width \(w\)) is defined and equals \(s\), then \(s\) is at most the Needleman–Wunsch score of \(x\) and \(y\).

theorem bandedScore_le_nwScore {xs ys : List α} {s : ℤ}
    (h : bandedScore σ gap w xs ys = some s) : s ≤ nwScore σ gap xs ys

Uses 9 · Used by 1

Statement usesBanded alignment score · Needleman–Wunsch score

Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch is optimal · The list of all alignments · Band check from a starting offset · The enumerated alignments are exactly the valid ones

Used byBanded alignment is exact when some optimal alignment is banded

TheoremBanded alignment is exact when some optimal alignment is banded#✓fully proved

Let \(\sigma\) be an integer substitution score on an alphabet, \(g\) an integer gap score and \(w \in \mathbb{N}\) a band width. For sequences \(x\) and \(y\) over the alphabet, if some alignment of \(x\) and \(y\) is banded with width \(w\) and has score (under \(\sigma\) and \(g\)) equal to the Needleman–Wunsch score of \(x\) and \(y\), then the banded score of \(x\) and \(y\) (under \(\sigma\), \(g\) and width \(w\)) is defined and equals their Needleman–Wunsch score.

theorem bandedScore_eq_nwScore_of_banded_optimal {xs ys : List α}
    (h : ∃ A, IsAlignment A xs ys ∧ IsBanded w A ∧
      alignmentScore σ gap A = nwScore σ gap xs ys) :
    bandedScore σ gap w xs ys = some (nwScore σ gap xs ys)

Uses 10 · Used by 1

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

Proof usesThe list of all alignments · Band check from a starting offset · The banded score is at most the Needleman–Wunsch score · The enumerated alignments are exactly the valid ones

Used byThe banded optimum is exact

TheoremNo banded score when the lengths differ by more than the band width#✓fully proved

Let \(\sigma\) be an integer substitution score on an alphabet, \(g\) an integer gap score and \(w \in \mathbb{N}\) a band width. For sequences \(x\) and \(y\) over the alphabet, of lengths \(m\) and \(n\), with \(w < |m - n|\), the banded score of \(x\) and \(y\) (under \(\sigma\), \(g\) and width \(w\)) is undefined: no alignment of \(x\) and \(y\) is banded with width \(w\).

theorem bandedScore_none_of_length_diff_gt {xs ys : List α}
    (h : (w : ℤ) < |(xs.length : ℤ) - (ys.length : ℤ)|) :
    bandedScore σ gap w xs ys = none

Uses 8

Statement usesBanded alignment score

Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · The list of all alignments · Band check from a starting offset · Banded alignments force close lengths · The enumerated alignments are exactly the valid ones

TheoremThe banded score is defined when the lengths are close#✓fully proved

Fix a substitution score \(\sigma\), assigning an integer \(\sigma(a, b)\) to each pair of letters \(a\), \(b\), an integer gap score \(g\) and a band width \(w \in \mathbb{N}\). If two sequences \(x\) and \(y\) have lengths differing by at most \(w\), that is \(\bigl| |x| - |y| \bigr| \le w\), then the banded alignment score of \(x\) and \(y\) (for \(\sigma\), \(g\) and \(w\)) is defined: it equals some integer \(s\).

theorem bandedScore_some_of_length_diff_le {xs ys : List α}
    (h : |(xs.length : ℤ) - (ys.length : ℤ)| ≤ (w : ℤ)) :
    ∃ s, bandedScore σ gap w xs ys = some s

Uses 10

Statement usesBanded alignment score

Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · The list of all alignments · Band check from a starting offset · Diagonal alignment · The diagonal alignment is a valid alignment · The diagonal alignment is banded · The enumerated alignments are exactly the valid ones

DefinitionNumber of gap columns of an alignment#✓fully proved

The number of gap columns of an alignment: columns with exactly one letter.

def gapColumns : Alignment α → ℕ
  | [] => 0
  | (some _, some _) :: A => gapColumns A
  | (some _, none) :: A => gapColumns A + 1
  | (none, some _) :: A => gapColumns A + 1
  | (none, none) :: A => gapColumns A

Uses 1 · Used by 4

Statement usesAlignment

Used byAlignment score is at most minus the number of gap columns · An alignment with few gap columns stays in the band from its start · An alignment with at most w gap columns is w-banded · The band lemma

TheoremAn alignment with few gap columns stays in the band from its start#✓fully proved

Along every prefix, the offset difference is at most the starting difference plus the number of gap columns: an alignment starting at (i, j) stays in the band of width w as soon as |i - j| + gapColumns A ≤ w.

theorem bandedFrom_of_abs_add_gapColumns_le (w : ℕ) :
    ∀ (A : Alignment α) (i j : ℕ),

Uses 3 · Used by 1

Statement usesAlignment · Band check from a starting offset · Number of gap columns of an alignment

Used byAn alignment with at most w gap columns is w-banded

TheoremAn alignment with at most w gap columns is w-banded#✓fully proved

An alignment with at most w gap columns is w-banded.

theorem isBanded_of_gapColumns_le {w : ℕ} {A : Alignment α} (h : gapColumns A ≤ w) :
    IsBanded w A

Uses 4 · Used by 1

Statement usesAlignment · Banded alignments · Number of gap columns of an alignment

Proof usesAn alignment with few gap columns stays in the band from its start

Used byThe band lemma

TheoremAlignment score is at most minus the number of gap columns#✓fully proved

With nonpositive substitution scores and gap score at most -1, an alignment scores at most minus its number of gap columns.

theorem alignmentScore_le_neg_gapColumns {σ : α → α → ℤ} {gap : ℤ}
    (hσ : ∀ a b, σ a b ≤ 0) (hgap : gap ≤ -1) :
    ∀ A : Alignment α, alignmentScore σ gap A ≤ -(gapColumns A : ℤ)

Uses 4 · Used by 1

Statement usesAlignment · Score of an alignment · Number of gap columns of an alignment

Proof usesScore of an alignment column

Used byThe band lemma

TheoremThe band lemma#✓fully proved

The band lemma (Ukkonen 1985): with nonpositive substitution scores and gap score at most -1, every alignment scoring at least -w (cost at most w) is w-banded.

theorem isBanded_of_neg_le_alignmentScore {σ : α → α → ℤ} {gap : ℤ}
    (hσ : ∀ a b, σ a b ≤ 0) (hgap : gap ≤ -1) {w : ℕ} {A : Alignment α}
    (h : -(w : ℤ) ≤ alignmentScore σ gap A) : IsBanded w A

Uses 6 · Used by 1

Statement usesAlignment · Banded alignments · Score of an alignment

Proof usesAlignment score is at most minus the number of gap columns · Number of gap columns of an alignment · An alignment with at most w gap columns is w-banded

Used byThe banded optimum is exact

TheoremThe banded optimum is exact#✓fully proved

The banded optimum is exact when the optimal score is at least -w (optimal cost at most w), for nonpositive substitution scores and gap score at most -1: some optimal alignment exists and, by the band lemma, it is w-banded.

theorem bandedScore_eq_nwScore_of_neg_le {σ : α → α → ℤ} {gap : ℤ}
    (hσ : ∀ a b, σ a b ≤ 0) (hgap : gap ≤ -1) {w : ℕ} {xs ys : List α}
    (h : -(w : ℤ) ≤ nwScore σ gap xs ys) :
    bandedScore σ gap w xs ys = some (nwScore σ gap xs ys)

Uses 9

Statement usesBanded alignment score · Needleman–Wunsch score

Proof usesAlignment · Valid alignment of two sequences · Banded alignments · Score of an alignment · Banded alignment is exact when some optimal alignment is banded · Needleman–Wunsch is attained · The band lemma

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.