{"version":3,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"std","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"],"statement_hash":"b29dcff892c50051bab9a5502dfe9aeaeca7aeac7b066ab0c3838699afd6f17d","problem":{"id":35,"title":"Sequence patches: bounded splice length is original minus deleted plus inserted","description":"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.","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","profile":"std","module_pins":[{"id":2,"hash":"9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc"}],"module_context":[{"id":2,"hash":"9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc","namespace":"ChunkedSequence","source":"namespace Hunch.ChunkedSequence\ndef contents : ((A : Type) → List (List A) → List A) :=\n  fun _ chunks => chunks.flatten\n\ndef splitAt : ((A : Type) → Nat → List (List A) → List A × List A) :=\n  fun A n chunks => ((contents A chunks).take n, (contents A chunks).drop n)\n\ndef splice : ((A : Type) → Nat → Nat → List (List A) → List (List A) → List A) :=\n  fun A n deleted inserted chunks => (contents A chunks).take n ++ contents A inserted ++ (contents A chunks).drop (n + deleted)\n\ntheorem concat_contents : (∀ (A : Type) (xs ys : List (List A)), contents A (xs ++ ys) = contents A xs ++ contents A ys) :=\n  by\n    intro A xs ys\n    exact List.flatten_append\n\ntheorem split_roundtrip : (∀ (A : Type) (n : Nat) (chunks : List (List A)), (splitAt A n chunks).1 ++ (splitAt A n chunks).2 = contents A chunks) :=\n  by\n    intro A n chunks\n    exact List.take_append_drop n (contents A chunks)\n\ntheorem measure_correct : (∀ (A : Type) (chunks : List (List A)), (contents A chunks).length = (chunks.map List.length).sum) :=\n  by\n    intro A chunks\n    induction chunks with\n    | nil => rfl\n    | cons chunk rest ih => simp [contents] at ih ⊢\n\ntheorem splice_length : (∀ (A : Type) (n deleted : Nat) (inserted chunks : List (List A)), n ≤ (contents A chunks).length → deleted ≤ (contents A chunks).length - n → (splice A n deleted inserted chunks).length = (contents A chunks).length - deleted + (contents A inserted).length) :=\n  by\n    intro A n deleted inserted chunks hn hd\n    simp only [splice, List.length_append, List.length_take, List.length_drop]\n    omega\n\nend Hunch.ChunkedSequence\n"}],"scope":{"obligations":["cost_accounting"],"assumptions":["Insertion index is at most original element length.","Deletion count is at most the remaining suffix length."],"cost_metric":"custom","model_scope":"Reference splice over flattened chunks: take n, append inserted contents, drop n+deleted.","implementation":"","correspondence":"abstract_model","limitations":["Counts output elements, not edit cost or encoded bytes.","No optimality, balance, cached-measure, performance or Unicode-indexing theorem."]}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/20/proof","source_url":"/api/v1/submissions/20/source","source_hash":"d8d6cb5d0e97e833ea673c7a142c596ad9a56d4ae033d05402beb5076224f0ba","proof_bytes":35,"proof_format":"term-trimmed-v1"}