Liking cljdoc? Tell your friends :D

Automaton Proofs Status

Current Status Date: May 26, 2026 Build Status: Compiles successfully under the focused formal runner

Current Live Status

The source-level admission scan is clean for the automaton Coq files: there are no active Admitted., admit., Axiom, or Parameter declarations in the current automaton proof surface.

The automaton evidence debt has been retired. In the automaton files, ./scripts/verify-formal.sh audit-evidence-tsv no longer reports AutomatonCompletenessCoreEvidence or any automaton *Evidence record. Transposition completeness is now proved directly from the executable Damerau recurrence, and MergeAndSplit soundness/completeness no longer exposes record fields at the public theorem boundary.

Recent local progress that retired the Standard representation evidence:

Exact same-index containment was replaced by executable Standard subsumption; standard_exact_positions_contain_counterexample documents why exact containment is false.
Empty-prefix representation is proved by position_subsumed_from_empty_run.
Delete-successor representation arithmetic is factored through subsumes_standard_delete_successor_chain, including the final-position case where non-final representatives cannot directly subsume final positions.
Insert representation through a Standard transition is now factored through subsumes_standard_insert_successor and transition_state_standard_represents_insert_represented.
The same represented-insert step is lifted to the can-complete invariant by transition_state_standard_preserves_can_complete_insert_represented.
Standard completeness is now proved unconditionally via the state_has_completable invariant and automaton_complete_standard_can_complete; the public Standard correctness theorem no longer consumes AutomatonCompletenessCoreEvidence.
Transposition completeness is now proved unconditionally by transposition_reachable_final and automaton_complete_transposition; the public Transposition correctness theorem no longer consumes AutomatonCompletenessCoreEvidence.
The executable delete-prefix case query = "ab", dict = "b", max_dist = 1 is covered by a focused Rust regression test.

The historical notes below are retained for context only.

Update (2026-05-24): this is historical status. The false exact fold-state correspondence path has since been removed: automaton_run_step_std_trans, automaton_run_std_trans_correspondence, automaton_run_step_std_ms, automaton_run_std_ms_correspondence, and AutomatonFoldStateEvidence no longer exist in Completeness.v. The Standard exact-match transition-success bridge is also now proved from containment and Standard run invariants, so no transition-success field remains in the old core completeness evidence. The MergeAndSplit transition has since been restored to the generic 2-to-1/1-to-2 semantics used by the Rust merge_and_split_distance implementation, and automaton soundness no longer needs an evidence record. The exact same-index position_contained_from_run bridge was replaced by position_subsumed_from_run, matching Standard antichain subsumption; Completeness.v contains a concrete counterexample for the old exact-containment shape. Use docs/verification/PROOF_COMPLETION_PLAN.md and ./scripts/verify-formal.sh audit-evidence-tsv for the current gap list.

Historical Summary

The Automaton verification module contains proofs for soundness and completeness of Levenshtein automata supporting three algorithms: Standard, Transposition (Damerau), and Merge/Split. The admitted-lemma counts below are historical notes from the pre-cleanup proof tree; the current automaton source scan is clean and the current evidence audit reports no automaton evidence records.

Recent Progress (December 18, 2025)

Session 6 Progress: Merge-Split Soundness Analysis

Key Finding: standard_accepts_implies_merge_split_accepts is PROVEN

The lemma at Completeness.v:4127-4206 is fully proven (Qed), not admitted. This was previously marked as out of scope. The proof uses:

automaton_run_std_ms_correspondence for relating Standard and MergeAndSplit runs
Initial position equality and epsilon closure correspondence
Final position preservation through antichain filtering

Analysis of Remaining Soundness Admits (3 total):

Lemma	Line	Issue	Required Infrastructure
`automaton_run_preserves_reachable_transposition`	3872-3999	Special position tracking gap at line 3991	Needs provenance tracking
`automaton_sound_merge_split`	4479-4491	No proof body	Needs `position_reachable_merge_split` infrastructure
`automaton_sound_merge_split_lev`	4498-4508	Depends on above + needs `lev_le_double_merge_split`	Moderate effort

Session 6 Action: Deleted pseudo_reachable_nonspecial_implies_reachable

The orphan position_pseudo_reachable_damerau infrastructure (inductive + 2 lemmas) was deleted because:

pseudo_reachable_nonspecial_implies_reachable was NEVER used
automaton_sound_transposition (Qed) uses a different proof path via automaton_run_preserves_reachable_transposition
Removing ~140 lines of dead code reduces complexity without affecting any proofs

Merge-Split Soundness Requirements:

For automaton_sound_merge_split:

Missing Infrastructure: No position_reachable_merge_split inductive type exists
Transition Structure: MergeAndSplit has transition_position_merge_split with:
- Standard transitions (match, substitute, insert)
- Merge: 2 query chars → 1 dict char (std_pos (S (S i)) (S e))
- Enter split: creates special_pos i (S e) to start split
- Complete split: from special, creates std_pos (S i) e
Required Work: Define position_reachable_merge_split and prove automaton_run_preserves_reachable_merge_split

For automaton_sound_merge_split_lev:

Depends on automaton_sound_merge_split (merge_split_distance ≤ n)
Needs lev_le_double_merge_split: lev_distance s1 s2 ≤ 2 * merge_split_distance s1 s2
- Not currently proven; needs induction on optimal MS edit sequence
- Each merge/split (cost 1) simulated by ≤2 standard ops (cost 2)

Proven Relationships:

✅ ms_le_standard: merge_split_distance ≤ lev_distance (MergeSplitDistance.v:184)
❌ lev_le_double_merge_split: lev_distance ≤ 2 * merge_split_distance (MISSING)

Session 5 Progress: Position Tracking Analysis

Key Finding: fold_state_insert_incl is FALSE as stated

The lemma at Completeness.v:3769 claimed that antichain filtering preserves inclusion between position lists. This is FALSE due to how subsumption works:

(* Counterexample: *)
(* pos_list1 = [p], pos_list2 = [p, q] where q subsumes p for alg2 *)
(* Output for pos_list1: [p] (p survives, nothing to subsume it) *)
(* Output for pos_list2: [q] (q subsumes and replaces p) *)
(* incl [p] [q] = false *)

Updated the lemma's docstring to clearly document it as FALSE with counterexample.

Fundamental Issue: positions_contain vs Antichain Mismatch

The completeness proof structure assumes positions_contain is preserved through execution, but this is incompatible with antichain filtering:

positions_contain requires exact term_index matching via position_subsumes
subsumes_standard allows positions at different indices to subsume each other when |i - j| <= f - e

This mismatch means:

A position (i, e) might be subsumed by (j, f) with j ≠ i and f < e
The transition from (j, f) produces different output than from (i, e)
So positions_contain invariant breaks

Blocking Admits in Completeness.v:

Line	Lemma	Issue
2438	`reachable_implies_contained_aux`	Inner admits at 2396, 2416, 2436 - need state-level transition lemmas
2566	`automaton_run_not_dead_for_reachable`	Match case at 2531 needs e < n but match has e <= n
2614	`automaton_final_state_accepts_standard`	Depends on `reachable_implies_contained_aux`
3345	`automaton_run_step_std_trans`	Uses false `fold_state_insert_incl`
3769	`fold_state_insert_incl`	FALSE as stated - documented
4054	`automaton_run_step_std_ms`	Uses false `fold_state_insert_incl`
4302	`automaton_complete_transposition`	Needs Damerau-specific path tracking
4340	`automaton_complete_merge_split`	Needs MergeAndSplit-specific path tracking
4397	`automaton_finds_distance`	Depends on completeness infrastructure

Proven Helpers:

✅ fold_state_insert_nonempty: Antichain on non-empty list is non-empty
✅ fold_state_insert_preserves_membership: Final positions survive antichain (key for acceptance)
✅ fold_state_insert_has_final: If input has final position, output has final position

Recommended Approach (Option C from above):

Instead of tracking all reachable positions, track only that:

The automaton doesn't go dead (maintains some position with bounded errors)
When a final position is reachable, SOME final position survives to the final state

Key insight: fold_state_insert_has_final + "non-final cannot subsume final" rule means final positions are protected. The gap is showing final positions enter the state in the first place.

Previous Progress (December 10, 2025)

Session 4 Progress: Merge-Split Trace Infrastructure

OptimalTrace/MergeSplitConstruction.v - Branch Lemmas:

✅ PROVEN: ms_trace_cost_shift_A_delete - Delete branch cost decomposition
✅ PROVEN: ms_trace_cost_shift_B_insert - Insert branch cost decomposition
⚠️ ADMITTED: ms_trace_cost_cons_merge - Merge branch (goal structure issue after unfold)
⚠️ ADMITTED: ms_trace_cost_cons_split - Split branch (same structural issue)
⚠️ ADMITTED: ms_trace_cost_cons_double - Double-subst branch (same structural issue)
⚠️ ADMITTED: ms_optimal_trace_cost_eq - Optimal trace has cost = distance

Key Issue Identified: After unfolding ms_trace_cost, the goal becomes a raw arithmetic expression and ms_trace_change_cost_shift_* lemmas cannot find their patterns because ms_trace_change_cost has been expanded. Requires either:

(a) Different proof strategy that doesn't unfold ms_trace_cost
(b) Direct fold_left manipulation lemmas
(c) Compositional cost function that avoids structural mismatch

Added Infrastructure:

ms_element_shift_A_2, ms_element_shift_B_2 - Shift by 2 for multi-position operations
ms_trace_shift_A_2_map, ms_trace_shift_B_2_map - Map versions of shift
nth_plus_2_minus_1 - Arithmetic helper for shift-by-2 proofs
Position length preservation lemmas for shift-by-2

Triangle Inequality Status:

ms_triangle in Core/MergeSplitDistance.v remains admitted
ms_triangle_via_trace in Composition/MergeSplitComposition.v remains admitted
Both await completion of ms_optimal_trace_cost_eq
Semantic justification is clear: going through intermediate string is one valid transformation

Previous Progress (December 9, 2025)

Session 3 Progress:

DamerauTrace.v - dl_distance_le_valid_trace_cost:

Added helper lemmas: dl_touched_A_length_bound, dl_touched_B_length_bound, dl_trace_cost_nonneg, dl_change_cost_mono, dl_change_cost_fold_ge
Completed empty trace case (uses damerau_lev_le_standard + lev_distance_upper_bound)
Non-empty trace case documented but still admitted (requires trace-to-edit-sequence correspondence)

DamerauTrace.v - dl_optimal_trace_exists:

Added detailed proof strategy documentation
Completed base cases:
- Empty A: empty trace has cost = |B| = distance
- Empty B: empty trace has cost = |A| = distance
- Single char A and B: [DLMatch 1 1] achieves exact distance
Remaining edge cases (single vs multi, multi vs single, main case) still admitted

Session 2 Progress:

COMPLETED: automaton_run_std_trans_correspondence (Qed)

Extended automaton_run_step_std_trans to return additional invariants:
- Position inclusion: incl (positions s_std') (positions s_trans')
- Non-special preservation: Standard positions are non-special
- Spread bound propagation: Transposition positions satisfy spread bound
Used these invariants in the induction step of automaton_run_std_trans_correspondence

PROVEN: Non-special preservation within automaton_run_step_std_trans

Used transition_state_positions_standard_nonspecial: Standard transitions produce only non-special positions
Used epsilon_closure_nonspecial: Epsilon closure preserves non-special property
Used fold_state_insert_non_special: Antichain filtering preserves non-special property

REMAINING in automaton_run_step_std_trans: 2 admits

Position inclusion (line 3214): Antichain filtering can differ between Standard and Transposition
Spread bound (line 3251): Need to show spread is preserved through transitions

Session 1 Progress:

Added: Epsilon closure helper lemmas to Transition.v:

epsilon_closure_from_origin_term_eq_errors_aux: Proves term_index = num_errors for positions from initial state
epsilon_closure_from_origin_term_eq_errors: Simplified interface for the above
epsilon_closure_from_origin_term_bounded: Proves term_index <= n for initial state positions
epsilon_closure_aux_preserves_original: Original positions are preserved in closure
std_pos_0_0_in_epsilon_closure: std_pos 0 0 is always in initial closure
fold_left_min_contains_zero: Helper for computing minimum term_index
epsilon_closure_from_origin_min_is_zero: Minimum term_index in initial closure is 0

COMPLETED: standard_accepts_implies_transposition_accepts (Qed)

Used the new epsilon closure lemmas to prove spread bound for initial state
Required adding spread bound hypothesis to automaton_run_step_std_trans and automaton_run_std_trans_correspondence

Previous Progress

Fixed assertion error in automaton_run_std_trans_correspondence (line 3337-3339)
Added helper lemmas: fold_state_insert_final_reverse, incl_not_nil

Admitted Lemmas by File

Automaton/Soundness.v (3 admitted - reduced from 4)

Line	Name	Type	Scope	Notes
3999	`automaton_run_preserves_reachable_transposition`	Lemma	Transposition	Special position tracking gap at line 3991
4491	`automaton_sound_merge_split`	Theorem	Merge/Split	Needs `position_reachable_merge_split`
4508	`automaton_sound_merge_split_lev`	Corollary	Merge/Split	Depends on above + `lev_le_double_merge_split`

Deleted: pseudo_reachable_nonspecial_implies_reachable (was orphan code, never used)

Automaton/Completeness.v (8 admitted)

Line	Name	Type	Scope	Notes
2438	`reachable_implies_contained_aux`	Lemma	Standard	CRITICAL - Core lemma for completeness
2566	`automaton_run_not_dead_for_reachable`	Lemma	Standard	Depends on contained_aux
2614	`automaton_final_state_accepts_standard`	Lemma	Standard	Depends on above two
3276	`automaton_run_step_std_trans`	Lemma	Transposition	2 internal admits: position inclusion, spread bound
~3388	`automaton_run_std_trans_correspondence`	Lemma	Transposition	✅ COMPLETED - Uses automaton_run_step_std_trans properties
~3474	`standard_accepts_implies_transposition_accepts`	Lemma	Transposition	✅ COMPLETED - Uses epsilon closure lemmas
3527	`standard_accepts_implies_merge_split_accepts`	Lemma	Merge/Split	OUT OF SCOPE
3623	`automaton_complete_transposition`	Theorem	Transposition	Main transposition completeness
3661	`automaton_complete_merge_split`	Theorem	Merge/Split	OUT OF SCOPE
3718	`automaton_finds_distance`	Corollary	All	Distance computation corollary

Automaton/MainTheorem.v (1 admitted)

Line	Name	Type	Scope	Notes
250	`automaton_distance_correct`	Theorem	Standard	Distance = lev_distance

Other Files

File	Line	Name	Notes
Composition/DamerauComposition.v	826	`damerau_change_cost_bound`	Inner admits in algebraic bounds
Composition/DamerauComposition.v	2082	`damerau_lev_triangle_via_composition`	Depends on above
Composition/MergeSplitComposition.v	176	`ms_triangle_via_trace`	Awaits ms_optimal_trace_cost_eq
Core/MergeSplitDistance.v	1648	`ms_seq_compose`	Edit sequence composition
Core/MergeSplitDistance.v	1896	`ms_triangle`	Direct approach (main case admitted)
OptimalTrace/MergeSplitConstruction.v	1120	`ms_trace_cost_cons_merge`	Goal structure issue after unfold
OptimalTrace/MergeSplitConstruction.v	1241	`ms_trace_cost_cons_split`	Same structural issue
OptimalTrace/MergeSplitConstruction.v	1268	`ms_trace_cost_cons_double`	Same structural issue
OptimalTrace/MergeSplitConstruction.v	1316	`ms_optimal_trace_cost_eq`	Main cost equality theorem

Note: Trace/DamerauTrace.v now has 0 admits (base cases fully proven)

Dependency Graph

reachable_implies_contained_aux (CRITICAL - Admitted)
    ↓
automaton_run_not_dead_for_reachable (Admitted)
    ↓
automaton_final_state_accepts_standard (Admitted)
    ↓
reachable_final_implies_accepts [PROVEN]
    ↓
automaton_complete_standard [PROVEN]
    ↓
automaton_distance_correct (MainTheorem.v - Admitted)

automaton_run_step_std_trans (Admitted - 2 internal admits remaining)
    ↓
automaton_run_std_trans_correspondence [PROVEN]
    ↓
standard_accepts_implies_transposition_accepts [PROVEN]
    ↓
automaton_complete_transposition (Admitted - needs Damerau-specific proof)

automaton_run_preserves_reachable_transposition (independent, for Damerau soundness - Admitted)

Critical Issue: `reachable_implies_contained_aux`

Statement

Lemma reachable_implies_contained_aux : forall query n dict_prefix p,
  position_reachable query n dict_prefix p ->
  num_errors p <= n ->
  is_special p = false ->
  forall s,
    automaton_run_from_initial Standard query n dict_prefix = Some s ->
    positions_contain (positions s) p.

Problem Analysis

The lemma attempts to prove that if a position p is reachable via edit operations, then the automaton's state contains that position. However, there's a fundamental mismatch between:

positions_contain (used in the lemma): Requires position_subsumes p1 p2 which demands:
- Same term_index
- Same is_special flag
- num_errors p1 <= num_errors p2
subsumes_standard (used by automaton's antichain): Allows different term_index values when one position dominates another:
```
(* A position at term_index i with errors e can subsume
   a position at term_index i+k with errors e+k *)
```

Consequence

When the automaton performs antichain filtering via fold_left state_insert, a position at (i, e) can remove a position at (i+1, e+1) because the first "dominates" the second (you can always reach (i+1, e+1) from (i, e) via deletion).

This means the exact reachable position may not survive antichain filtering, only a dominating position with lower term_index remains.

Why This Matters

The current lemma statement is too strong for intermediate positions
Cannot prove that std_pos (length dict_prefix) e is in the state if a dominating position std_pos k e' (where k < length dict_prefix and k + (length dict_prefix - k) = length dict_prefix, e' + (length dict_prefix - k) = e) is in the antichain

Possible Solutions

Option A: Weaker Predicate

Replace positions_contain with a weaker predicate:

Definition positions_dominate (ps : list Position) (p : Position) : bool :=
  existsb (fun p' =>
    (term_index p' <= term_index p) &&
    (num_errors p' + (term_index p - term_index p') <= num_errors p)
  ) ps.

Option B: Track Final Positions Only

For completeness, we only need to show that final positions survive. The "non-final cannot subsume final" rule (2024-12 bug fix) protects final positions:

(* In subsumes_standard: *)
if position_is_final p1 qlen then
  if position_is_final p2 qlen then
    (* both final: compare errors *)
    num_errors p1 <=? num_errors p2
  else
    (* p1 final, p2 non-final: p1 cannot subsume p2 *)
    false
else
  (* p1 non-final: standard subsumption *)
  ...

This means a final position can only be removed by another final position with fewer errors.

Option C: Restructure Completeness Proof

Use existing proven infrastructure:

fold_state_insert_has_final: If closed_positions contains a final position, the result is accepting
fold_state_insert_preserves_min_error: Minimum error count is preserved
transition_state_not_dead_standard: Standard never goes dead if errors < n

New lemma needed:

Lemma reachable_final_produces_closed_final : forall query n dict_prefix,
  (exists p, position_reachable query n dict_prefix p /\
             position_is_final p (length query) = true /\
             num_errors p <= n) ->
  forall s,
    automaton_run_from_initial Standard query n dict_prefix = Some s ->
    exists p', In p' (positions s) /\
               position_is_final p' (length query) = true.

Progress Made

Recently Fixed Lemmas

transition_produces_insert_bounded (Completeness.v:1349-1366)
- Fixed type unification issue by moving destruct p before exists
- Used change tactic to make definitional equality explicit
transition_produces_insert_exact (Completeness.v:1369-1383)
- Same fix pattern as above

Helper Infrastructure Available

The following proven lemmas can help complete the remaining proofs:

transition_standard_produces_match (Transition.v)
transition_standard_produces_substitute (Transition.v)
transition_standard_produces_insert (Transition.v)
fold_state_insert_has_final (Completeness.v)
fold_state_insert_preserves_min_error (Completeness.v)
fold_state_insert_accepting (Completeness.v)
transition_state_not_dead_standard (Completeness.v)

Merge/Split Lemma Status

PROVEN:

✅ standard_accepts_implies_merge_split_accepts (Completeness.v:4127-4206) - Qed

ADMITTED (require infrastructure):

automaton_sound_merge_split (Soundness.v:4622-4634) - needs position_reachable_merge_split
automaton_sound_merge_split_lev (Soundness.v:4641-4651) - depends on above + lev_le_double_merge_split
automaton_complete_merge_split (Completeness.v:4326-4340) - needs merge-split-specific path tracking

These require integration with the MergeSplitDistance.v module which defines a different distance metric.

Critical Issue: Transposition Soundness (`automaton_run_preserves_reachable_transposition`)

Date Updated: December 8, 2025

Statement

Lemma automaton_run_preserves_reachable_transposition : forall query n dict_prefix dict s final,
  query_length s = length query ->
  automaton_run Transposition query n dict s = Some final ->
  (forall p, In p (Automaton.State.positions s) ->
             is_special p = false ->
             position_reachable_damerau query n dict_prefix p) ->
  (forall p, In p (Automaton.State.positions final) ->
             is_special p = false ->
             position_reachable_damerau query n (dict_prefix ++ dict) p).

Problem Analysis: Spurious Special Positions

The transposition algorithm creates spurious special positions when query[i] = query[i+1]:

Normal case (c ≠ query[i]): Enter-transpose creates special_pos i (e+1) which is reachable via reach_damerau_enter_transpose
Spurious case (c = query[i] = query[i+1]): Enter-transpose ALSO creates special_pos i (e+1) but:
- reach_damerau_enter_transpose requires c ≠ c_next (c ≠ query[i])
- So the spurious special position is NOT semantically reachable
- It exists in the automaton state but has no valid edit sequence

Why This Breaks the Proof

At line 4134 in Soundness.v, we need to provide:

position_reachable_damerau query n dict_prefix p2

where p2 is a special position in state s.

The issue: transition_positions_reachable_transposition (line 3814) requires ALL input positions to be reachable, but our hypothesis only guarantees non-special inputs are reachable.

Key Insight: Subsumption Saves Soundness

Spurious positions don't affect soundness because:

Same term_index: When query[i] = query[i+1] = c:
- Spurious path: std_pos i e → special_pos i (e+1) → std_pos (i+2) (e+1)
- Match path: std_pos i e → std_pos (i+1) e → std_pos (i+2) e
Error count: Match path has error count e, spurious path has e+1
Subsumption: std_pos (i+2) e subsumes std_pos (i+2) (e+1) by standard subsumption rules (same term_index, lower errors)
Antichain filtering: The spurious position is removed, only the reachable one survives

Solution Approaches

Approach A: Track Position Provenance

Strengthen the invariant to track how special positions were created:

Inductive position_trackable_damerau (query : list Char) (n : nat) :
  list Char -> Position -> Prop :=
  | trackable_reachable : forall dp p,
      position_reachable_damerau query n dp p ->
      is_special p = false ->
      position_trackable_damerau query n dp p
  | trackable_special : forall dp c i e,
      position_reachable_damerau query n dp (std_pos i e) ->
      S i < length query ->
      nth_error query (S i) = Some c ->
      e < n ->
      position_trackable_damerau query n (dp ++ [c]) (special_pos i (S e)).

Then prove non-special trackable positions are either reachable OR subsumed by reachable.

Approach B: Use Pseudo-Reachability (ABANDONED)

~~1. Complete pseudo_reachable_nonspecial_implies_reachable (Soundness.v:246)~~ ~~2. Change invariant to track pseudo-reachability~~ ~~3. Convert to true reachability at final step~~

Status: ABANDONED - The position_pseudo_reachable_damerau infrastructure was deleted in Session 6 as orphan code. The soundness proof uses a different path via automaton_run_preserves_reachable_transposition.

Approach C: Prove Post-Antichain Only

Instead of proving all trans_pos positions are reachable, prove:

Positions surviving antichain are reachable
Use the fact that spurious positions are always subsumed

This requires showing: if std_pos (i+2) (e+1) comes from spurious complete_transpose, then std_pos (i+2) e (from matches) is also in trans_pos.

Verified Behaviors

From Subsumption.v (lines 73-96), for Transposition subsumption:

Same is_special: standard subsumption e ≤ f ∧ |i-j| ≤ f-e
Different is_special: no subsumption possible
Special positions only subsume same-index special positions

This confirms spurious non-special outputs ARE subsumed by match outputs.

Recommended Path Forward

Prove helper: Show that when enter_transpose fires and c = query[i], the match transition also fires, producing std_pos (i+1) e which leads to std_pos (i+2) e
Prove subsumption: Show std_pos (i+2) e subsumes std_pos (i+2) (e+1) and both are in same trans_pos
Restructure main lemma: Only claim reachability for positions surviving antichain

Recommended Next Steps

Decide on solution approach for reachable_implies_contained_aux:
- Option A: Weaker predicate (most general, more work)
- Option B: Final positions only (sufficient for completeness, simpler)
- Option C: Restructure proof (use existing infrastructure)
If Option B/C chosen:
- Create reachable_final_produces_closed_final lemma
- Modify automaton_final_state_accepts_standard to use new approach
- Chain through to automaton_complete_standard (already proven given accepts)
For transposition proofs:
- automaton_run_step_std_trans needs characteristic vector analysis
- standard_accepts_implies_transposition_accepts builds on step lemma
- automaton_complete_transposition may need separate Damerau reachability
- See detailed analysis above for automaton_run_preserves_reachable_transposition
For soundness:
- automaton_run_preserves_reachable_transposition blocked by spurious position issue
- Need to implement one of the solution approaches (A, B, or C) above

Categorization of Remaining Work

Category 1: Requires Structural Changes (HIGH COMPLEXITY)

These lemmas need fundamental changes to the proof approach:

Lemma	Issue	Effort
`automaton_run_preserves_reachable_transposition`	Spurious special positions (see analysis above)	HIGH

Deleted: pseudo_reachable_nonspecial_implies_reachable was removed as orphan code (Session 6)

Recommendation: Implement Approach C (post-antichain reachability) - requires proving spurious outputs are always subsumed.

Category 2: Requires Trace-Edit Correspondence (MEDIUM COMPLEXITY)

These lemmas need to establish correspondence between traces and edit sequences:

Lemma	What's Needed	Effort
`dl_distance_le_valid_trace_cost`	Prove trace represents valid edit sequence with matching cost	MEDIUM
`dl_optimal_trace_exists`	Construct trace by backtracking through DP recursion	MEDIUM

Recommendation: Define an inductive "trace-to-edits" relation and prove correspondence.

Category 3: Requires Characteristic Vector Analysis (MEDIUM COMPLEXITY)

Lemma	What's Needed	Effort
`automaton_run_step_std_trans`	Analyze CV bit compatibility between Standard and Transposition	MEDIUM

Recommendation: Prove that Standard's CV window is contained in Transposition's, so Standard transitions are a subset.

Category 4: Chain from Other Lemmas (LOW COMPLEXITY once dependencies complete)

Lemma	Dependencies	Status
`standard_accepts_implies_transposition_accepts`	`automaton_run_step_std_trans`	COMPLETED (Qed)
`automaton_complete_transposition`	Direct Damerau completeness (cannot use Standard→Trans because damerau < lev possible)	Admitted

Note on standard_accepts_implies_transposition_accepts: This lemma is proven but relies on admitted subcases in automaton_run_step_std_trans (spread bound) and automaton_run_std_trans_correspondence (position inclusion through antichain). The proof structure is sound.

Category 4.1: Position Inclusion Through Antichain (HIGH COMPLEXITY)

The automaton_run_std_trans_correspondence lemma requires maintaining position inclusion incl (positions s_std) (positions s_trans) through the automaton run. After each transition:

We have incl closed_std closed_trans before antichain filtering
But proving inclusion AFTER antichain filtering is complex because:
- Transposition's closed_trans has extra positions (from complete_transpose)
- These extra non-special positions could subsume Standard positions
- Special positions cannot subsume non-special (subsumption rules)

Key insight: For FINAL positions, the protection is that final positions can only be subsumed by other final positions with lower errors. So even if exact position inclusion doesn't hold, FINAL position preservation does hold.

The current proof uses this weaker property (final state preservation) rather than full position inclusion.

Category 5: Merge/Split (Requires Significant Infrastructure)

PROVEN:

✅ standard_accepts_implies_merge_split_accepts (Completeness.v:4127-4206)

ADMITTED:

automaton_sound_merge_split - requires position_reachable_merge_split inductive type
automaton_sound_merge_split_lev - requires lev_le_double_merge_split lemma
automaton_complete_merge_split - requires merge-split-specific path tracking

Option C Implementation Strategy (December 18, 2025)

Key Insight: Subsumption Preserves Reachability to Final

The fundamental insight enabling Option C is that if position p can reach a final position with errors ≤ n, and p' subsumes p (via subsumes_standard), then p' can ALSO reach a final position with errors ≤ n.

Proof Sketch:

Let p = (i, e) reach final (qlen, f) with f ≤ n via some edit operations
Let p' = (j, e') subsume p, meaning e' ≤ e and |i - j| ≤ e - e'
Case j ≤ i (i.e., j = i - d where 0 ≤ d ≤ e - e'):
- Use d delete operations: (j, e') → (j+d, e'+d) = (i, e'+d) with e'+d ≤ e
- Follow same path as p to reach (qlen, f' = e'+d + (f-e))
- Total: f' = f + (e'+d) - e ≤ f + (e'-e) + d ≤ f (since d ≤ e-e')
- So f' ≤ f ≤ n ✓
Case j > i is symmetric

Implementation Plan

Step 1: Define `can_complete_to_final` Predicate

(* Position can complete to a final position via remaining dict chars *)
Definition can_complete_to_final (qlen n : nat) (p : Position) (remaining_dict : list Char) (query : list Char) : Prop :=
  exists p_final,
    position_reachable_from query n remaining_dict p p_final /\
    position_is_final p_final qlen = true /\
    num_errors p_final <= n.

Where position_reachable_from extends position_reachable to start from position p instead of initial_position.

Step 2: Prove `subsumption_preserves_can_complete`

Lemma subsumption_preserves_can_complete : forall qlen n p p' remaining query,
  subsumes_standard qlen p' p = true ->
  can_complete_to_final qlen n p remaining query ->
  can_complete_to_final qlen n p' remaining query.

This follows from the insight above: the subsuming position can simulate the path by prepending delete operations.

Step 3: Prove `can_complete_preserved_through_antichain`

Lemma can_complete_preserved_through_antichain : forall qlen alg positions remaining query n,
  (exists p, In p positions /\ can_complete_to_final qlen n p remaining query) ->
  let result := fold_left (fun s q => state_insert q s) positions (empty_state alg qlen) in
  (exists p', In p' (positions result) /\ can_complete_to_final qlen n p' remaining query).

This uses subsumption_preserves_can_complete: if a can-complete position is filtered out, its subsuming replacement can also complete.

Step 4: Prove `can_complete_preserved_through_transition`

Lemma can_complete_preserved_through_transition : forall qlen n s c remaining query s',
  transition_state Standard s c query n = Some s' ->
  (exists p, In p (positions s) /\ can_complete_to_final qlen n p (c :: remaining) query) ->
  (exists p', In p' (positions s') /\ can_complete_to_final qlen n p' remaining query).

Key steps:

From can_complete for (c :: remaining), extract the position p and its completion path
The first step of the path uses c via match/substitute/insert
transition_state generates the corresponding next position in trans_positions
epsilon_closure preserves or extends it
Antichain filtering preserves can_complete (Step 3)

Step 5: Prove `reachable_final_produces_closed_final`

Lemma reachable_final_produces_closed_final : forall query n dict,
  (exists p, position_reachable query n dict p /\
             position_is_final p (length query) = true /\
             num_errors p <= n) ->
  match automaton_run_from_initial Standard query n dict with
  | None => False
  | Some final => state_is_final final = true
  end.

Proof by induction on dict:

Base: dict = [], initial position (0,0) can complete to final (given hypothesis)
Step: Use can_complete_preserved_through_transition for each character

At the end, can_complete_to_final qlen n p [] query means p IS a final position (no more chars to process). Use fold_state_insert_has_final to show it survives.

Step 6: Update `automaton_final_state_accepts_standard`

Replace the current admitted proof with:

Lemma automaton_final_state_accepts_standard : forall query n dict final p,
  automaton_run_from_initial Standard query n dict = Some final ->
  position_reachable query n dict p ->
  position_is_final p (length query) = true ->
  is_special p = false ->
  num_errors p <= n ->
  state_is_final final = true.
Proof.
  intros query n dict final p Hrun Hreach Hfinal Hspec Herr.
  apply reachable_final_produces_closed_final.
  - exists p. split; [exact Hreach | split; [exact Hfinal | exact Herr]].
  - rewrite Hrun. (* Shows final state exists *)
Qed.

Why This Approach Works

No individual position tracking: We don't track whether specific positions survive antichain
Property-based reasoning: We track "can complete to final" which is preserved by subsumption
Final position protection: fold_state_insert_has_final ensures final positions survive
Existing infrastructure: Uses proven lemmas (fold_state_insert_has_final, transition_*_produces_*)

Estimated Complexity

Lemma	Lines	Difficulty
`can_complete_to_final` definition	10-20	LOW
`position_reachable_from` inductive	30-50	MEDIUM
`subsumption_preserves_can_complete`	40-60	MEDIUM
`can_complete_preserved_through_antichain`	30-50	MEDIUM
`can_complete_preserved_through_transition`	60-100	HIGH
`reachable_final_produces_closed_final`	40-60	MEDIUM
Update `automaton_final_state_accepts_standard`	10-20	LOW
Total	220-360	-

Build Command

cd docs/verification/core/theories
systemd-run --user --scope -p MemoryMax=126G -p CPUQuota=1800% -p IOWeight=30 -p TasksMax=200 make -j1

File Locations

Plan: /home/dylon/.claude/plans/robust-gliding-porcupine.md
Completeness.v: Automaton/Completeness.v
Soundness.v: Automaton/Soundness.v
MainTheorem.v: Automaton/MainTheorem.v
Transition.v: Automaton/Transition.v (helper lemmas)
DamerauTrace.v: Trace/DamerauTrace.v (DL trace infrastructure)
DamerauComposition.v: Composition/DamerauComposition.v (triangle inequality)

❮Liblevenshtein Core Verification Library Verification — Core Theories: Automaton❯

Can you improve this documentation?Edit on GitHub

cljdoc builds & hosts documentation for Clojure/Script libraries

Keyboard shortcuts

`Ctrl`+`k`	Jump to recent docs
`←`	Move to previous article
`→`	Move to next article
`Ctrl`+`/`	Jump to the search field

Raise an issue Browse cljdoc source Chat on Slack

× close