AlignmentSplitting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Splitting an optimal edit script at a source cut

An arbitrary unrestricted edit script transports a cut through its intermediate strings. Each edit belongs to one side of that cut. Applied to a shortest script, this gives an exact optimal target split, including empty source or target pieces.

theorem OAI.EditApproximation.step_split line 20
theorem OAI.EditApproximation.script_split line 79

theorem OAI.EditApproximation.edit_append_split line 98

Source documentation

A shortest unrestricted edit script admits an exactly optimal split at every source cut.

theorem edit_append_split {α : Type u} (left right target : List α) :
    ∃ targetLeft targetRight, target = targetLeft ++ targetRight ∧
      edit (left ++ right) target = edit left targetLeft + edit right targetRight := by
…

theorem OAI.EditApproximation.edit_partition_split line 116

Source documentation

Repeated source cuts have a common ordered target partition whose piecewise edit costs sum exactly to the parent optimum. Source pieces may be empty. A nonempty list of pieces is needed to assign insertions.

theorem edit_partition_split {α : Type u} (parts : List (List α))
    (hne : parts ≠ []) (target : List α) :
    ∃ targetParts : List (List α), targetParts.length = parts.length ∧
      targetParts.flatten = target ∧
      (List.zipWith edit parts targetParts).sum = edit parts.flatten target := by
…

theorem OAI.EditApproximation.edit_partition_prefix_le line 140

Source documentation

Prefixes of an ordered source/target partition use at most the partition's total edit cost. This bounds every alignment anchor shift.

theorem edit_partition_prefix_le {α : Type u}
    (parts targets : List (List α)) (hlen : parts.length = targets.length) (k : ℕ) :
    edit (parts.take k).flatten (targets.take k).flatten ≤
      (List.zipWith edit parts targets).sum := by
…

theorem OAI.EditApproximation.optimal_partition_anchor_shift_bound line 165