Status: ✅ Complete
Coq File: rocq/liblevenshtein/Core.v
Date: 2025-11-17
Authors: Formal Verification Team
This document provides comprehensive documentation for the three foundational properties of the subsumption relation $(\sqsubseteq )$ used in Levenshtein automata for state minimization. These properties establish that subsumption forms a strict partial order, which is essential for maintaining anti-chain states.
In Levenshtein automata, states consist of sets of positions. As the automaton processes input, the number of positions can grow exponentially. Subsumption provides a mathematical foundation for removing redundant positions:
p_{1} \sqsubseteq p_{2}),$ then p₂ is redundantThe three theorems proven here ensure this minimization is:
\mathcal{O}(n^{2})$ state size boundRecord Position : Type := mkPosition {
variant : PositionVariant; (* Type: I/M/Transposing/Splitting *)
offset : Z; (* Position in term *)
errors : nat; (* Remaining error budget *)
max_distance : nat; (* Maximum allowed distance *)
entry_char : option ascii (* For multi-step operations *)
}.
Geometric Interpretation: A position (offset, errors) represents a location in the edit graph with a reachable region R = Manhattan ball of radius (max_distance - errors).
Definition subsumes_core (offset1 : Z) (errors1 : nat)
(offset2 : Z) (errors2 : nat) : Prop :=
(errors2 > errors1)%nat /\
Z.abs (offset2 - offset1) <= Z.of_nat (errors2 - errors1).
Definition subsumes (p1 p2 : Position) : Prop :=
variant p1 = variant p2 /\
subsumes_core (offset p1) (errors p1) (offset p2) (errors p2).
Notation "p1 '⊑' p2" := (subsumes p1 p2) (at level 70).
Informal Definition: Position p₁ subsumes p₂ if:
\lvert \text{offset}_2 - \text{offset}_1\rvert \le \text{errors}_2 - \text{errors}_1$Geometric Meaning: The reachable region R(p₂) is contained within R(p₁):
R(p₂) ⊆ R(p₁) ⟺ p₁ ⊑ p₂
No position subsumes itself.
A position cannot be redundant with respect to itself. This is the foundation of the strict ordering property.
Theorem subsumes_irreflexive : forall p, ~ (p ⊑ p).
English: For all positions p, it is not the case that p subsumes p.
The subsumption relation requires errors₂ > errors₁. For $p \sqsubseteq p,$ we would need errors(p) > errors(p), which is impossible since a natural number cannot be strictly greater than itself.
This is an immediate consequence of the strict inequality in the definition.
Type: Proof by contradiction
Steps:
p \sqsubseteq p$ for some position pProof.
intros p [_ [Hcontr _]].
(* subsumes_core requires errors p > errors p *)
lia. (* Contradiction: n > n is impossible *)
Qed.
Tactics Used:
intros: Introduce hypothesis and destructlia: Linear integer arithmetic solver (recognizes n > n as false)Rust code: src/transducer/generalized/subsumption.rs:80-150
This theorem ensures that when checking if positions subsume each other during state minimization, we never incorrectly remove a position by comparing it to itself. While obvious, it's a crucial sanity check for the formalization.
Practical consequence: The anti-chain maintenance code can safely use strict inequality:
if subsumes(existing, &pos, max_distance) {
return; // pos is redundant
}
This will never trigger when existing == pos (pointer equality), and our theorem proves it won't trigger for value equality either.
If p₁ subsumes p₂, and p₂ subsumes p₃, then p₁ subsumes p₃.
Subsumption chains compose: if p₂ is redundant with respect to p₁, and p₃ is redundant with respect to p₂, then p₃ is redundant with respect to p₁.
Theorem subsumes_transitive : forall p1 p2 p3,
p1 ⊑ p2 -> p2 ⊑ p3 -> p1 ⊑ p3.
Geometric interpretation: If $R(p_{2}) \subseteq R(p_{1})$ and $R(p_{3}) \subseteq R(p_{2}),$ then $R(p_{3}) \subseteq R(p_{1})$ by set containment transitivity.
Algebraic reasoning:
|o_{3} - o_{1}| \le |o_{3} - o_{2}| + |o_{2} - o_{1}|$|o_{3} - o_{1}| \le |o_{3} - o_{2}| + |o_{2} - o_{1}| \le (e_{3} - e_{2}) + (e_{2} - e_{1}) = e_{3} - e_{1}$The key insight is that Manhattan distance satisfies the triangle inequality, and error gaps are additive, so containment chains compose naturally.
Type: Constructive proof using arithmetic properties
Steps:
Variant equality: Show variant(p₁) = variant(p₃)
Error gap: Show errors(p₃) > errors(p₁)
Offset bound: Show $\lvert \text{offset}(p_3) - \text{offset}(p_1)\rvert \le \text{errors}(p_3) - \text{errors}(p_1)$
|o₃ - o₁| ≤ |o₃ - o₂| + |o₂ - o₁|
|o₃ - o₂| ≤ e₃ - e₂ (from p₂ ⊑ p₃)
|o₂ - o₁| ≤ e₂ - e₁ (from p₁ ⊑ p₂)
|o₃ - o₁| ≤ (e₃ - e₂) + (e₂ - e₁)
(e₃ - e₂) + (e₂ - e₁) = e₃ - e₁
Proof.
intros p1 p2 p3
[Hv12 [He12 Ho12]] (* Assumptions from p1 ⊑ p2 *)
[Hv23 [He23 Ho23]]. (* Assumptions from p2 ⊑ p3 *)
unfold subsumes, subsumes_core.
(* Step 1: Variant transitivity *)
split.
{ rewrite Hv12. exact Hv23. } (* variant(p1) = variant(p2) = variant(p3) *)
(* Step 2: Error transitivity *)
split.
{ lia. } (* e₃ > e₂ ∧ e₂ > e₁ ⟹ e₃ > e₁ *)
(* Step 3: Offset bound by triangle inequality *)
assert (Htri : Z.abs (offset p3 - offset p1) <=
Z.abs (offset p3 - offset p2) + Z.abs (offset p2 - offset p1)).
{ replace (offset p3 - offset p1)
with ((offset p3 - offset p2) + (offset p2 - offset p1)) by lia.
apply Z.abs_triangle. }
(* Combine with assumptions *)
assert (Hsum : Z.abs (offset p3 - offset p2) + Z.abs (offset p2 - offset p1) <=
Z.of_nat (errors p3 - errors p2) + Z.of_nat (errors p2 - errors p1)).
{ assert (Z.abs (offset p3 - offset p2) <= Z.of_nat (errors p3 - errors p2)) by exact Ho23.
assert (Z.abs (offset p2 - offset p1) <= Z.of_nat (errors p2 - errors p1)) by exact Ho12.
lia. }
(* Simplify sum of gaps *)
assert (Hsimpl : Z.of_nat (errors p3 - errors p2) + Z.of_nat (errors p2 - errors p1) =
Z.of_nat (errors p3 - errors p1)).
{ assert (Hgap: (errors p3 - errors p2 + (errors p2 - errors p1) = errors p3 - errors p1)%nat). {
lia. (* Arithmetic on natural numbers *)
}
rewrite <- Hgap.
rewrite Nat2Z.inj_add. (* Z.of_nat distributes over addition *)
reflexivity. }
(* Chain all inequalities *)
rewrite Hsimpl in Hsum.
lia. (* |o₃-o₁| ≤ Htri ≤ Hsum = e₃-e₁ *)
Qed.
Z.abs_triangle: Z.abs (a + b) <= Z.abs a + Z.abs b
Nat2Z.inj_add: Z.of_nat (m + n) = Z.of_nat m + Z.of_nat n
lia: Linear Integer Arithmetic decision procedure
+, -, \le , <, =$Rust code: src/transducer/generalized/state.rs:89-130
Transitivity is critical for anti-chain maintenance. When adding a new position, we check:
// If new position is subsumed by ANY existing position, discard it
for existing in &self.positions {
if subsumes(existing, &pos, self.max_distance) {
return; // pos is redundant
}
}
// If new position subsumes ANY existing positions, remove them
self.positions.retain(|existing| {
!subsumes(&pos, existing, self.max_distance)
});
Without transitivity, this algorithm could fail:
p_{1} \sqsubseteq p_{2}$ and $p_{2} \sqsubseteq p_{3}$Complexity impact: Transitivity justifies the $\mathcal{O}(|Q|^{2})$ subsumption check complexity, where |Q| = $\mathcal{O}(n^{2})$. Without transitivity, we might need to maintain full subsumption closure, which could be exponential.
Error budget (vertical) vs Offset (horizontal):
e=3 | p₁ (o=0, e=3)
| |
| |
e=2 | +------- p₂ (o=1, e=2)
| |
| |
e=1 | +------- p₃ (o=2, e=1)
|
e=0 +--------------------------------
o=0 o=1 o=2 o=3
Reachable regions (Manhattan balls):
- R(p₁) = {(o,e) : |o-0| ≤ 3-3} = radius 0 at o=0 ... wait, errors=3 means budget=3
Actually, let me correct this:
- R(p₁) = {positions reachable with 3 errors from o=0}
- R(p₂) = {positions reachable with 2 errors from o=1}
- R(p₃) = {positions reachable with 1 error from o=2}
Check subsumption:
- p₁ ⊑ p₂? : e₂(2) > e₁(3)? NO ✗
Let me use a correct example:
Corrected Example:
e=3 | p₃ (o=0, e=3)
| |
| |
e=2 | p₂ (o=-1, e=2)
| | |
| | |
e=1 | p₁ (o=0, e=1) |
| | |
e=0 +-------------------------
o=-2 o=-1 o=0 o=1
Check p₁ ⊑ p₂:
- Variant: Same ✓
- e₂ > e₁: 2 > 1 ✓
- |o₂ - o₁| ≤ e₂ - e₁: |-1 - 0| = 1 ≤ 2-1 = 1 ✓
Result: p₁ ⊑ p₂ ✓
Check p₂ ⊑ p₃:
- Variant: Same ✓
- e₃ > e₂: 3 > 2 ✓
- |o₃ - o₂| ≤ e₃ - e₂: |0 - (-1)| = 1 ≤ 3-2 = 1 ✓
Result: p₂ ⊑ p₃ ✓
Check p₁ ⊑ p₃ (by transitivity):
- Variant: Same ✓
- e₃ > e₁: 3 > 1 ✓
- |o₃ - o₁| ≤ e₃ - e₁: |0 - 0| = 0 ≤ 3-1 = 2 ✓
Result: p₁ ⊑ p₃ ✓
Geometric: R(p₁) ⊇ R(p₂) ⊇ R(p₃), so R(p₁) ⊇ R(p₃) by set containment.
Positions with different variants cannot subsume each other.
Position types (I vs M, or base vs transposing/splitting) represent fundamentally different automaton states. A position of one type can never make a position of a different type redundant.
Theorem subsumes_variant_restriction : forall p1 p2,
variant p1 <> variant p2 -> ~ (p1 ⊑ p2).
English: For all positions p₁ and p₂, if their variants differ, then p₁ does not subsume p₂.
This is a definitional property. The subsumption relation explicitly requires variant equality as its first conjunct:
Definition subsumes (p1 p2 : Position) : Prop :=
variant p1 = variant p2 /\ (* ← This line *)
subsumes_core (offset p1) (errors p1) (offset p2) (errors p2).
If variants differ, the first conjunct is false, so the entire conjunction is false.
Why this makes sense:
Type: Proof by contradiction (immediate)
Steps:
\text{variant}(p_1) \ne \text{variant}(p_2)$p_{1} \sqsubseteq p_{2}$Proof.
intros p1 p2 Hneq [Heq _].
(* subsumes requires variant equality (Heq) *)
(* but Hneq says variants differ *)
contradiction.
Qed.
Tactics Used:
intros: Introduce hypotheses and destruct subsumptioncontradiction: Automatically finds Heq and Hneq contradictRust code: src/transducer/generalized/subsumption.rs:143-148
pub fn subsumes(pos1: &GeneralizedPosition, pos2: &GeneralizedPosition,
max_distance: u8) -> bool {
use GeneralizedPosition::*;
// Core check function (same as subsumes_core in Coq)
fn check_subsumption(i: i32, e: u8, j: i32, f: u8) -> bool {
f > e && (j - i).abs() <= (f - e) as i32
}
match (pos1, pos2) {
(INonFinal { offset: i, errors: e },
INonFinal { offset: j, errors: f }) =>
check_subsumption(*i, *e, *j, *f),
(MFinal { offset: i, errors: e },
MFinal { offset: j, errors: f }) =>
check_subsumption(*i, *e, *j, *f),
// ... similar for other same-variant pairs
_ => false, // ← Enforces variant restriction
}
}
The match statement's catch-all _ => false directly implements this theorem.
Performance optimization: This theorem justifies an early-exit optimization:
if std::mem::discriminant(pos1) != std::mem::discriminant(pos2) {
return false; // Fast path: different variants
}
// Only check numeric conditions if variants match
This reduces subsumption checks from $\mathcal{O}(1)$ to $\mathcal{O}(0)$ for mismatched variants (just a discriminant comparison, no arithmetic).
State minimization impact: Anti-chain maintenance preserves all six variant types:
| Variant | Purpose | Preserved? |
|---|---|---|
| INonFinal | Base I-type position | ✓ Always |
| MFinal | Base M-type position | ✓ Always |
| ITransposing | Mid-transposition (I) | ✓ Always |
| MTransposing | Mid-transposition (M) | ✓ Always |
| ISplitting | Mid-split phonetic (I) | ✓ Always |
| MSplitting | Mid-split phonetic (M) | ✓ Always |
Without this theorem, we might incorrectly think an I-type position can subsume an M-type, leading to incorrect acceptance behavior.
While not directly used in the codebase, anti-symmetry is a standard property of partial orders and follows from irreflexivity + transitivity.
Theorem subsumes_antisymmetric : forall p1 p2,
p1 ⊑ p2 -> p2 ⊑ p1 -> False.
English: It is impossible for p₁ to subsume p₂ while p₂ also subsumes p₁.
If $p_{1} \sqsubseteq p_{2}$ and $p_{2} \sqsubseteq p_{1},$ then by transitivity, $p_1 \sqsubseteq p_1$, contradicting irreflexivity.
Proof.
intros p1 p2 H12 H21.
(* By transitivity: p1 ⊑ p2 ⊑ p1 implies p1 ⊑ p1 *)
assert (Hcontr : p1 ⊑ p1).
{ apply (subsumes_transitive p1 p2 p1); assumption. }
(* But subsumption is irreflexive *)
apply (subsumes_irreflexive p1).
exact Hcontr.
Qed.
Anti-symmetry confirms that subsumption has no cycles. This is important for:
Primary file: src/transducer/generalized/subsumption.rs
Key functions:
subsumes() function (implements subsumption check)Primary file: rocq/liblevenshtein/Core.v
Key definitions:
subsumes_core (arithmetic conditions)subsumes (full relation with variant check)subsumes_irreflexive (Theorem 1)subsumes_transitive (Theorem 2)subsumes_variant_restriction (Theorem 3)subsumes_antisymmetric (derived property)| Property | Coq Theorem | Rust Implementation | Status |
|---|---|---|---|
| Variant equality | variant p1 = variant p2 | match (pos1, pos2) | ✓ Exact match |
| Error gap | errors2 > errors1 | f > e | ✓ Exact match |
| Offset bound | Z.abs(o2-o1) <= e2-e1 | (j-i).abs() <= (f-e) | ✓ Exact match |
| Irreflexivity | Theorem proven | Implicit in f > e | ✓ Guaranteed |
| Transitivity | Theorem proven | Implicit in algorithm | ✓ Relies on proof |
| Variant restriction | Theorem proven | _ => false pattern | ✓ Enforced |
✅ Fully verified: The Coq proofs compiled successfully, establishing:
🔄 Implementation correspondence: The Rust code structurally matches the Coq definition. Future work includes:
Prove that position constructors maintain invariants:
new_i(offset, errors, n) produces valid I-type positionnew_m(offset, errors, n) produces valid M-type positionFile: rocq/liblevenshtein/Invariants.v
Formalize and prove correctness of standard edit operations:
File: rocq/liblevenshtein/Operations.v, Transitions.v
Extend to transposition and merge operations:
Defer: Split operations (phonetic, Phase 3b) for later
Prove the add_position algorithm maintains anti-chain property:
File: rocq/liblevenshtein/State.v
Compare proven specification with Rust implementation:
Primary: docs/research/weighted-levenshtein-automata/README.md
Lemma 3.1 (Subsumption Correctness): Geometric justification for the definition
Lemma 3.2 (Subsumption Transitivity): Edit graph path composition
Lemma 4.5 (State Size Bound): $\mathcal{O}(n^{2})$ positions per state
src/transducer/generalized/position.rssrc/transducer/generalized/subsumption.rssrc/transducer/generalized/state.rssrc/transducer/generalized/automaton.rs:1200-1700Z (Integers): Stdlib.ZArith
Z.abs: Absolute valueZ.abs_triangle: Triangle inequality lemmaZ.of_nat: Conversion from nat to Znat (Natural numbers): Stdlib.Arith
Nat.ltb: Boolean less-than testNat2Z.inj_add: Additive homomorphismlia: Linear Integer Arithmetic decision procedure
+, -, \le , <, =$ for both Z and natEnd of Document
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |