Longest increasing subsequence

DefinitionLength of a longest increasing subsequence#✓fully proved

For a list \(xs\) over a preorder and a natural number \(k\), \(k\) is the length of a longest strictly increasing subsequence of \(xs\) when some strictly increasing subsequence of \(xs\) has length \(k\) and every strictly increasing subsequence of \(xs\) has length at most \(k\). Here a subsequence need not be contiguous, and strictly increasing means that each element is strictly less than every later one.

def IsLISLength (xs : List α) (k : ℕ) : Prop :=
  (∃ ys, ys <+ xs ∧ ys.Pairwise (· < ·) ∧ ys.length = k) ∧
    ∀ ys, ys <+ xs → ys.Pairwise (· < ·) → ys.length ≤ k

Used by 5

Used byThe quadratic LIS program attains the optimal length · Correctness of the quadratic LIS program, by length · Patience sorting agrees with the quadratic dynamic program · Correctness of patience sorting · Uniqueness of the longest increasing subsequence length

DefinitionTable cell of the LIS dynamic program#✓fully proved

For an element \(x\), lists \(s\) and \(zs\), and a natural number \(k\), the pair \((k, zs)\) is a table cell for \(x\) followed by \(s\) when \(zs\) is a subsequence (not necessarily contiguous) of \(s\), the list \(x\) followed by \(zs\) is strictly increasing (each element strictly less than every later one) and has length \(k\), and for every subsequence \(zs'\) of \(s\) such that \(x\) followed by \(zs'\) is strictly increasing, the list \(x\) followed by \(zs'\) has length at most \(k\). So \(x\) followed by \(zs\) is a longest strictly increasing subsequence of \(x\) followed by \(s\) that starts with this \(x\).

def IsLISCell (x : α) (s : List α) (k : ℕ) (zs : List α) : Prop :=
  zs <+ s ∧ (x :: zs).Pairwise (· < ·) ∧ zs.length + 1 = k ∧
    ∀ zs', zs' <+ s → (x :: zs').Pairwise (· < ·) → zs'.length + 1 ≤ k

Used by 3

Used byThe step of the LIS recurrence · Invariant of the LIS table · Correctness of the quadratic LIS program

DefinitionBest table entry above a value#✓fully proved

Given a value \(x\) and a list \(t\) of entries \((y, k, zs)\), where \(y\) is a value, \(k\) a natural number and \(zs\) a list of values, this timed computation returns the pair of \(k\) and the list \(y\) followed by \(zs\) for an entry of \(t\) with \(x < y\) whose \(k\) is largest among such entries, provided that \(k\) is positive; if no entry with \(x < y\) has \(k > 0\), it returns \(0\) and the empty list. It costs one unit per entry of \(t\).

def maxAbove (x : α) : List (α × ℕ × List α) → TimeM ℕ (ℕ × List α)
  | [] => pure (0, [])
  | (y, k, zs) :: t => do
      ✓
      let b ← maxAbove x t
      pure (if x < y ∧ b.1 < k then (k, y :: zs) else b)

Used by 5

Used byThe step of the LIS recurrence · Table of the quadratic LIS program · Correctness of the quadratic LIS program · Running time of the quadratic LIS program · Cost of the scan for the best entry above a value

DefinitionTable of the quadratic LIS program#✓fully proved

The table of a list is a list of triples \((y, k, zs)\), built from the right: the empty list has the empty table, and the table of \(x\) followed by \(rest\) is the table \(t\) of \(rest\) with the entry \((x, b + 1, w)\) put in front, where \((b, w)\) is the result of the scan of \(t\) for entries above \(x\). Building the table costs the total cost of these scans.

def lisTable : List α → TimeM ℕ (List (α × ℕ × List α))
  | [] => pure []
  | x :: rest => do
      let t ← lisTable rest
      let b ← maxAbove x t
      pure ((x, b.1 + 1, b.2) :: t)

Uses 1 · Used by 3

Statement usesBest table entry above a value

Used byLongest increasing subsequence by dynamic programming · Correctness of the quadratic LIS program · Running time of the quadratic LIS program

DefinitionTable entry of largest length#✓fully proved

Given a list \(t\) of entries \((y, k, zs)\), where \(k\) is a natural number and \(zs\) is a list with elements of the same type as \(y\), this timed computation returns the pair of \(k\) and the list \(y\) followed by \(zs\) for an entry of \(t\) whose \(k\) is largest, provided that this \(k\) is positive, and returns \(0\) and the empty list otherwise (in particular when \(t\) is empty). It costs one unit per entry of \(t\).

def maxEntry : List (α × ℕ × List α) → TimeM ℕ (ℕ × List α)
  | [] => pure (0, [])
  | (y, k, zs) :: t => do
      ✓
      let b ← maxEntry t
      pure (if b.1 < k then (k, y :: zs) else b)

Used by 3

Used byLongest increasing subsequence by dynamic programming · Correctness of the quadratic LIS program · Running time of the quadratic LIS program

DefinitionLongest increasing subsequence by dynamic programming#✓fully proved

Given a list \(x_0, \dots, x_{n-1}\) of elements of a preorder with decidable \(<\), this timed computation builds, from the right, a table recording for each position \(i\) a length and a strictly increasing subsequence starting with \(x_i\) (the longest one, by the recurrence \(L_i = 1 + \max \{ L_j : i < j,\ x_i < x_j \}\) with \(\max \emptyset = 0\)), and returns the stored subsequence of an entry of largest length, or the empty list when \(n = 0\). The cost is one unit for each table entry inspected: building the entry for position \(i\) scans the entries to its right, and the final scan inspects each entry once.

def longestIncreasingSubsequence (xs : List α) : TimeM ℕ (List α) := do
  let t ← lisTable xs
  let b ← maxEntry t
  pure b.2

Uses 2 · Used by 5

Statement usesTable of the quadratic LIS program · Table entry of largest length

Used byThe quadratic LIS program attains the optimal length · Correctness of the quadratic LIS program, by length · Correctness of the quadratic LIS program · Running time of the quadratic LIS program · Patience sorting agrees with the quadratic dynamic program

TheoremCost of the scan for the best entry above a value#✓fully proved

Let \(\alpha\) be a preorder with decidable \(<\). For every value \(x \in \alpha\) and every list \(t\) of entries \((y, k, zs)\), where \(y \in \alpha\), \(k\) is a natural number and \(zs\) is a list over \(\alpha\), the scan of \(t\) for the best table entry above \(x\) costs exactly the length of \(t\).

@[simp]
theorem maxAbove_time (x : α) (t : List (α × ℕ × List α)) :
    (maxAbove x t).time = t.length

Uses 1 · Used by 1

Statement usesBest table entry above a value

Used byRunning time of the quadratic LIS program

TheoremRunning time of the quadratic LIS program#✓fully proved

For every list \(xs\) of length \(n\) over a preorder, twice the cost of the quadratic longest-increasing-subsequence program on \(xs\) equals \(n(n + 1)\), so the program costs exactly \(n(n + 1)/2\).

The cost model charges one unit for each table entry inspected.

theorem longestIncreasingSubsequence_time (xs : List α) :
    2 * (longestIncreasingSubsequence xs).time = xs.length * (xs.length + 1)

Uses 5

Statement usesLongest increasing subsequence by dynamic programming

Proof usesTable of the quadratic LIS program · Best table entry above a value · Cost of the scan for the best entry above a value · Table entry of largest length

TheoremA subsequence starting with \(y\) starts at an occurrence of \(y\)#✓fully proved

For an element \(y\) and lists \(zs\) and \(l\), if the list \(y\) followed by \(zs\) is a subsequence (not necessarily contiguous) of \(l\), then there is a list \(s\) such that \(y\) followed by \(s\) is a suffix of \(l\) and \(zs\) is a subsequence of \(s\).

theorem exists_suffix_of_cons_sublist {y : α} {zs l : List α} (h : y :: zs <+ l) :
    ∃ s, y :: s <:+ l ∧ zs <+ s

Used by 2

Used byThe step of the LIS recurrence · Correctness of the quadratic LIS program

DefinitionInvariant of the LIS table#✓fully proved

A table \(t\) of triples \((y, k, zs)\) satisfies the invariant for a list \(l\) when every entry \((y, k, zs)\) of \(t\) has a list \(s\) such that \(y\) followed by \(s\) is a suffix of \(l\) and \((k, zs)\) is a table cell for \(y\) followed by \(s\), and conversely, for every element \(y\) and list \(s\) such that \(y\) followed by \(s\) is a suffix of \(l\), some entry \((y, k, zs)\) of \(t\) makes \((k, zs)\) a table cell for \(y\) followed by \(s\).

def LISTableSpec (l : List α) (t : List (α × ℕ × List α)) : Prop :=
  (∀ y k zs, (y, k, zs) ∈ t → ∃ s, y :: s <:+ l ∧ IsLISCell y s k zs) ∧
    ∀ y s, y :: s <:+ l → ∃ k zs, (y, k, zs) ∈ t ∧ IsLISCell y s k zs

Uses 1 · Used by 2

Statement usesTable cell of the LIS dynamic program

Used byThe step of the LIS recurrence · Correctness of the quadratic LIS program

TheoremThe step of the LIS recurrence#✓fully proved

Let \(x\) be an element, \(rest\) a list, and \(t\) a table of triples \((y, k, zs)\) that satisfies the invariant of the LIS table for \(rest\). Let \((b, w)\) be the result of the scan of \(t\) for entries above \(x\). Then \((b + 1, w)\) is a table cell for \(x\) followed by \(rest\): \(w\) is a subsequence of \(rest\), the list \(x\) followed by \(w\) is strictly increasing and has length \(b + 1\), and every strictly increasing list \(x\) followed by a subsequence of \(rest\) has length at most \(b + 1\).

theorem isLISCell_maxAbove {x : α} {rest : List α} {t : List (α × ℕ × List α)}
    (ht : LISTableSpec rest t) :
    IsLISCell x rest ((maxAbove x t).ret.1 + 1) (maxAbove x t).ret.2

Uses 4 · Used by 1

Statement usesTable cell of the LIS dynamic program · Invariant of the LIS table · Best table entry above a value

Proof usesA subsequence starting with \(y\) starts at an occurrence of \(y\)

Used byCorrectness of the quadratic LIS program

TheoremCorrectness of the quadratic LIS program#✓fully proved

For every list \(xs\) over a preorder, the list returned by the quadratic longest-increasing-subsequence program on \(xs\) is a subsequence of \(xs\), is strictly increasing (each element strictly less than every later one), and is at least as long as every strictly increasing subsequence of \(xs\).

theorem longestIncreasingSubsequence_spec (xs : List α) :
    (longestIncreasingSubsequence xs).ret <+ xs ∧
      (longestIncreasingSubsequence xs).ret.Pairwise (· < ·) ∧
      ∀ ys, ys <+ xs → ys.Pairwise (· < ·) →
        ys.length ≤ (longestIncreasingSubsequence xs).ret.length

Uses 8 · Used by 1

Statement usesLongest increasing subsequence by dynamic programming

Proof usesTable cell of the LIS dynamic program · Invariant of the LIS table · A subsequence starting with \(y\) starts at an occurrence of \(y\) · The step of the LIS recurrence · Table of the quadratic LIS program · Best table entry above a value · Table entry of largest length

Used byThe quadratic LIS program attains the optimal length

TheoremThe quadratic LIS program attains the optimal length#✓fully proved

For every list \(xs\) over a preorder, the length of the list returned by the quadratic longest-increasing-subsequence program on \(xs\) is the length of a longest strictly increasing subsequence of \(xs\).

theorem isLISLength_longestIncreasingSubsequence (xs : List α) :
    IsLISLength xs (longestIncreasingSubsequence xs).ret.length

Uses 3 · Used by 1

Statement usesLength of a longest increasing subsequence · Longest increasing subsequence by dynamic programming

Proof usesCorrectness of the quadratic LIS program

Used byCorrectness of the quadratic LIS program, by length

TheoremUniqueness of the longest increasing subsequence length#✓fully proved

For every list \(xs\) of elements of a preorder and all natural numbers \(k\) and \(k'\), if both \(k\) and \(k'\) are the length of a longest strictly increasing subsequence of \(xs\), then \(k = k'\).

theorem IsLISLength.unique {xs : List α} {k k' : ℕ} (h : IsLISLength xs k)
    (h' : IsLISLength xs k') : k = k'

Uses 1 · Used by 1

Statement usesLength of a longest increasing subsequence

Used byCorrectness of the quadratic LIS program, by length

TheoremCorrectness of the quadratic LIS program, by length#✓fully proved

For every list \(xs\) over a preorder and every natural number \(k\), the list returned by the quadratic longest-increasing-subsequence program on \(xs\) has length \(k\) if and only if \(k\) is the length of a longest strictly increasing subsequence of \(xs\).

theorem length_longestIncreasingSubsequence_eq_iff (xs : List α) (k : ℕ) :
    (longestIncreasingSubsequence xs).ret.length = k ↔ IsLISLength xs k

Uses 4 · Used by 1

Statement usesLength of a longest increasing subsequence · Longest increasing subsequence by dynamic programming

Proof usesUniqueness of the longest increasing subsequence length · The quadratic LIS program attains the optimal length

Used byPatience sorting agrees with the quadratic dynamic program

DefinitionPatience step#✓fully proved

Given an array \(t\) of tails and an element \(x\) over a linear order, let \(i\) be the index returned by the lower-bound binary search for \(x\) in \(t\). If \(i\) is less than the size of \(t\), the step replaces the entry of \(t\) at index \(i\) by \(x\); otherwise it appends \(x\) to \(t\). Its cost is the number of comparisons made by the binary search.

When \(t\) is sorted increasingly, as it stays throughout the patience scan from the empty array, \(i\) is the first index whose entry is at least \(x\), so the step replaces the first entry \(\ge x\), or appends \(x\) if there is none. On unsorted input \(i\) need not be the first such index.

def patienceStep (tails : Array α) (x : α) : TimeM ℕ (Array α) := do
  let i ← lowerBound tails x
  if h : i < tails.size then pure (tails.set i x h) else pure (tails.push x)

Uses 1 · Used by 4

Statement usesLower-bound search

Used byComparison bound for patience sorting · Patience scan · A patience step grows the tails by at most one · The patience scan preserves the invariant

DefinitionPatience scan#✓fully proved

Given an array of tails and a list over a linear order, the patience scan applies the patience step to the elements of the list in order: on the empty list it returns the tails unchanged, and on a list \(x\) followed by \(xs\) it applies the patience step for \(x\) to the tails and then runs the patience scan of \(xs\) from the result. Its cost is the total cost of the steps.

def patienceScan : Array α → List α → TimeM ℕ (Array α)
  | tails, [] => pure tails
  | tails, x :: xs => do
      let t ← patienceStep tails x
      patienceScan t xs

Uses 1 · Used by 4

Statement usesPatience step

Used byPatience sorting · Correctness of patience sorting · Comparison bound for patience sorting · The patience scan preserves the invariant

DefinitionPatience sorting#✓fully proved

Given a list \(xs\) over a linear order, patience sorting runs the patience scan of \(xs\) starting from the empty array of tails and returns the size of the resulting array. Its cost is the number of comparisons made by the scan.

def patienceLength (xs : List α) : TimeM ℕ ℕ := do
  let t ← patienceScan #[] xs
  pure t.size

Uses 1 · Used by 3

Statement usesPatience scan

Used byPatience sorting agrees with the quadratic dynamic program · Correctness of patience sorting · Comparison bound for patience sorting

StructurePatience sorting invariant#✓fully proved

For lists \(P\) and \(t = (t_0, \dots, t_{m-1})\) over a linear order, the invariant holds for the processed prefix \(P\) and the tails \(t\) when three conditions hold: \(t\) is strictly increasing; for every \(k < m\) some strictly increasing subsequence of \(P\) of length \(k + 1\) has last element \(t_k\); and every nonempty strictly increasing subsequence of \(P\), of length \(\ell\) and with last element \(y\), satisfies \(\ell \le m\) and \(t_{\ell - 1} \le y\).

structure PatienceInv (P t : List α) : Prop where
  sorted : t.Pairwise (· < ·)
  witness : ∀ k (hk : k < t.length), ∃ ys, ys <+ P ∧ ys.Pairwise (· < ·) ∧
    ys.length = k + 1 ∧ ys.getLast? = some t[k]
  bound : ∀ ys y, ys <+ P → ys.Pairwise (· < ·) → ys.getLast? = some y →
    ∃ h : ys.length - 1 < t.length, t[ys.length - 1] ≤ y

Used by 2

Used byCorrectness of patience sorting · The patience scan preserves the invariant

TheoremThe patience scan preserves the invariant#✓fully proved

Let \(P\) be a list and \(t\) an array of tails over a linear order such that the patience sorting invariant holds for \(P\) and the entries of \(t\). Then for every list \(xs\), the invariant holds for \(P\) followed by \(xs\) and the entries of the array returned by the patience scan of \(xs\) from \(t\).

theorem PatienceInv.scan {P : List α} {tails : Array α} (h : PatienceInv P tails.toList)
    (xs : List α) : PatienceInv (P ++ xs) (patienceScan tails xs).ret.toList

Uses 5 · Used by 1

Statement usesPatience sorting invariant · Patience scan

Proof usesLower-bound search · Correctness of lower-bound search · Patience step

Used byCorrectness of patience sorting

TheoremCorrectness of patience sorting#✓fully proved

For every list \(xs\) over a linear order, the value returned by patience sorting on \(xs\) is the length of a longest strictly increasing subsequence of \(xs\): some strictly increasing subsequence of \(xs\) has this length, and no strictly increasing subsequence of \(xs\) is longer.

theorem patienceLength_spec (xs : List α) : IsLISLength xs (patienceLength xs).ret

Uses 5 · Used by 1

Statement usesLength of a longest increasing subsequence · Patience sorting

Proof usesPatience sorting invariant · The patience scan preserves the invariant · Patience scan

Used byPatience sorting agrees with the quadratic dynamic program

TheoremPatience sorting agrees with the quadratic dynamic program#✓fully proved

For every list \(xs\) over a linear order, the value returned by patience sorting on \(xs\) equals the length of the list returned on \(xs\) by the quadratic dynamic program for a longest strictly increasing subsequence.

theorem patienceLength_eq_length_longestIncreasingSubsequence (xs : List α) :
    (patienceLength xs).ret = (longestIncreasingSubsequence xs).ret.length

Uses 5

Statement usesLongest increasing subsequence by dynamic programming · Patience sorting

Proof usesLength of a longest increasing subsequence · Correctness of the quadratic LIS program, by length · Correctness of patience sorting

TheoremA patience step grows the tails by at most one#✓fully proved

Let \(\alpha\) be a linear order. For every array \(t\) over \(\alpha\) and every element \(x \in \alpha\), the array returned by the patience step for \(x\) on \(t\) has size at most the size of \(t\) plus \(1\).

theorem patienceStep_size_le (tails : Array α) (x : α) :
    (patienceStep tails x).ret.size ≤ tails.size + 1

Uses 2 · Used by 1

Statement usesPatience step

Proof usesLower-bound search

Used byComparison bound for patience sorting

TheoremComparison bound for patience sorting#✓fully proved

For every list \(xs\) of length \(n\) over a linear order, patience sorting on \(xs\) uses at most \(n \lceil \log_2 (n + 1) \rceil\) comparisons.

theorem patienceLength_time_le (xs : List α) :
    (patienceLength xs).time ≤ xs.length * Nat.clog 2 (xs.length + 1)

Uses 6

Statement usesPatience sorting

Proof usesLower-bound search · Comparison bound for lower-bound search · Patience scan · Patience step · A patience step grows the tails by at most one

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.