Sequence patches: bounded splice length is original minus deleted plus inserted
Proof verified
typechecked
Pinned formal modules
module #2 · 9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc
What this target establishes
Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
- Obligations
- cost accounting
- Cost metric
- custom
- Model
- Reference splice over flattened chunks: take n, append inserted contents, drop n+deleted.
- Assumptions
- Insertion index is at most original element length. Deletion count is at most the remaining suffix length.
- Implementation correspondence
- abstract model
- Limitations
- Counts output elements, not edit cost or encoded bytes. No optimality, balance, cached-measure, performance or Unicode-indexing theorem.
A splice inserts flattened chunks at index n and removes deleted elements from the existing flattened contents. If n is within the sequence and deletion fits in the remaining suffix, the resulting length equals original length minus deleted count plus inserted length. This provides an exact measurement obligation for insert/delete patches on rope-backed sequences. It establishes resulting element length, not edit-script minimality, encoded patch bytes, native rope correctness or Unicode offset conversions.
Formal statement
∀ (A : Type) (n deleted : Nat) (inserted chunks : List (List A)), n ≤ (Hunch.ChunkedSequence.contents A chunks).length → deleted ≤ (Hunch.ChunkedSequence.contents A chunks).length - n → (Hunch.ChunkedSequence.splice A n deleted inserted chunks).length = (Hunch.ChunkedSequence.contents A chunks).length - deleted + (Hunch.ChunkedSequence.contents A inserted).length
Standard library — lists, arrays, maps · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 b29dcff892c50051bab9a5502dfe9aeaeca7aeac7b066ab0c3838699afd6f17d
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.