Diff and patch correctness: a minimum-cost edit script reconstructs its target
Proof verified
complete
What this target establishes
Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
- Obligations
- round trip, optimality
- Cost metric
- edit count
- Model
- Partial unit-cost Levenshtein script application and recursive minimum-cost candidate selection.
- Assumptions
- Fuel is at least the sum of input lengths. Copy costs zero; replace, delete and insert each cost one.
- Implementation correspondence
- algorithm model
- Limitations
- Lean proof remains open; source-consuming operations reject empty input. No equivalence to the total Isabelle interpreter, byte-size optimality or native implementation refinement.
Porting target for existing verified edit-script results. Isabelle AFP Min_Ed_Dist0 proves min_eds_correct (the generated script reconstructs the target), min_eds_minimal (no successfully applied script is cheaper), and min_ed_min_eds (distance equals script cost). The existing source proof is supplied; a Lean proof of this exact target remains requested.
The entire executable model is included. Edit = Sum (Option Nat) (Option Nat): inl none copies the next symbol, inl (some x) replaces it with x, inr none deletes it, and inr (some x) inserts x. Copy costs zero; other edits cost one. Apply rejects copy/replace/delete on empty input. Finishing the script leaves the unconsumed suffix unchanged. The generator compares replace/delete/insert candidates by complete script cost and copies when the heads agree. Empty-input cases insert or delete the remaining symbols. Fuel at least sourceLength+targetLength prevents truncation.
The conclusions are successful reconstruction and minimum cost against EVERY competing successfully applied script. Neither is a premise. This is unit-cost Levenshtein editing, distinct from insertion/deletion-only LCS distance, encoded bytes or runtime. The Isabelle edit function is total with different out-of-range behavior; this model validates those operations, so the external proof is a guide rather than a directly reusable term. No universal port-equivalence, memoization, Myers correctness or native implementation refinement is claimed. Known-result formalization request prepared with Codex.
Formal statement
(fun (cost : List (Sum (Option Nat) (Option Nat)) → Nat) =>
(fun (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat)) =>
(fun (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat))) =>
(fun (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))) =>
∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
apply (diff fuel xs ys) xs = some ys ∧
∀ script : List (Sum (Option Nat) (Option Nat)), apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script
) (fun fuel => Nat.rec (fun _ _ : List Nat => [])
(fun _ recur xs ys => match xs, ys with
| [], _ => ys.map (fun y => Sum.inr (some y))
| _, [] => List.replicate xs.length (Sum.inr none)
| x :: xt, y :: yt => if x = y then Sum.inl none :: recur xt yt
else best (Sum.inl (some y) :: recur xt yt)
(Sum.inr none :: recur xt ys)
(Sum.inr (some y) :: recur xs yt)) fuel)
) (fun a b c => if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c)
) (fun script => List.rec (fun xs : List Nat => some xs)
(fun edit _ rest xs => match edit, xs with
| .inl none, x :: xt => (rest xt).map (fun ys => x :: ys)
| .inl (some y), _ :: xt => (rest xt).map (fun ys => y :: ys)
| .inr none, _ :: xt => rest xt
| .inr (some y), _ => (rest xs).map (fun ys => y :: ys)
| _, [] => none) script)
) (fun script => script.foldr (fun edit n => match edit with | .inl none => n | _ => n + 1) 0)Lean core · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 8a86b4d6476261560d43f6ea3df9394ba847eb65bf27eb0728f61c014858789d
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.