Hirschberg's linear-space alignment

DefinitionArgmax over an initial segment#✓fully proved

For a function \(f : \mathbb{N} \to \mathbb{Z}\) and \(n \in \mathbb{N}\), the argmax of \(f\) over \(\{0, \dots, n\}\) is the least \(k \le n\) such that \(f(j) \le f(k)\) for all \(j \le n\).

It is computed as the first maximizer of \(f\) on the list \([0, 1, \dots, n]\), which is never empty.

def bestArgmax (f : ℕ → ℤ) (n : ℕ) : ℕ :=
  ((List.range (n + 1)).argmax f).getD 0

Used by 10

Used byHirschberg reconstruction with enough fuel attains the optimum · The argmax over \(\{0, \dots, n\}\) is at most \(n\) · The argmax over \(\{0, \dots, n\}\) maximizes the function there · 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

TheoremThe argmax over \(\{0, \dots, n\}\) is at most \(n\)#✓fully proved

For every function \(f : \mathbb{N} \to \mathbb{Z}\) and every \(n \in \mathbb{N}\), the argmax of \(f\) over \(\{0, \dots, n\}\) is at most \(n\).

theorem bestArgmax_le (f : ℕ → ℤ) (n : ℕ) : bestArgmax f n ≤ n

Uses 1 · Used by 2

Statement usesArgmax over an initial segment

Used byHirschberg reconstruction with enough fuel attains the optimum · Hirschberg reconstruction with enough fuel is valid

TheoremThe argmax over \(\{0, \dots, n\}\) maximizes the function there#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{Z}\), let \(n \in \mathbb{N}\) and let \(m\) be the argmax of \(f\) over \(\{0, \dots, n\}\). Then \(f(k) \le f(m)\) for every \(k \le n\).

theorem bestArgmax_spec (f : ℕ → ℤ) {n k : ℕ} (hk : k ≤ n) :
    f k ≤ f (bestArgmax f n)

Uses 1 · Used by 2

Statement usesArgmax over an initial segment

Used byHirschberg split identity, splitting the first sequence · Hirschberg split identity, splitting the second sequence

TheoremA split of the second sequence scores at most the Needleman–Wunsch optimum#✓fully proved

Let \(\sigma\) be an integer-valued substitution score on an alphabet, let \(g\) be an integer gap score, and write \(\mathrm{NW}(x, y)\) for the optimal Needleman–Wunsch global alignment score of sequences \(x\) and \(y\) under \(\sigma\) and \(g\). For sequences \(x\), \(y\) and natural numbers \(k\), \(m\), let \(x_{\lt k}\) be the first \(k\) letters of \(x\) (all of \(x\) if \(k\) is at least its length) and \(x_{\ge k}\) the remaining letters, and define \(y_{\lt m}\) and \(y_{\ge m}\) likewise. Then \(\mathrm{NW}(x_{\lt k}, y_{\lt m}) + \mathrm{NW}(x_{\ge k}, y_{\ge m}) \le \mathrm{NW}(x, y)\).

The bound holds because optimal alignments of the two halves concatenate to an alignment of \(x\) and \(y\).

theorem splitScore_le_nwScore_ys (xs ys : List α) {mid k : ℕ} :
    nwScore σ gap (List.take k xs) (List.take mid ys) +
      nwScore σ gap (List.drop k xs) (List.drop mid ys) ≤ nwScore σ gap xs ys

Uses 8 · Used by 2

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 · Concatenation of alignments

Used byEvery cut of the second list extends to an optimal split · Hirschberg split identity, splitting the second sequence

TheoremA split of the first sequence scores at most the Needleman–Wunsch optimum#✓fully proved

Let \(\sigma\) be an integer-valued substitution score on an alphabet, let \(g\) be an integer gap score, and write \(\mathrm{NW}(x, y)\) for the optimal Needleman–Wunsch global alignment score of sequences \(x\) and \(y\) under \(\sigma\) and \(g\). For sequences \(x\), \(y\) and natural numbers \(m\), \(k\), let \(x_{\lt m}\) be the first \(m\) letters of \(x\) (all of \(x\) if \(m\) is at least its length) and \(x_{\ge m}\) the remaining letters, and define \(y_{\lt k}\) and \(y_{\ge k}\) likewise. Then \(\mathrm{NW}(x_{\lt m}, y_{\lt k}) + \mathrm{NW}(x_{\ge m}, y_{\ge k}) \le \mathrm{NW}(x, y)\).

theorem splitScore_le_nwScore_xs (xs ys : List α) {mid k : ℕ} :
    nwScore σ gap (List.take mid xs) (List.take k ys) +
      nwScore σ gap (List.drop mid xs) (List.drop k ys) ≤ nwScore σ gap xs ys

Uses 8 · Used by 2

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 · Concatenation of alignments

Used byEvery cut of the first list extends to an optimal split · Hirschberg split identity, splitting the first sequence

TheoremEvery cut of the second list extends to an optimal split#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). Write \(S(u, v)\) for the Needleman–Wunsch score of lists \(u\), \(v\), and \(u_{\lt m}\) for the first \(m\) elements of \(u\) and \(u_{\ge m}\) for the rest. For all lists \(xs\), \(ys\) over \(\alpha\) and every \(m \le |ys|\), there is \(k \le |xs|\) with \(S(xs_{\lt k}, ys_{\lt m}) + S(xs_{\ge k}, ys_{\ge m}) = S(xs, ys)\).

theorem exists_split_eq_nwScore_ys (xs ys : List α) {mid : ℕ}
    (hmid : mid ≤ ys.length) :
    ∃ k ≤ xs.length, nwScore σ gap (List.take k xs) (List.take mid ys) +
      nwScore σ gap (List.drop k xs) (List.drop mid ys) = 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 · Score of an alignment column · Needleman–Wunsch is attained · A split of the second sequence scores at most the Needleman–Wunsch optimum

Used byHirschberg split identity, splitting the second sequence

TheoremEvery cut of the first list extends to an optimal split#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). Write \(S(u, v)\) for the Needleman–Wunsch score of lists \(u\), \(v\), and \(u_{\lt m}\) for the first \(m\) elements of \(u\) and \(u_{\ge m}\) for the rest. For all lists \(xs\), \(ys\) over \(\alpha\) and every \(m \le |xs|\), there is \(k \le |ys|\) with \(S(xs_{\lt m}, ys_{\lt k}) + S(xs_{\ge m}, ys_{\ge k}) = S(xs, ys)\).

theorem exists_split_eq_nwScore_xs (xs ys : List α) {mid : ℕ}
    (hmid : mid ≤ xs.length) :
    ∃ k ≤ ys.length, nwScore σ gap (List.take mid xs) (List.take k ys) +
      nwScore σ gap (List.drop mid xs) (List.drop k ys) = 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 · Score of an alignment column · Needleman–Wunsch is attained · A split of the first sequence scores at most the Needleman–Wunsch optimum

Used byHirschberg split identity, splitting the first sequence

TheoremHirschberg split identity, splitting the second sequence#✓fully proved

Fix a substitution score \(\sigma\) assigning an integer to each pair of letters and an integer gap score \(g\), and write \(\mathrm{NW}\) for the Needleman–Wunsch score. For a sequence \(s\), write \(s_{\lt j}\) for its first \(j\) letters and \(s_{\ge j}\) for the remaining letters. Let \(x\), \(y\) be sequences and \(m \le |y|\), and let \(k\) be the first index \(j \in \{0, \dots, |x|\}\) that maximizes \(\mathrm{NW}(x_{\lt j}, y_{\lt m}) + \mathrm{NW}(x_{\ge j}, y_{\ge m})\). Then \(\mathrm{NW}(x_{\lt k}, y_{\lt m}) + \mathrm{NW}(x_{\ge k}, y_{\ge m}) = \mathrm{NW}(x, y)\).

theorem nwScore_eq_bestSplit_ys (xs ys : List α) {mid : ℕ}
    (hmid : mid ≤ ys.length) :
    nwScore σ gap
        (List.take (bestArgmax (fun k => nwScore σ gap (List.take k xs)
          (List.take mid ys) + nwScore σ gap (List.drop k xs)
          (List.drop mid ys)) xs.length) xs) (List.take mid ys) +
      nwScore σ gap
        (List.drop (bestArgmax (fun k => nwScore σ gap (List.take k xs)
          (List.take mid ys) + nwScore σ gap (List.drop k xs)
          (List.drop mid ys)) xs.length) xs) (List.drop mid ys) =
    nwScore σ gap xs ys

Uses 5 · Used by 1

Statement usesArgmax over an initial segment · Needleman–Wunsch score

Proof usesThe argmax over \(\{0, \dots, n\}\) maximizes the function there · Every cut of the second list extends to an optimal split · A split of the second sequence scores at most the Needleman–Wunsch optimum

Used byHirschberg reconstruction with enough fuel attains the optimum

TheoremHirschberg split identity, splitting the first sequence#✓fully proved

Fix a substitution score \(\sigma\) assigning an integer to each pair of letters and an integer gap score \(g\), and write \(\mathrm{NW}\) for the Needleman–Wunsch score. For a sequence \(s\), write \(s_{\lt j}\) for its first \(j\) letters and \(s_{\ge j}\) for the remaining letters. Let \(x\), \(y\) be sequences and \(m \le |x|\), and let \(k\) be the first index \(j \in \{0, \dots, |y|\}\) that maximizes \(\mathrm{NW}(x_{\lt m}, y_{\lt j}) + \mathrm{NW}(x_{\ge m}, y_{\ge j})\). Then \(\mathrm{NW}(x_{\lt m}, y_{\lt k}) + \mathrm{NW}(x_{\ge m}, y_{\ge k}) = \mathrm{NW}(x, y)\).

theorem nwScore_eq_bestSplit_xs (xs ys : List α) {mid : ℕ}
    (hmid : mid ≤ xs.length) :
    nwScore σ gap (List.take mid xs)
        (List.take (bestArgmax (fun k => nwScore σ gap (List.take mid xs)
          (List.take k ys) + nwScore σ gap (List.drop mid xs)
          (List.drop k ys)) ys.length) ys) +
      nwScore σ gap (List.drop mid xs)
        (List.drop (bestArgmax (fun k => nwScore σ gap (List.take mid xs)
          (List.take k ys) + nwScore σ gap (List.drop mid xs)
          (List.drop k ys)) ys.length) ys) =
    nwScore σ gap xs ys

Uses 5 · Used by 1

Statement usesArgmax over an initial segment · Needleman–Wunsch score

Proof usesThe argmax over \(\{0, \dots, n\}\) maximizes the function there · Every cut of the first list extends to an optimal split · A split of the first sequence scores at most the Needleman–Wunsch optimum

Used byHirschberg reconstruction with enough fuel attains the optimum

TheoremNeedleman–Wunsch score of two single letters#✓fully proved

For every substitution score \(\sigma\) assigning an integer to each pair of letters, integer gap score \(g\) and letters \(a\), \(b\), the Needleman–Wunsch score of the one-letter sequences \([a]\) and \([b]\) is \(\max(\sigma(a, b), g + g)\): the better of matching \(a\) with \(b\) and gapping both.

theorem nwScore_singleton_singleton (a b : α) :
    nwScore σ gap [a] [b] = max (σ a b) (gap + gap)

Uses 4 · Used by 1

Statement usesNeedleman–Wunsch score

Proof usesThe Needleman–Wunsch recurrence · Aligning the empty sequence with a sequence · Aligning a sequence with the empty sequence

Used byThe base-case alignment is optimal

DefinitionBase-case alignment for Hirschberg#✓fully proved

Fix a substitution score \(\sigma\) assigning an integer to each pair of letters and an integer gap score \(g\), and write a column as a pair whose missing entry, a gap, is marked \(\bot\). The base-case alignment of sequences \(x\) and \(y\) is the empty alignment if both are empty; the single column \((\bot, b)\) if \(x\) is empty and \(y = [b]\); the single column \((a, \bot)\) if \(x = [a]\) and \(y\) is empty; if \(x = [a]\) and \(y = [b]\), it is the single column \((a, b)\) when \(\sigma(a, b) \ge 2g\) and the two columns \((a, \bot)\), \((\bot, b)\) otherwise; and it is the empty alignment when \(x\) or \(y\) has length at least \(2\).

def smallAlign : List α → List α → Alignment α
  | [], [] => []
  | [], [b] => [(none, some b)]
  | [a], [] => [(some a, none)]
  | [a], [b] => if σ a b ≥ 2 * gap then [(some a, some b)]
      else [(some a, none), (none, some b)]
  | _, _ => []

Uses 1 · Used by 8

Statement usesAlignment

Used byHirschberg reconstruction with enough fuel attains the optimum · The base-case alignment is optimal · 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

TheoremThe base-case alignment is valid#✓fully proved

For every substitution score \(\sigma\) assigning an integer to each pair of letters, integer gap score \(g\) and sequences \(x\), \(y\) with \(|x| \le 1\) and \(|y| \le 1\), the base-case alignment of \(x\) and \(y\) is a valid alignment of \(x\) and \(y\).

theorem isAlignment_smallAlign (xs ys : List α) (hxs : xs.length ≤ 1)
    (hys : ys.length ≤ 1) : IsAlignment (smallAlign σ gap xs ys) xs ys

Uses 3 · Used by 1

Statement usesValid alignment of two sequences · Base-case alignment for Hirschberg

Proof usesAlignment

Used byHirschberg reconstruction with enough fuel is valid

TheoremThe base-case alignment is optimal#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). For all lists \(xs\), \(ys\) over \(\alpha\) with \(|xs| \le 1\) and \(|ys| \le 1\), the alignment score of the base-case alignment of \(xs\) and \(ys\) equals the Needleman–Wunsch score of \(xs\) and \(ys\).

theorem alignmentScore_smallAlign_eq_nwScore (xs ys : List α)
    (hxs : xs.length ≤ 1) (hys : ys.length ≤ 1) :
    alignmentScore σ gap (smallAlign σ gap xs ys) = nwScore σ gap xs ys

Uses 8 · Used by 1

Statement usesScore of an alignment · Needleman–Wunsch score · Base-case alignment for Hirschberg

Proof usesAlignment · Score of an alignment column · Aligning the empty sequence with a sequence · Aligning a sequence with the empty sequence · Needleman–Wunsch score of two single letters

Used byHirschberg reconstruction with enough fuel attains the optimum

DefinitionHirschberg reconstruction with fuel#✓fully proved

Fix a substitution score \(\sigma\) assigning an integer to each pair of letters and an integer gap score \(g\), and write \(\mathrm{NW}\) for the Needleman–Wunsch score. For a sequence \(s\), write \(s_{\lt j}\) for its first \(j\) letters and \(s_{\ge j}\) for the remaining letters. The Hirschberg reconstruction of sequences \(x\) and \(y\) with fuel \(n\) is the alignment defined by recursion on \(n\). With fuel \(0\) it is the empty alignment. With fuel \(n + 1\): if \(|x| \le 1\) and \(|y| \le 1\), it is the base-case alignment of \(x\) and \(y\); otherwise, if \(|y| \ge |x|\), let \(m = \lfloor |y|/2 \rfloor\) and let \(k\) be the first index \(j \in \{0, \dots, |x|\}\) that maximizes \(\mathrm{NW}(x_{\lt j}, y_{\lt m}) + \mathrm{NW}(x_{\ge j}, y_{\ge m})\), and the result is the concatenation of the reconstructions with fuel \(n\) of \(x_{\lt k}\) and \(y_{\lt m}\) and of \(x_{\ge k}\) and \(y_{\ge m}\); otherwise, let \(m = \lfloor |x|/2 \rfloor\) and let \(k\) be the first index \(j \in \{0, \dots, |y|\}\) that maximizes \(\mathrm{NW}(x_{\lt m}, y_{\lt j}) + \mathrm{NW}(x_{\ge m}, y_{\ge j})\), and the result is the concatenation of the reconstructions with fuel \(n\) of \(x_{\lt m}\) and \(y_{\lt k}\) and of \(x_{\ge m}\) and \(y_{\ge k}\).

Hirschberg's alignment algorithm runs this reconstruction with fuel \(|x| + |y|\).

Cslib.Algorithms.Lean.hirschbergAlign · 27 lines

def hirschbergAlign : ℕ → List α → List α → Alignment α
  | 0, _, _ => []
  | fuel + 1, xs, ys =>
      if (decide (xs.length ≤ 1) && decide (ys.length ≤ 1)) then
        smallAlign σ gap xs ys
      else if decide (ys.length ≥ xs.length) then
        hirschbergAlign fuel
            (List.take (bestArgmax (fun k => nwScore σ gap (List.take k xs)
              (List.take (ys.length / 2) ys) + nwScore σ gap (List.drop k xs)
              (List.drop (ys.length / 2) ys)) xs.length) xs)
            (List.take (ys.length / 2) ys) ++
        hirschbergAlign fuel
            (List.drop (bestArgmax (fun k => nwScore σ gap (List.take k xs)
              (List.take (ys.length / 2) ys) + nwScore σ gap (List.drop k xs)
              (List.drop (ys.length / 2) ys)) xs.length) xs)
            (List.drop (ys.length / 2) ys)
      else
        hirschbergAlign fuel
            (List.take (xs.length / 2) xs)
            (List.take (bestArgmax (fun k => nwScore σ gap
              (List.take (xs.length / 2) xs) (List.take k ys) + nwScore σ gap
              (List.drop (xs.length / 2) xs) (List.drop k ys)) ys.length) ys) ++
        hirschbergAlign fuel
            (List.drop (xs.length / 2) xs)
            (List.drop (bestArgmax (fun k => nwScore σ gap
              (List.take (xs.length / 2) xs) (List.take k ys) + nwScore σ gap
              (List.drop (xs.length / 2) xs) (List.drop k ys)) ys.length) ys)

Uses 4 · Used by 6

Statement usesAlignment · Argmax over an initial segment · Needleman–Wunsch score · Base-case alignment for Hirschberg

Used byHirschberg reconstruction with enough fuel attains the optimum · Hirschberg's alignment algorithm · 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

TheoremHirschberg reconstruction on lists of length at most one#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). For every \(n \in \mathbb{N}\) and all lists \(xs\), \(ys\) over \(\alpha\) with \(|xs| \le 1\) and \(|ys| \le 1\), the Hirschberg reconstruction of \(xs\) and \(ys\) with fuel \(n + 1\) is the base-case alignment of \(xs\) and \(ys\).

theorem hirschbergAlign_small (fuel : ℕ) (xs ys : List α)
    (hsmall : xs.length ≤ 1 ∧ ys.length ≤ 1) :
    hirschbergAlign σ gap (fuel + 1) xs ys = smallAlign σ gap xs ys

Uses 5 · Used by 2

Statement usesAlignment · Hirschberg reconstruction with fuel · Base-case alignment for Hirschberg

Proof usesArgmax over an initial segment · Needleman–Wunsch score

Used byHirschberg reconstruction with enough fuel attains the optimum · Hirschberg reconstruction with enough fuel is valid

TheoremHirschberg recursion step splitting the second sequence#✓fully proved

Fix a substitution score \(\sigma\) assigning an integer to each pair of letters and an integer gap score \(g\), and write \(\mathrm{NW}\) for the Needleman–Wunsch score. For a sequence \(s\), write \(s_{\lt j}\) for its first \(j\) letters and \(s_{\ge j}\) for the remaining letters. Let \(x\), \(y\) be sequences with \(|y| \ge |x|\) that do not both have length at most \(1\), let \(m = \lfloor |y|/2 \rfloor\), and let \(k\) be the first index \(j \in \{0, \dots, |x|\}\) that maximizes \(\mathrm{NW}(x_{\lt j}, y_{\lt m}) + \mathrm{NW}(x_{\ge j}, y_{\ge m})\). Then for every natural number \(n\), the Hirschberg reconstruction of \(x\) and \(y\) with fuel \(n + 1\) is the concatenation of the Hirschberg reconstruction of \(x_{\lt k}\) and \(y_{\lt m}\) with fuel \(n\) and the Hirschberg reconstruction of \(x_{\ge k}\) and \(y_{\ge m}\) with fuel \(n\).

theorem hirschbergAlign_split_ys (fuel : ℕ) (xs ys : List α)
    (hsmall : ¬ (xs.length ≤ 1 ∧ ys.length ≤ 1)) (hge : ys.length ≥ xs.length) :
    hirschbergAlign σ gap (fuel + 1) xs ys =
      hirschbergAlign σ gap fuel
          (List.take (bestArgmax (fun k => nwScore σ gap (List.take k xs)
            (List.take (ys.length / 2) ys) + nwScore σ gap (List.drop k xs)
            (List.drop (ys.length / 2) ys)) xs.length) xs)
          (List.take (ys.length / 2) ys) ++
      hirschbergAlign σ gap fuel
          (List.drop (bestArgmax (fun k => nwScore σ gap (List.take k xs)
            (List.take (ys.length / 2) ys) + nwScore σ gap (List.drop k xs)
            (List.drop (ys.length / 2) ys)) xs.length) xs)
          (List.drop (ys.length / 2) ys)

Uses 5 · Used by 2

Statement usesAlignment · Argmax over an initial segment · Hirschberg reconstruction with fuel · Needleman–Wunsch score

Proof usesBase-case alignment for Hirschberg

Used byHirschberg reconstruction with enough fuel attains the optimum · Hirschberg reconstruction with enough fuel is valid

TheoremHirschberg reconstruction splits the longer first list#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). Write \(H_n(u, v)\) for the Hirschberg reconstruction of lists \(u\), \(v\) with fuel \(n\), \(S(u, v)\) for their Needleman–Wunsch score, and \(u_{\lt m}\), \(u_{\ge m}\) for the first \(m\) elements of \(u\) and the rest. Let \(xs\), \(ys\) be lists over \(\alpha\) that are not both of length at most \(1\), with \(|ys| < |xs|\). Put \(h = \lfloor |xs| / 2 \rfloor\) and let \(k\) be the least maximizer over \(\{0, \dots, |ys|\}\) of \(j \mapsto S(xs_{\lt h}, ys_{\lt j}) + S(xs_{\ge h}, ys_{\ge j})\). Then for every \(n \in \mathbb{N}\), \(H_{n+1}(xs, ys)\) is the concatenation of \(H_n(xs_{\lt h}, ys_{\lt k})\) and \(H_n(xs_{\ge h}, ys_{\ge k})\).

theorem hirschbergAlign_split_xs (fuel : ℕ) (xs ys : List α)
    (hsmall : ¬ (xs.length ≤ 1 ∧ ys.length ≤ 1))
    (hge : ¬ ys.length ≥ xs.length) :
    hirschbergAlign σ gap (fuel + 1) xs ys =
      hirschbergAlign σ gap fuel
          (List.take (xs.length / 2) xs)
          (List.take (bestArgmax (fun k => nwScore σ gap
            (List.take (xs.length / 2) xs) (List.take k ys) + nwScore σ gap
            (List.drop (xs.length / 2) xs) (List.drop k ys)) ys.length) ys) ++
      hirschbergAlign σ gap fuel
          (List.drop (xs.length / 2) xs)
          (List.drop (bestArgmax (fun k => nwScore σ gap
            (List.take (xs.length / 2) xs) (List.take k ys) + nwScore σ gap
            (List.drop (xs.length / 2) xs) (List.drop k ys)) ys.length) ys)

Uses 5 · Used by 2

Statement usesAlignment · Argmax over an initial segment · Hirschberg reconstruction with fuel · Needleman–Wunsch score

Proof usesBase-case alignment for Hirschberg

Used byHirschberg reconstruction with enough fuel attains the optimum · Hirschberg reconstruction with enough fuel is valid

TheoremHirschberg reconstruction with enough fuel is valid#✓fully proved

For every substitution score \(\sigma\) assigning an integer to each pair of letters, integer gap score \(g\), natural number \(n\) and sequences \(x\), \(y\) with \(|x| + |y| \le n\), the Hirschberg reconstruction of \(x\) and \(y\) with fuel \(n\) is a valid alignment of \(x\) and \(y\).

theorem isAlignment_hirschbergAlign : ∀ (fuel : ℕ) (xs ys : List α),
    xs.length + ys.length ≤ fuel →
    IsAlignment (hirschbergAlign σ gap fuel xs ys) xs ys

Uses 12 · Used by 1

Statement usesValid alignment of two sequences · Hirschberg reconstruction with fuel

Proof usesAlignment · Argmax over an initial segment · The argmax over \(\{0, \dots, n\}\) is at most \(n\) · Hirschberg reconstruction on lists of length at most one · Hirschberg reconstruction splits the longer first list · Hirschberg recursion step splitting the second sequence · Concatenation of alignments · The base-case alignment is valid · Needleman–Wunsch score · Base-case alignment for Hirschberg

Used byHirschberg reconstruction is valid

TheoremHirschberg reconstruction with enough fuel attains the optimum#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). For every fuel \(n \in \mathbb{N}\) and all lists \(xs\), \(ys\) over \(\alpha\) with \(|xs| + |ys| \le n\), the alignment score of the Hirschberg reconstruction of \(xs\) and \(ys\) with fuel \(n\) equals the Needleman–Wunsch score of \(xs\) and \(ys\).

theorem alignmentScore_hirschbergAlign : ∀ (fuel : ℕ) (xs ys : List α),
    xs.length + ys.length ≤ fuel →
    alignmentScore σ gap (hirschbergAlign σ gap fuel xs ys) = nwScore σ gap xs ys

Uses 14 · Used by 1

Statement usesScore of an alignment · Hirschberg reconstruction with fuel · Needleman–Wunsch score

Proof usesAlignment · The base-case alignment is optimal · Argmax over an initial segment · The argmax over \(\{0, \dots, n\}\) is at most \(n\) · Score of an alignment column · Hirschberg reconstruction on lists of length at most one · Hirschberg reconstruction splits the longer first list · Hirschberg recursion step splitting the second sequence · Hirschberg split identity, splitting the first sequence · Hirschberg split identity, splitting the second sequence · Base-case alignment for Hirschberg

Used byHirschberg reconstruction attains the Needleman–Wunsch optimum

DefinitionHirschberg's alignment algorithm#✓fully proved

Fix a substitution score \(\sigma\) assigning an integer to each pair of letters and an integer gap score \(g\). The Hirschberg alignment of sequences \(x\) and \(y\) is the Hirschberg reconstruction of \(x\) and \(y\) with fuel \(|x| + |y|\).

def hirschberg (xs ys : List α) : Alignment α :=
  hirschbergAlign σ gap (xs.length + ys.length) xs ys

Uses 2 · Used by 2

Statement usesAlignment · Hirschberg reconstruction with fuel

Used byHirschberg reconstruction attains the Needleman–Wunsch optimum · Hirschberg reconstruction is valid

TheoremHirschberg reconstruction is valid#✓fully proved

For every substitution score \(\sigma\) assigning an integer to each pair of letters, integer gap score \(g\) and sequences \(x\), \(y\), the Hirschberg alignment of \(x\) and \(y\) is a valid alignment of \(x\) and \(y\).

theorem isAlignment_hirschberg (xs ys : List α) :
    IsAlignment (hirschberg σ gap xs ys) xs ys

Uses 3

Statement usesValid alignment of two sequences · Hirschberg's alignment algorithm

Proof usesHirschberg reconstruction with enough fuel is valid

TheoremHirschberg reconstruction attains the Needleman–Wunsch optimum#✓fully proved

Fix a type \(\alpha\), a substitution score \(\sigma : \alpha \to \alpha \to \mathbb{Z}\) and a gap score \(g \in \mathbb{Z}\). For all lists \(xs\), \(ys\) over \(\alpha\), the alignment score of the Hirschberg alignment of \(xs\) and \(ys\) equals the Needleman–Wunsch score of \(xs\) and \(ys\).

theorem alignmentScore_hirschberg (xs ys : List α) :
    alignmentScore σ gap (hirschberg σ gap xs ys) = nwScore σ gap xs ys

Uses 4

Statement usesScore of an alignment · Hirschberg's alignment algorithm · Needleman–Wunsch score

Proof usesHirschberg reconstruction with enough fuel attains the optimum

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.