[wip/levenshtein] Prove DP/recursive equivalence bridge

[CharlesCNorton]

Summary

This PR completes the missing bridge between the dynamic-programming Levenshtein model and Crane's intrinsic recursive model.

It adds a new proof file tests/wip/levenshtein/BridgeDP.v and refactors tests/wip/levenshtein/Levenshtein.v to expose reusable recurrence lemmas used by the bridge.

Why this matters

Before this PR, we had:

• a recursive intrinsic implementation/proof in Levenshtein.v
• a loop-structured DP model in progress

but no completed theorem showing they compute the same value for the same inputs.

This PR closes that gap with:

• lev_dp_string_eq_levenshtein_computed

What changed

1) New file: tests/wip/levenshtein/BridgeDP.v

Adds a full DP formalization and bridge proof:

• DP model definitions:
  • dp_min, inner_loop, process_row, outer_result_run
  • lev_dp_list, lev_dp_string
• Row/cache invariants and loop correctness lemmas:
  • row_values, row_last
  • inner_loop_cont_correct
  • process_row_correct_nonempty
  • outer_result_run_correct
• Orientation/reversal machinery:
  • chain_append_right
  • chain_add_last_source
  • chain_strip_last_source
  • chain_update_last_source
  • rev_string, chain_rev_string
  • levenshtein_computed_rev_string
  • lev_spec_list_rev
• Main bridge theorem:
  • lev_dp_string_eq_levenshtein_computed

2) Refactor: tests/wip/levenshtein/Levenshtein.v

Adds reusable lemmas and reduces repeated proof patterns:

• new helper lemmas:
  • levenshtein_computed_of_chain
  • levenshtein_computed_nil_l
  • levenshtein_computed_nil_r
  • levenshtein_computed_cons_neq
• mismatch upper-bound lemmas now rewrite through levenshtein_computed_cons_neq and finish with lia instead of re-deriving min3 branch details each time
• updates fragile Nat.* references to PeanoNat.Nat.* where needed for current Rocq compatibility

Dependency chain (project-level)

Within Crane, this PR establishes:

• DP model (BridgeDP.v) -> recursive model (Levenshtein.v)

In the broader 4-file story discussed during development:

• levenshtein-vst/levenshtein.v + levenshtein-vst/verif_levenshtein.v (VST side, separate toolchain)
• tests/wip/levenshtein/BridgeDP.v + tests/wip/levenshtein/Levenshtein.v (this PR)

So this PR contributes the Crane-side bridge artifact and its required recurrence refactor.

Verification

Ran locally (Rocq toolchain used by Crane tests):

• coqc -Q /mnt/d/crane/theories Crane -Q /mnt/d/crane/tests/wip/levenshtein '' /mnt/d/crane/tests/wip/levenshtein/Levenshtein.v
• coqc -Q /mnt/d/crane/theories Crane -Q /mnt/d/crane/tests/wip/levenshtein '' /mnt/d/crane/tests/wip/levenshtein/BridgeDP.v

Both compile successfully.

Proof hygiene:

• no Admitted
• no Axiom

Diff summary

• tests/wip/levenshtein/BridgeDP.v: new file (+912)
• tests/wip/levenshtein/Levenshtein.v: +564 / -179

[CharlesCNorton]

Companion artifact (separate toolchain) is now published at:

• https://github.com/CharlesCNorton/levenshtein-vst

This contains the VST/CompCert-side files (levenshtein.v, �erif_levenshtein.v, levenshtein.c, _CoqProject) and build instructions. The split keeps this Crane PR focused on the Rocq/Dune bridge proof files.

[joom]

I'm trying to keep the tests in a specific format: one Rocq file, one .t.cpp file, and generated .h and .cpp files. This PR breaks this format, so I'm not sure what the right thing to do is. One possible solution is to have a separate levenshtein_dp test (only with the dynamic programming version of the function). Another solution is to add the dynamic programming version (and all the proofs) directly in the Levenshtein.v file. My worry about that is that the file already does a lot, but I guess the second solution is the better option? What do you think?