Edit distance

InductiveEdit step#✓fully proved

An edit step over a type \(\alpha\) is one of four operations, for \(a, b \in \alpha\): keep \(a\) (consume the input value \(a\) and reproduce it), delete \(a\) (consume \(a\)), insert \(a\) (produce \(a\) without consuming input), or substitute \(a\) by \(b\) (consume \(a\) and produce \(b\)).

inductive EditStep (α : Type u) where
  /-- Consume and reproduce the given value at zero cost. -/
  | keep (value : α)
  /-- Consume the given value. -/
  | delete (value : α)
  /-- Produce the given value without consuming input. -/
  | insert (value : α)
  /-- Consume the first value and produce the second. -/
  | substitute (source target : α)
  deriving Repr, BEq, DecidableEq

Used by 15

Used byRunning an edit script · Unit cost of an edit step · Cost of an edit script · Edit distance algorithm · Table cost of the edit distance algorithm · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Correctness of the returned edit script · The returned edit script realizes the distance · Running time of the edit distance algorithm · Edit script · Composition of edit scripts is subadditive in cost · Every edit script has an inverse of the same cost

AbbreviationEdit script#✓fully proved

An edit script over a type \(\alpha\) is a finite list of edit steps over \(\alpha\), applied from left to right.

abbrev EditScript (α : Type u) := List (EditStep α)

Uses 1 · Used by 17

Statement usesEdit step

Used byRunning an edit script · Cost of an edit script · Edit distance algorithm · Table cost of the edit distance algorithm · Symmetry · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Edit-distance result record · Correctness of the returned edit script · The returned edit script realizes the distance · Running time of the edit distance algorithm · The triangle inequality · Composition of edit scripts is subadditive in cost · Every edit script has an inverse of the same cost · An edit script transforming one list into another

DefinitionUnit cost of an edit step#✓fully proved

The cost of an edit step is \(0\) for a keep step and \(1\) for a deletion, an insertion or a substitution.

def EditStep.cost : EditStep α → Nat
  | .keep _ => 0
  | .delete _ => 1
  | .insert _ => 1
  | .substitute _ _ => 1

Uses 1 · Used by 8

Statement usesEdit step

Used byCost of an edit script · Table cost of the edit distance algorithm · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Correctness of the returned edit script · The returned edit script realizes the distance

DefinitionCost of an edit script#✓fully proved

The cost of an edit script is the sum of the unit costs of its steps; the empty script has cost \(0\).

def EditScript.cost : EditScript α → Nat
  | [] => 0
  | step :: script => step.cost + EditScript.cost script

Uses 3 · Used by 11

Statement usesEdit script · Edit step · Unit cost of an edit step

Used byTable cost of the edit distance algorithm · Symmetry · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Correctness of the returned edit script · The returned edit script realizes the distance · The triangle inequality · Composition of edit scripts is subadditive in cost · Every edit script has an inverse of the same cost

DefinitionRunning an edit script#✓fully proved

Over a type \(\alpha\) with a boolean equality test, running an edit script on an input list processes the steps from left to right and either fails or returns an output list. A keep step with value \(a\) consumes the next input value \(b\) and outputs \(a\); a deletion of \(a\) consumes \(b\) and outputs nothing; a substitution of \(a\) by \(c\) consumes \(b\) and outputs \(c\). Each of these three fails if the input is exhausted or if the equality test of \(a\) against \(b\) fails. An insertion of \(c\) outputs \(c\) without consuming input. When the script ends, the run succeeds with the outputs in order if the input is used up, and fails if input values remain.

def EditScript.apply? [BEq α] : EditScript α → List α → Option (List α)
  | [], [] => some []
  | [], _ :: _ => none
  | .keep value :: script, source :: rest =>
      if value == source then (EditScript.apply? script rest).map (value :: ·) else none
  | .keep _ :: _, [] => none
  | .delete value :: script, source :: rest =>
      if value == source then EditScript.apply? script rest else none
  | .delete _ :: _, [] => none
  | .insert value :: script, source =>
      (EditScript.apply? script source).map (value :: ·)
  | .substitute value target :: script, source :: rest =>
      if value == source then (EditScript.apply? script rest).map (target :: ·) else none
  | .substitute _ _ :: _, [] => none

Uses 2 · Used by 5

Statement usesEdit script · Edit step

Used byMinimality of the computed edit distance · Correctness of the returned edit script · Composition of edit scripts is subadditive in cost · Every edit script has an inverse of the same cost · An edit script transforming one list into another

DefinitionAn edit script transforming one list into another#✓fully proved

Over a type with a boolean equality test, an edit script transforms a list \(x\) into a list \(y\) when running the script on \(x\) succeeds and outputs \(y\).

def EditScript.Transforms [BEq α]
    (script : EditScript α) (source target : List α) : Prop :=
  script.apply? source = some target

Uses 2 · Used by 6

Statement usesEdit script · Running an edit script

Used bySymmetry · Minimality of the computed edit distance · Correctness of the returned edit script · The triangle inequality · Composition of edit scripts is subadditive in cost · Every edit script has an inverse of the same cost

StructureEdit-distance result record#✓fully proved

An edit-distance result over a type \(\alpha\) consists of a natural number, the reported distance, and an edit script over \(\alpha\).

The record imposes no relation between the two fields; it is meant to hold a minimum edit distance and a script realizing it.

structure EditDistanceResult (α : Type u) where
  /-- Minimum number of non-keep edit operations. -/
  distance : Nat
  /-- A script that realizes the reported distance. -/
  script : EditScript α
  deriving Repr, BEq, DecidableEq

Uses 1 · Used by 15

Statement usesEdit script

Used byEdit distance algorithm · Table cost of the edit distance algorithm · Symmetry · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Edit distance from the empty list · Edit distance to the empty list · Edit distance between distinct lists is positive · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Correctness of the returned edit script · The returned edit script realizes the distance · Edit distance of a list to itself · Running time of the edit distance algorithm · The triangle inequality

StructureEdit-distance cost counters#✓fully proved

An edit-distance cost record is a pair of natural numbers: the number of dynamic-programming table cells initialized or transitioned, and the number of operations emitted while reconstructing an edit script.

structure EditDistanceCost where
  /-- Dynamic-programming cells initialized or transitioned. -/
  cellTransitions : Nat
  /-- Operations emitted while reconstructing a script. -/
  reconstructionSteps : Nat
  deriving Repr, BEq, DecidableEq

Used by 16

Used byEdit distance algorithm · Table cost of the edit distance algorithm · Symmetry · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Edit distance from the empty list · Edit distance to the empty list · Edit distance between distinct lists is positive · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Correctness of the returned edit script · The returned edit script realizes the distance · Edit distance of a list to itself · Running time of the edit distance algorithm · The triangle inequality · Total edit-distance cost

DefinitionTotal edit-distance cost#✓fully proved

The total of an edit-distance cost record is the number of table cells initialized or transitioned plus the number of operations emitted during reconstruction.

def EditDistanceCost.total (cost : EditDistanceCost) : Nat :=
  cost.cellTransitions + cost.reconstructionSteps

Uses 1 · Used by 1

Statement usesEdit-distance cost counters

Used byRunning time of the edit distance algorithm

DefinitionEdit distance algorithm#✓fully proved

Given lists \(s = s_1 \cdots s_m\) and \(t = t_1 \cdots t_n\) over a type with a Boolean equality test, the algorithm fills a table \(D(i, j)\) for \(0 \le i \le m\) and \(0 \le j \le n\) by \(D(0, j) = j\), \(D(i, 0) = i\) and \(D(i, j) = \min(D(i-1, j-1) + c_{ij}, D(i-1, j) + 1, D(i, j-1) + 1)\) for \(i, j \ge 1\), where \(c_{ij}\) is \(0\) if the test reports \(s_i = t_j\) and \(1\) otherwise. It then walks back from \((m, n)\) to \((0, 0)\): on the boundary it deletes the remaining \(s_i\) or inserts the remaining \(t_j\); otherwise it takes a move attaining the minimum, preferring the diagonal move (a keep of \(s_i\) if the test reports \(s_i = t_j\), else a substitution of \(t_j\) for \(s_i\)), then a deletion of \(s_i\), then an insertion of \(t_j\). It returns the distance \(D(m, n)\) together with the edit script of the chosen moves in left-to-right order. Each of the \((m + 1)(n + 1)\) table entries is charged as one cell transition and each emitted operation as one reconstruction step.

Cslib.Algorithms.Lean.editDistance · 101 lines

public def editDistance {α : Type u} [BEq α] (source target : List α) :
    TimeM EditDistanceCost (EditDistanceResult α) :=
  let diagonalCost (sourceValue targetValue : α) : Nat :=
    if sourceValue == targetValue then 0 else 1
  let diagonalStep (sourceValue targetValue : α) : EditStep α :=
    if sourceValue == targetValue then .keep sourceValue else .substitute sourceValue targetValue
  let Row (n : Nat) : Type u :=
    ULift.{u} (Subtype (fun row : Array Nat => row.size = n + 1))
  let rec @[reducible] buildInitialRow (n : Nat) :
      (j : Nat) → j ≤ n → TimeM EditDistanceCost (Row j)
    | 0, _ => do
        TimeM.tick ⟨1, 0⟩
        pure ⟨⟨#[0], by simp⟩⟩
    | j + 1, hj => do
        let row ← buildInitialRow n j (by omega)
        TimeM.tick ⟨1, 0⟩
        pure ⟨⟨row.down.1.push (j + 1), by simp [row.down.2]⟩⟩
  let rec @[reducible] buildRow (sourceValue : α) (target : Array α)
      (up : Row target.size) (first : Nat) :
      (j : Nat) → j ≤ target.size → TimeM EditDistanceCost (Row j)
    | 0, _ => do
        TimeM.tick ⟨1, 0⟩
        pure ⟨⟨#[first], by simp⟩⟩
    | j + 1, hj => do
        let row ← buildRow sourceValue target up first j (by omega)
        TimeM.tick ⟨1, 0⟩
        let diagonal := up.down.1[j]'(by rw [up.down.2]; omega) +
          if sourceValue == target[j] then 0 else 1
        let deletion := up.down.1[j + 1]'(by rw [up.down.2]; omega) + 1
        let insertion := row.down.1[j]'(by rw [row.down.2]; omega) + 1
        let value := min diagonal (min deletion insertion)
        pure ⟨⟨row.down.1.push value, by simp [row.down.2]⟩⟩
  let Table (m n : Nat) : Type u :=
    ULift.{u} (Subtype (fun data : Array (Array Nat) =>
      data.size = m + 1 ∧ ∀ i (hi : i < data.size), data[i].size = n + 1))
  let cell {m n : Nat} (table : Table m n) (i j : Nat)
      (hi : i ≤ m) (hj : j ≤ n) : Nat :=
    (table.down.1[i]'(by rw [table.down.2.1]; omega))[j]'(by
      rw [table.down.2.2]; omega)
  let rec @[reducible] buildTable (source target : Array α) :
      (i : Nat) → i ≤ source.size → TimeM EditDistanceCost (Table i target.size)
    | 0, _ => do
        let row ← buildInitialRow target.size target.size (by omega)
        pure ⟨⟨#[row.down.1], by simp, by
          intro i hi
          have : i = 0 := by simpa using hi
          subst i
          exact row.down.2⟩⟩
    | i + 1, hi => do
        let table ← buildTable source target i (by omega)
        let up : Row target.size :=
          ⟨⟨table.down.1[i]'(by rw [table.down.2.1]; omega),
            table.down.2.2 i (by rw [table.down.2.1]; omega)⟩⟩
        let row ← buildRow (source[i]'(by omega)) target up (i + 1)
          target.size (by omega)
        pure ⟨⟨table.down.1.push row.down.1, by simp [table.down.2.1], by
          intro k hk
          rw [Array.getElem_push]
          split
          · exact table.down.2.2 _ _
          · exact row.down.2⟩⟩
  let rec @[reducible] reconstruct (source target : Array α)
      (table : Table source.size target.size) :
      (i j : Nat) → i ≤ source.size → j ≤ target.size →
        EditScript α → TimeM EditDistanceCost (EditScript α)
    | 0, 0, _, _, accumulator => pure accumulator
    | 0, j + 1, hi, hj, accumulator => do
        TimeM.tick ⟨0, 1⟩
        reconstruct source target table 0 j hi (by omega)
          (.insert (target[j]'(by omega)) :: accumulator)
    | i + 1, 0, hi, hj, accumulator => do
        TimeM.tick ⟨0, 1⟩
        reconstruct source target table i 0 (by omega) hj
          (.delete (source[i]'(by omega)) :: accumulator)
    | i + 1, j + 1, hi, hj, accumulator => do
        TimeM.tick ⟨0, 1⟩
        let sourceValue := source[i]'(by omega)
        let targetValue := target[j]'(by omega)
        let diagonal := cell table i j (by omega) (by omega) +
          diagonalCost sourceValue targetValue
        let deletion := cell table i (j + 1) (by omega) hj + 1
        let insertion := cell table (i + 1) j hi (by omega) + 1
        if diagonal ≤ deletion ∧ diagonal ≤ insertion then
          reconstruct source target table i j (by omega) (by omega)
            (diagonalStep sourceValue targetValue :: accumulator)
        else if deletion ≤ insertion then
          reconstruct source target table i (j + 1) (by omega) hj
            (.delete sourceValue :: accumulator)
        else
          reconstruct source target table (i + 1) j hi (by omega)
            (.insert targetValue :: accumulator)
  termination_by i j _ _ _ => i + j
  do
    let sourceArray := source.toArray
    let targetArray := target.toArray
    let table ← buildTable sourceArray targetArray sourceArray.size (by omega)
    let script ← reconstruct sourceArray targetArray table sourceArray.size targetArray.size
      (by omega) (by omega) []
    pure {
      distance := cell table sourceArray.size targetArray.size (by omega) (by omega)
      script := script }

Uses 4 · Used by 14

Statement usesEdit-distance cost counters · Edit-distance result record · Edit script · Edit step

Used byTable cost of the edit distance algorithm · Symmetry · Edit distance vanishes only on equal lists · Minimality of the computed edit distance · Edit distance from the empty list · Edit distance to the empty list · Edit distance between distinct lists is positive · Reconstruction cost of the edit distance algorithm · Reconstruction cost bound for edit distance · Correctness of the returned edit script · The returned edit script realizes the distance · Edit distance of a list to itself · Running time of the edit distance algorithm · The triangle inequality

TheoremCorrectness of the returned edit script#✓fully proved

For lists \(s\) and \(t\) over a type whose Boolean equality test agrees with equality, the edit script returned by the edit distance algorithm on \(s\) and \(t\) transforms \(s\) into \(t\).

theorem editDistance_script_applies [BEq α] [LawfulBEq α] (source target : List α) :
    (editDistance source target).ret.script.Transforms source target

Uses 9 · Used by 2

Statement usesEdit-distance cost counters · Edit-distance result record · Edit script · An edit script transforming one list into another · Edit distance algorithm

Proof usesRunning an edit script · Cost of an edit script · Edit step · Unit cost of an edit step

Used bySymmetry · The triangle inequality

TheoremThe returned edit script realizes the distance#✓fully proved

For lists \(s\) and \(t\) over a type with a Boolean equality test, the unit cost of the edit script returned by the edit distance algorithm on \(s\) and \(t\) equals the distance it returns.

theorem editDistance_script_cost [BEq α] (source target : List α) :
    (editDistance source target).ret.script.cost =
      (editDistance source target).ret.distance

Uses 7 · Used by 3

Statement usesEdit-distance cost counters · Edit-distance result record · Edit script · Cost of an edit script · Edit distance algorithm

Proof usesEdit step · Unit cost of an edit step

Used bySymmetry · Edit distance vanishes only on equal lists · The triangle inequality

TheoremMinimality of the computed edit distance#✓fully proved

Let \(s\) and \(t\) be lists over a type whose Boolean equality test agrees with equality. Every edit script that transforms \(s\) into \(t\) has unit cost at least the distance returned by the edit distance algorithm on \(s\) and \(t\).

theorem editDistance_minimal [BEq α] [LawfulBEq α]
    (source target : List α) (script : EditScript α) :
    script.Transforms source target →
      (editDistance source target).ret.distance ≤ script.cost

Uses 9 · Used by 2

Statement usesEdit-distance cost counters · Edit-distance result record · Edit script · An edit script transforming one list into another · Cost of an edit script · Edit distance algorithm

Proof usesRunning an edit script · Edit step · Unit cost of an edit step

Used bySymmetry · The triangle inequality

TheoremEdit distance from the empty list#✓fully proved

For every list \(t\) over a type with a Boolean equality test, the distance returned by the edit distance algorithm from the empty list to \(t\) is the length of \(t\).

theorem editDistance_nil_left [BEq α] (target : List α) :
    (editDistance [] target).ret.distance = target.length

Uses 3

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

TheoremEdit distance to the empty list#✓fully proved

For every list \(s\) over a type with a Boolean equality test, the distance returned by the edit distance algorithm from \(s\) to the empty list is the length of \(s\).

theorem editDistance_nil_right [BEq α] (source : List α) :
    (editDistance source []).ret.distance = source.length

Uses 3

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

TheoremEdit distance of a list to itself#✓fully proved

For every list \(s\) over a type whose Boolean equality test agrees with equality, the distance returned by the edit distance algorithm from \(s\) to \(s\) is \(0\).

theorem editDistance_self [BEq α] [LawfulBEq α] (source : List α) :
    (editDistance source source).ret.distance = 0

Uses 3 · Used by 1

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Used byEdit distance vanishes only on equal lists

TheoremEdit distance vanishes only on equal lists#✓fully proved

For lists \(s\) and \(t\) over a type whose Boolean equality test agrees with equality, the distance returned by the dynamic-programming edit distance algorithm on \(s\) and \(t\) is \(0\) if and only if \(s = t\).

theorem editDistance_eq_zero_iff [BEq α] [LawfulBEq α] (source target : List α) :
    (editDistance source target).ret.distance = 0 ↔ source = target

Uses 9 · Used by 1

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Proof usesEdit script · Cost of an edit script · Edit step · Unit cost of an edit step · The returned edit script realizes the distance · Edit distance of a list to itself

Used byEdit distance between distinct lists is positive

TheoremTable cost of the edit distance algorithm#✓fully proved

For lists \(s\) and \(t\) over a type with a Boolean equality test, write \(|s|\) and \(|t|\) for their lengths. The number of table-cell transitions charged by the dynamic-programming edit distance algorithm on \(s\) and \(t\) is exactly \((|s| + 1)(|t| + 1)\), one per pair of a prefix of \(s\) and a prefix of \(t\).

theorem editDistance_cellTransitions [BEq α] (source target : List α) :
    (editDistance source target).time.cellTransitions =
      (source.length + 1) * (target.length + 1)

Uses 7 · Used by 1

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Proof usesEdit script · Cost of an edit script · Edit step · Unit cost of an edit step

Used byRunning time of the edit distance algorithm

TheoremReconstruction cost of the edit distance algorithm#✓fully proved

For lists \(s\) and \(t\) over a type with a Boolean equality test, the number of reconstruction steps charged by the edit distance algorithm on \(s\) and \(t\) equals the length of the edit script it returns.

theorem editDistance_reconstructionSteps [BEq α] (source target : List α) :
    (editDistance source target).time.reconstructionSteps =
      (editDistance source target).ret.script.length

Uses 7 · Used by 2

Statement usesEdit-distance cost counters · Edit-distance result record · Edit script · Edit step · Edit distance algorithm

Proof usesCost of an edit script · Unit cost of an edit step

Used byReconstruction cost bound for edit distance · Running time of the edit distance algorithm

TheoremReconstruction cost bound for edit distance#✓fully proved

For lists \(s\) and \(t\) over a type with a Boolean equality test, write \(|s|\) and \(|t|\) for their lengths. The number of reconstruction steps charged by the edit distance algorithm on \(s\) and \(t\) is at most \(|s| + |t|\).

theorem editDistance_reconstructionSteps_le [BEq α] (source target : List α) :
    (editDistance source target).time.reconstructionSteps ≤ source.length + target.length

Uses 8

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Proof usesEdit script · Cost of an edit script · Edit step · Unit cost of an edit step · Reconstruction cost of the edit distance algorithm

TheoremRunning time of the edit distance algorithm#✓fully proved

For lists \(s\) and \(t\) over a type with a Boolean equality test, the total number of events charged by the edit distance algorithm on \(s\) and \(t\), that is its cell transitions plus its reconstruction steps, equals \((|s| + 1)(|t| + 1) + k\), where \(k\) is the length of the edit script it returns.

theorem editDistance_time [BEq α] (source target : List α) :
    (editDistance source target).time.total =
      (source.length + 1) * (target.length + 1) +
        (editDistance source target).ret.script.length

Uses 8

Statement usesEdit-distance cost counters · Total edit-distance cost · Edit-distance result record · Edit script · Edit step · Edit distance algorithm

Proof usesTable cost of the edit distance algorithm · Reconstruction cost of the edit distance algorithm

TheoremEvery edit script has an inverse of the same cost#✓fully proved

Every script has an inverse of the same cost (swap insertions and deletions, reverse substitutions).

theorem EditScript.exists_inverse [BEq α] [LawfulBEq α] {script : EditScript α}
    {source target : List α} (h : script.Transforms source target) :
    ∃ inverse : EditScript α, inverse.Transforms target source ∧
      inverse.cost = script.cost

Uses 5 · Used by 1

Statement usesEdit script · An edit script transforming one list into another · Cost of an edit script

Proof usesRunning an edit script · Edit step

Used bySymmetry

TheoremComposition of edit scripts is subadditive in cost#✓fully proved

Two scripts compose into one whose cost is at most the sum of their costs.

theorem EditScript.exists_compose [BEq α] [LawfulBEq α] {first second : EditScript α}
    {source middle target : List α} (h₁ : first.Transforms source middle)
    (h₂ : second.Transforms middle target) :
    ∃ composed : EditScript α, composed.Transforms source target ∧
      composed.cost ≤ first.cost + second.cost

Uses 5 · Used by 1

Statement usesEdit script · An edit script transforming one list into another · Cost of an edit script

Proof usesRunning an edit script · Edit step

Used byThe triangle inequality

TheoremSymmetry#✓fully proved

Symmetry of unit-cost edit distance.

theorem editDistance_comm [BEq α] [LawfulBEq α] (x y : List α) :
    (editDistance x y).ret.distance = (editDistance y x).ret.distance

Uses 10

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Proof usesEdit script · An edit script transforming one list into another · Cost of an edit script · Every edit script has an inverse of the same cost · Minimality of the computed edit distance · Correctness of the returned edit script · The returned edit script realizes the distance

TheoremThe triangle inequality#✓fully proved

The triangle inequality for unit-cost edit distance.

theorem editDistance_triangle [BEq α] [LawfulBEq α] (x y z : List α) :
    (editDistance x z).ret.distance ≤
      (editDistance x y).ret.distance + (editDistance y z).ret.distance

Uses 10

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Proof usesEdit script · An edit script transforming one list into another · Cost of an edit script · Composition of edit scripts is subadditive in cost · Minimality of the computed edit distance · Correctness of the returned edit script · The returned edit script realizes the distance

TheoremEdit distance between distinct lists is positive#✓fully proved

Distinct lists are at positive distance.

theorem editDistance_pos_iff [BEq α] [LawfulBEq α] (x y : List α) :
    0 < (editDistance x y).ret.distance ↔ x ≠ y

Uses 4

Statement usesEdit-distance cost counters · Edit-distance result record · Edit distance algorithm

Proof usesEdit distance vanishes only on equal lists

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.