Getting Levenshtein right

On day 9, we looked at edits as a way to talk about how related two strings were---in particular, strands of DNA bases. We made a variety of assertions: that our various edit-producing functions were "correct", i.e., produced valid edits; that sub_edit produced edits no more expensive than naive_sub_edit; that levenshtein produces edits that were "optimal", often much better than even sub_edit. Let's substantiate those claims!

Edit-generating functions

First, let's look at our edit-producing functions.

The delete_add_edit approach is the simplest way to find edits from one strand to another: erase the first one entirely, then write in the second.

This one's new! It produces edits from a strand to itself. We'll need it in the proof of correctness for levenshtein.

The naive_sub_edit approach is a bit better than delete_add_edit, using substitute instead of deletes and adds.

And sub_edit is still better, using copy when it can.

But levenshtein's "choose the best" approach will be optimal. Here's our definition.

Proving validity

Let's prove each of them valid. But what does that mean? Some edits are valid for a given src and tgt strand when applying the edits to src with apply_edits yields the tgt strand.

We could have worked propositionally here, saying:

The eq_strand_iff lemma lets us know that valid_edit and valid_edit' are equivalent. The proofs turn out ot be marginally easier using valid_edit's approach, so let's stick with that.

Exercise: 1 star, standard (delete_edit_valid)

Exercise: 1 star, standard (add_edit_valid)

Exercise: 1 star, standard (copy_edit_valid)

Exercise: 2 stars, standard (delete_add_valid)

This one is the hardest so far. You ought to be able to simply combine delete_edit_valid and add_edit_valid, but it doesn't quite work. (Try it and see!) That said, a simple proof can do the trick here, or you can prove a helper and prove `delete_add_valid` without any direct induction.

So much for those simpler edit-generating functions. Let's work on some more complex ones.

Exercise: 2 stars, standard (naive_sub_edit_valid)

Exercise: 2 stars, standard (sub_edit_valid)

Prove that sub_edit produces valid edits.

Proving Levenshtein valid

This next lemma will be handy for proving levenshtein_valid.

Exercise: 2 stars, standard, optional (argmin3_valid)

We're finally equipped to prove that Levenshtein's edit distance generates valid edits! You'll want to use Search to find relevant lemmas from before.

Exercise: 3 stars, standard (levenshtein_valid)

A word of warning: you're going to get some pretty complicated terms in your goal! Using unfold/fold in combination will help a bit, but nothing will help quite so much as patient attention. A lot of what's in your goal is noise resulting from the let fix inner, and you can often pay attention only to the front of your goal.

Going the distance

Exercise: 3 stars, standard, optional (costs)

Prove lemmas characterizing the costs of each of our basic edit-generating functions.

Exercise: 3 stars, standard (levenshtein_distance_correct)

Let's define a levenshtein_distance that only computes the edit distance without computing edits themselves--this cost is the real thing we care about, not edits... but it'd be nice to know that the cost that levenshtein_distance produces the right cost, i.e., that it agrees with levenshtein. Let's prove it!

Optimality for Levenshtein edit distance

We've proven that our various edit-finding algorithms are correct. But which is best (for our notion of edit)? Levenshtein edit distance is optimal: it always produces the lowest cost edits possible. Now that we have a notion like ≤, we can prove that!

Exercise: 2 stars, standard (naive_sub_worse)

As a warm up, let's show that sub_edit is better than naive_sub_edit. The intuition here is that sub_edit and naive_sub_edit are more or less identical, except sub_edit sometimes produces a copy edit while naive_sub_edit always produces substitute. Since cost copy = 0 and cost (substitute b) = 1, using sub_edit should never be worse than naive_sub_edit.

Exercise: 2 stars, standard, optional (add_empty_optimal)

For any edits from the empty strand to a given tgt strand, add_edit is optimal. Why? Well, you need to build the whole strand! Hint: the proof should go by induction on edits. You'll need to do some case analysis on the other edit and on tgt.

Exercise: 2 stars, standard, optional (delete_empty_optimal)

Similarly, delete_edit is optimal when editing a strand to empty.

Exercise: 3 stars, standard (levenshtein_optimal)

Prove that levenshtein is optimal. The following lemma will be helpful.

We've given you the structure of this (fairly challenging!) proof. Try not to be intimidated by the large formulae you might be given. Go slow and read everything. If you get confused, use a whiteboard.