Created: 2025-11-23 Status: Ready for implementation Estimated Time: 4-6.5 hours Confidence: HIGH (85%)
This document contains the detailed research and proof plan for completing change_cost_compose_bound (line 3892-3942 in Distance.v), which bounds the sum of substitution costs in a composed trace.
Location: Distance.v:3892-3942
Lemma change_cost_compose_bound :
forall (A B C : list Char) (T1 : Trace A B) (T2 : Trace B C),
is_valid_trace A B T1 = true ->
is_valid_trace B C T2 = true ->
let comp := compose_trace T1 T2 in
fold_left (fun sum '(i, k) =>
sum + subst_cost (nth i A default_char) (nth k C default_char)
) comp 0 <=
fold_left (fun sum '(i, j) =>
sum + subst_cost (nth i A default_char) (nth j B default_char)
) T1 0 +
fold_left (fun sum '(j, k) =>
sum + subst_cost (nth j B default_char) (nth k C default_char)
) T2 0.
Purpose: Prove that the sum of substitution costs in the composed trace is bounded by the sum of costs in T1 plus the sum of costs in T2.
Current Status: Admitted (line 3942)
After comprehensive analysis of the codebase, the proof infrastructure is 95% complete. All witness extraction, injectivity, cardinality bounds, and fold_left monotonicity lemmas exist and are proven with Qed.
The only missing piece: fold_left_sum_bound_subset
This lemma states that the sum over a subset is bounded by the sum over the superset.
witness_to_T1 (line 3377-3402)
(i,j) ∈ T1 witness for (i,k) ∈ compose_tracewitness_to_T2 (line 3407-3432)
(j,k) ∈ T2 witness for (i,k) ∈ compose_tracewitness_to_T1_correct (line 3437-3503)
In ik (compose_trace T1 T2) → In (witness_to_T1 ... ik) T1witness_to_T2_correct (line 3508-3574)
In ik (compose_trace T1 T2) → In (witness_to_T2 ... ik) T2witness_to_T1_injective (line 3579-3639)
witness_to_T1 is injective on compose_trace T1 T2witness_j_unique_in_T1 (line 2746)witness_to_T2_injective (line 3644-3704)
witness_to_T2 is injective on compose_trace T1 T2witness_k_unique_in_T2 (line 2773)compose_witness_bounded_T1 (line 3798-3838)
length (compose_trace T1 T2) ≤ length T1 via injectivitycompose_trace_preserves_NoDup)compose_witness_bounded_T2 (line 3843-3884)
length (compose_trace T1 T2) ≤ length T2 via injectivitycompose_trace_preserves_NoDup)fold_left_add_monotone (line 2480)
fold_left_add_init_monotone (line ~2450)
subst_cost_triangle (line 2059)
subst_cost(a,c) ≤ subst_cost(a,b) + subst_cost(b,c)What it proves: Sum over a subset is bounded by sum over the superset.
Lemma fold_left_sum_bound_subset :
forall (f : nat * nat -> nat) (sub super : list (nat * nat)),
(forall x, In x sub -> In x super) -> (* sub ⊆ super *)
fold_left (fun sum ik => sum + f ik) sub 0 <=
fold_left (fun sum ik => sum + f ik) super 0.
Proof strategy:
supersuper = [] implies sub = [] (from subset property), both sums are 0super = x :: super'
In x sub
sub = sub' ++ [x] for some sub' (reorder)sub' and super'f x, preserve inequality¬In x sub
sub ⊆ super'sub and super'f x), inequality strengthensEstimated effort: 60-80 lines, 1-1.5 hours
Alternative: Could use Coq's standard library lemmas about fold_left and subsets if available, potentially reducing to 20-30 lines.
Create and prove the missing lemma as described above.
Placement: Insert before change_cost_compose_bound (around line 3890)
Create two lemmas showing that the witness maps produce subsets:
Lemma witness_T1_image_subset :
forall (A B C : list Char) (T1 : Trace A B) (T2 : Trace B C),
is_valid_trace A B T1 = true ->
is_valid_trace B C T2 = true ->
forall ik, In ik (compose_trace T1 T2) ->
In (witness_to_T1 A B C T1 T2 ik) T1.
Proof.
intros. apply witness_to_T1_correct. assumption.
Qed.
Similar for witness_T2_image_subset.
These may be trivial wrappers around existing correctness lemmas, or may require 40-60 lines each to establish the subset relationship for the full list.
Estimated effort: 80-120 lines total, 1-2 hours
Now we have all the pieces:
Map composition elements to witnesses:
let comp_T1_witnesses := map (witness_to_T1 A B C T1 T2) comp in
let comp_T2_witnesses := map (witness_to_T2 A B C T1 T2) comp in
Apply triangle inequality pointwise:
Each (i,k) in comp has witnesses (i,j) in T1 and (j,k) in T2:
subst_cost(A[i], C[k]) ≤ subst_cost(A[i], B[j]) + subst_cost(B[j], C[k])
Sum both sides:
sum_{(i,k) ∈ comp} subst_cost(A[i], C[k]) ≤
sum_{(i,k) ∈ comp} [subst_cost(A[i], B[j]) + subst_cost(B[j], C[k])]
Split sum:
≤ sum_{(i,k) ∈ comp} subst_cost(A[i], B[j]) +
sum_{(i,k) ∈ comp} subst_cost(B[j], C[k])
Rewrite as sums over witness images:
= sum_{(i,j) ∈ comp_T1_witnesses} subst_cost(A[i], B[j]) +
sum_{(j,k) ∈ comp_T2_witnesses} subst_cost(B[j], C[k])
Apply fold_left_sum_bound_subset twice:
comp_T1_witnesses ⊆ T1 (by witness_T1_image_subset)comp_T2_witnesses ⊆ T2 (by witness_T2_image_subset)sum over comp_T1_witnesses ≤ sum over T1
sum over comp_T2_witnesses ≤ sum over T2
Combine inequalities:
sum over comp ≤ sum over T1 + sum over T2
∎
Estimated effort: 60-100 lines, 1-2 hours
| Task | Lines | Time |
|---|---|---|
fold_left_sum_bound_subset | 60-80 | 1-1.5h |
| Witness image subset helpers | 80-120 | 1-2h |
| Main proof | 60-100 | 1-2h |
| Total | 200-300 | 4-6.5h |
Confidence: HIGH (85%)
fold_left vs. map interaction: May need auxiliary lemmas about fold_left (fun sum x => sum + f x) (map g L) 0 equivalence to fold_left (fun sum x => sum + f (g x)) L 0.
Mitigation: These are standard list lemmas; should be straightforward 10-20 line proofs each if needed.
Subset vs. Injection: The witness maps are injective but may not be surjective. Need to ensure subset lemmas handle this correctly.
Mitigation: We only need image(witness_map) ⊆ T, not equality. This is exactly what the correctness lemmas provide.
fold_left commutativity assumptions: Standard fold_left proofs sometimes require commutativity/associativity of the operation. Addition has both, so this should not be an issue.
Mitigation: Explicitly use Nat.add_assoc and Nat.add_comm where needed.
After completing the proof:
Compilation test:
systemd-run --user --scope -p MemoryMax=126G -p CPUQuota=1800% \
-p IOWeight=30 -p TasksMax=200 \
coqc -Q docs/verification/core/theories "" \
docs/verification/core/theories/Distance.v
Check dependencies:
Print Assumptions change_cost_compose_bound.
Should show only standard axioms (functional extensionality, etc.), not our custom admits.
Update tracking:
change_cost_compose_bound as complete in ADMITTED_LEMMAS_STATUS.mdWith change_cost_compose_bound proven, the next lemmas in the dependency chain are:
lost_A_positions_bound (6-10h est.)lost_C_positions_bound (2-3h est.)trace_composition_delete_insert_bound (1-2h est.)All three depend on change_cost_compose_bound and form the "cost bounds chain" required for the Triangle Inequality.
Recommended order: 4 → 5 → 6 (dependency order)
Hypothesis: The proof requires only fold_left_sum_bound_subset, with all other infrastructure already proven.
Prediction: Proof should complete in 4-6.5 hours with high confidence.
Test: Implement according to this plan and measure actual time.
Validation criteria:
Qed (not Admitted)Print Assumptions shows no custom admitsIf hypothesis fails, 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 |