LevenshteinEstimator'.distances_eq
theorem LevenshteinEstimator'.distances_eq :
∀ {α β δ : Type} [inst : CanonicallyLinearOrderedAddCommMonoid δ] {C : Levenshtein.Cost α β δ} {xs : List α}
{ys : List β} (self : LevenshteinEstimator' C xs ys), self.distances = suffixLevenshtein C xs self.suff
This theorem verifies that the `distances` field of a `LevenshteinEstimator'` object is correctly calculated. In particular, for any types `α`, `β`, and `δ`, where `δ` is a canonically linear ordered additive commutative monoid, given a cost function `C` for calculating the Levenshtein distance between elements of type `α` and `β`, a list `xs` of elements of `α`, a list `ys` of elements of `β`, and a `LevenshteinEstimator'` object `self` constructed with `C`, `xs`, and `ys`, the `distances` field of `self` is equal to the computation of the suffix Levenshtein distances between `xs` and the suffixes of `ys` according to `C`.
More concisely: For any type `α`, `β`, and additively commutative monoid `δ`, given a cost function `C` for Levenshtein distance between `α` and `β`, a list `xs` of `α`, a list `ys` of `β`, and a `LevenshteinEstimator'` object `self` built with `C`, `xs`, and `ys`, the `distances` field of `self` equals the sequence of suffix Levenshtein distances of `xs` against the suffixes of `ys` according to `C`.
|
LevenshteinEstimator'.split
theorem LevenshteinEstimator'.split :
∀ {α β δ : Type} [inst : CanonicallyLinearOrderedAddCommMonoid δ] {C : Levenshtein.Cost α β δ} {xs : List α}
{ys : List β} (self : LevenshteinEstimator' C xs ys), self.pre_rev.reverse ++ self.suff = ys
This theorem asserts that for any given types `α`, `β`, and `δ`, and for any instance of the canonically linearly ordered additive commutative monoid on `δ`, and given a cost function `C` from `Levenshtein.Cost` over `α`, `β`, and `δ`, and for any lists `xs` and `ys` of types `α` and `β` respectively, for any `LevenshteinEstimator'` over these parameters, the reverse of `pre_rev` concatenated with `suff` gives `ys`. In essence, it is verifying that `ys` can be split into a prefix (reverse of `pre_rev`) and a suffix (`suff`).
More concisely: For any types `α`, `β`, additively commutative monoid `δ` with a linear order, cost function `C` from `Levenshtein.Cost`, and lists `xs: list α` and `ys: list β`, there exists `pre_rev: list α` and `suff: list β` such that `reverse pre_rev ++ suff` equals `ys`, where `++` represents list concatenation.
|
LevenshteinEstimator'.bound_eq
theorem LevenshteinEstimator'.bound_eq :
∀ {α β δ : Type} [inst : CanonicallyLinearOrderedAddCommMonoid δ] {C : Levenshtein.Cost α β δ} {xs : List α}
{ys : List β} (self : LevenshteinEstimator' C xs ys),
self.bound =
match self.pre_rev, ⋯ with
| [], split => ((↑self.distances)[0], ys.length)
| x, split => (List.minimum_of_length_pos ⋯, self.suff.length)
The theorem `LevenshteinEstimator'.bound_eq` states that for any types α, β, δ, where δ is a canonically linearly ordered additive commutative monoid, and any Levenshtein cost function `C` from α to β mapped to δ, and any lists `xs` of type α and `ys` of type β, the Levenshtein estimator's bound is determined as follows: if the reversed prefix (`self.pre_rev`) of the estimator is an empty list, the bound is a pair consisting of the first element of the 'distances' list (casted to δ) and the length of list `ys`. If the reversed prefix is not empty, the bound is a pair consisting of the minimum value in a certain list (determined by `List.minimum_of_length_pos`) and the length of the 'sufficient' part of the estimator (`self.suff.length`).
More concisely: The Levenshtein estimator's bound is given by the minimum distance in the list of distances up to the sufficient prefix length, or the first distance and the length of the second list if the prefix is empty.
|