Multiple sequence alignment

AbbreviationMultiple alignments#✓fully proved

A multiple alignment with \(k\) rows over an alphabet \(\alpha\) is a finite list of columns, each of which assigns to every row \(i \in \{0, \dots, k-1\}\) either a letter of \(\alpha\) or a gap. No condition ties the rows to given sequences.

abbrev MSAlignment (k : ℕ) (α : Type*) := List (Fin k → Option α)

Used by 11

Used byScore of an induced pairwise alignment · Every family of sequences has a multiple 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 · Valid multiple alignment · Sum-of-pairs score · The SP score is the sum of the induced pairwise scores · The sum-of-pairs score is bounded by the pairwise optima

DefinitionValid multiple alignment#✓fully proved

A multiple alignment \(A\) of \(k\) rows is a valid multiple alignment of sequences \(s_0, \dots, s_{k-1}\) when no column of \(A\) consists only of gaps and, for every \(i < k\), deleting the gaps from row \(i\) of \(A\) gives \(s_i\).

def IsMSAlignment {k : ℕ} (seqs : Fin k → List α) (A : MSAlignment k α) : Prop :=
  (∀ col ∈ A, ∃ i, col i ≠ none) ∧
    ∀ i, (A.map fun col => col i).filterMap id = seqs i

Uses 1 · Used by 3

Statement usesMultiple alignments

Used byEvery family of sequences has a multiple alignment · Induced pairwise alignments are valid · The sum-of-pairs score is bounded by the pairwise optima

DefinitionInduced pairwise alignment#✓fully proved

Given a multiple alignment \(A\) of \(k\) sequences and rows \(i, j < k\), the pairwise alignment induced by \(A\) on rows \(i\) and \(j\) is obtained by keeping, for each column \(c\) of \(A\) in order, the pair \((c_i, c_j)\), and dropping the columns in which both \(c_i\) and \(c_j\) are gaps.

def inducedPair {k : ℕ} (A : MSAlignment k α) (i j : Fin k) : Alignment α :=
  A.filterMap (fun col =>
    if (col i).isSome || (col j).isSome then some (col i, col j) else none)

Uses 2 · Used by 7

Statement usesAlignment · Multiple alignments

Used byScore of an 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 · The SP score is the sum of the induced pairwise scores · The sum-of-pairs score is bounded by the pairwise optima

TheoremInduced alignments have no all-gap column#✓fully proved

For a multiple alignment \(A\) of \(k\) sequences and rows \(i, j < k\), no column of the pairwise alignment induced by \(A\) on rows \(i\) and \(j\) is a gap in both rows.

theorem inducedPair_ne_none_none {k : ℕ} {A : MSAlignment k α} {i j : Fin k}
    {c : Option α × Option α} (hc : c ∈ inducedPair A i j) :
    c ≠ (none, none)

Uses 3 · Used by 1

Statement usesAlignment · Multiple alignments · Induced pairwise alignment

Used byInduced pairwise alignments are valid

TheoremLetters of the first row of an induced alignment#✓fully proved

For a multiple alignment \(A\) of \(k\) sequences and rows \(i, j < k\), deleting the gaps from the first row of the pairwise alignment induced by \(A\) on rows \(i\) and \(j\) gives the same sequence as deleting the gaps from row \(i\) of \(A\).

theorem inducedPair_filterMap_fst {k : ℕ} {A : MSAlignment k α} {i j : Fin k} :
    (inducedPair A i j).filterMap Prod.fst =
      (A.map fun col => col i).filterMap id

Uses 3 · Used by 1

Statement usesMultiple alignments · Induced pairwise alignment

Proof usesAlignment

Used byInduced pairwise alignments are valid

TheoremLetters of the second row of an induced alignment#✓fully proved

For a multiple alignment \(A\) of \(k\) sequences and rows \(i, j < k\), deleting the gaps from the second row of the pairwise alignment induced by \(A\) on rows \(i\) and \(j\) gives the same sequence as deleting the gaps from row \(j\) of \(A\).

theorem inducedPair_filterMap_snd {k : ℕ} {A : MSAlignment k α} {i j : Fin k} :
    (inducedPair A i j).filterMap Prod.snd =
      (A.map fun col => col j).filterMap id

Uses 3 · Used by 1

Statement usesMultiple alignments · Induced pairwise alignment

Proof usesAlignment

Used byInduced pairwise alignments are valid

TheoremInduced pairwise alignments are valid#✓fully proved

Let \(A\) be a valid multiple alignment of sequences \(s_0, \dots, s_{k-1}\). Then for all rows \(i, j < k\), the pairwise alignment induced by \(A\) on rows \(i\) and \(j\) is a valid pairwise alignment of \(s_i\) and \(s_j\).

theorem inducedPair_isAlignment {k : ℕ} {seqs : Fin k → List α}
    {A : MSAlignment k α} (hA : IsMSAlignment seqs A) (i j : Fin k) :
    IsAlignment (inducedPair A i j) (seqs i) (seqs j)

Uses 8 · Used by 1

Statement usesValid alignment of two sequences · Valid multiple alignment · Multiple alignments · Induced pairwise alignment

Proof usesAlignment · Letters of the first row of an induced alignment · Letters of the second row of an induced alignment · Induced alignments have no all-gap column

Used byThe sum-of-pairs score is bounded by the pairwise optima

DefinitionPairs of rows#✓fully proved

For \(k \in \mathbb{N}\), the finite set of all pairs \((i, j)\) with \(i, j \in \{0, \dots, k-1\}\) and \(i < j\), so that each unordered pair of distinct rows appears exactly once.

def pairFinset (k : ℕ) : Finset (Fin k × Fin k) :=
  Finset.univ.filter (fun p => p.1 < p.2)

Used by 3

Used bySum-of-pairs score of a column · The SP score is the sum of the induced pairwise scores · The sum-of-pairs score is bounded by the pairwise optima

DefinitionSum-of-pairs score of a column#✓fully proved

Let \(\sigma\) assign an integer score to each pair of letters and let \(g\) be an integer gap score. For a column \(c\) of a multiple alignment of \(k\) sequences, which gives each row \(r < k\) either a letter or a gap \(c_r\), the sum-of-pairs score of \(c\) is \(\sum_{i < j < k} s(c_i, c_j)\), where \(s\) is the pairwise column score: \(\sigma(a, b)\) for letters \(a\) and \(b\), \(g\) for a letter against a gap, and \(0\) for two gaps.

def columnSP {k : ℕ} (col : Fin k → Option α) : ℤ :=
  ∑ p ∈ pairFinset k, columnScore σ gap (col p.1, col p.2)

Uses 2 · Used by 1

Statement usesScore of an alignment column · Pairs of rows

Used bySum-of-pairs score

DefinitionSum-of-pairs score#✓fully proved

Fix a score \(\sigma(a, b) \in \mathbb{Z}\) for each pair of letters \(a, b\) and a gap score \(g \in \mathbb{Z}\). For two entries \(x, y\), each a letter or a gap, let \(s(x, y) = \sigma(x, y)\) if both are letters, \(s(x, y) = g\) if exactly one is a gap, and \(s(x, y) = 0\) if both are gaps. The sum-of-pairs score of a multiple alignment \(A\) of \(k\) sequences is the sum, over the columns \(c\) of \(A\), of \(\sum_{0 \le i < j < k} s(c_i, c_j)\), where \(c_i\) is the entry of \(c\) in row \(i\).

def msaScore {k : ℕ} (A : MSAlignment k α) : ℤ :=
  (A.map (fun col => columnSP σ gap col)).sum

Uses 2 · Used by 2

Statement usesMultiple alignments · Sum-of-pairs score of a column

Used byThe SP score is the sum of the induced pairwise scores · The sum-of-pairs score is bounded by the pairwise optima

TheoremScore of an induced pairwise alignment#✓fully proved

Let \(\sigma\) assign an integer score to each pair of letters and let \(g\) be an integer gap score. For a multiple alignment \(A\) of \(k\) sequences and rows \(i, j < k\), the score (with respect to \(\sigma\) and \(g\)) of the pairwise alignment induced by \(A\) on rows \(i\) and \(j\) equals the sum, over all columns \(c\) of \(A\), of the column score of the pair \((c_i, c_j)\).

theorem alignmentScore_inducedPair {k : ℕ} {A : MSAlignment k α} (i j : Fin k) :
    alignmentScore σ gap (inducedPair A i j) =
      (A.map (fun col => columnScore σ gap (col i, col j))).sum

Uses 5 · Used by 1

Statement usesMultiple alignments · Score of an alignment · Score of an alignment column · Induced pairwise alignment

Proof usesAlignment

Used byThe SP score is the sum of the induced pairwise scores

TheoremThe SP score is the sum of the induced pairwise scores#✓fully proved

Let \(\sigma\) assign an integer score to each pair of letters and let \(g\) be an integer gap score. For every multiple alignment \(A\) of \(k\) sequences, the sum-of-pairs score of \(A\) equals the sum, over all pairs of rows \(i < j < k\), of the score of the pairwise alignment induced by \(A\) on rows \(i\) and \(j\).

theorem msaScore_eq_sum_induced {k : ℕ} {A : MSAlignment k α} :
    msaScore σ gap A =
      ∑ p ∈ pairFinset k, alignmentScore σ gap (inducedPair A p.1 p.2)

Uses 7 · Used by 1

Statement usesMultiple alignments · Score of an alignment · Induced pairwise alignment · Sum-of-pairs score · Pairs of rows

Proof usesScore of an induced pairwise alignment · Score of an alignment column

Used byThe sum-of-pairs score is bounded by the pairwise optima

TheoremThe sum-of-pairs score is bounded by the pairwise optima#✓fully proved

Fix a score \(\sigma(a, b) \in \mathbb{Z}\) for each pair of letters \(a, b\) of an alphabet \(\alpha\) and a gap score \(g \in \mathbb{Z}\). Let \(s_0, \dots, s_{k-1}\) be sequences over \(\alpha\) and let \(A\) be a valid multiple alignment of them: no column of \(A\) consists only of gaps, and deleting the gaps from row \(i\) of \(A\) leaves \(s_i\). Then the sum-of-pairs score of \(A\) under \(\sigma\) and \(g\) is at most \(\sum_{0 \le i < j < k} \mathrm{NW}(s_i, s_j)\), where \(\mathrm{NW}(s_i, s_j)\) is the optimal global (Needleman–Wunsch) alignment score of \(s_i\) and \(s_j\) under \(\sigma\) and \(g\).

theorem msaScore_le_sum_nwScore {k : ℕ} {seqs : Fin k → List α}
    {A : MSAlignment k α} (hA : IsMSAlignment seqs A) :
    msaScore σ gap A ≤
      ∑ p ∈ pairFinset k, nwScore σ gap (seqs p.1) (seqs p.2)

Uses 10

Statement usesValid multiple alignment · Multiple alignments · Sum-of-pairs score · Needleman–Wunsch score · Pairs of rows

Proof usesScore of an alignment · Needleman–Wunsch is optimal · Induced pairwise alignment · Induced pairwise alignments are valid · The SP score is the sum of the induced pairwise scores

TheoremEvery family of sequences has a multiple alignment#✓fully proved

For every natural number \(n\) and every family of \(k\) sequences \(s_0, \dots, s_{k-1}\) whose lengths sum to at most \(n\), there is a valid multiple alignment of \(s_0, \dots, s_{k-1}\).

The bound \(n\) is the parameter of the induction in the proof, which removes the first letter of one nonempty sequence; taking \(n\) to be the total length shows that every finite family of sequences has a valid multiple alignment.

theorem exists_isMSAlignment : ∀ (n : ℕ) {k : ℕ} (seqs : Fin k → List α),
    (∑ i, (seqs i).length) ≤ n → ∃ A, IsMSAlignment seqs A

Uses 2

Statement usesValid multiple alignment · Multiple alignments

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.