{"version":3,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"std","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"],"statement_hash":"65c8b5fe5e8d97d87b554ee5e4ab010ddb7650f7cba418b00ea8c2e3b96c3fb5","problem":{"id":34,"title":"Chunked sequences: concatenation, split round-trip and exact element measure","description":"A reusable reference model for ropes and chunked strings. Flattening chunk concatenation equals concatenation of flattened contents. Splitting the flattened sequence at any natural index and rejoining returns the original contents, including out-of-range indices. The element length equals the sum of chunk lengths. These generic list laws are useful specifications for a future balanced rope refinement. They do not verify balancing, cached measures, Unicode byte/grapheme offsets or runtime complexity. The external Isabelle finger-tree development supplies a richer measured-tree model; incomplete Coq wrapper results are separately qualified.","statement":"∀ (A : Type) (n : Nat) (xs ys : List (List A)), Hunch.ChunkedSequence.contents A (xs ++ ys) = Hunch.ChunkedSequence.contents A xs ++ Hunch.ChunkedSequence.contents A ys ∧ (Hunch.ChunkedSequence.splitAt A n xs).1 ++ (Hunch.ChunkedSequence.splitAt A n xs).2 = Hunch.ChunkedSequence.contents A xs ∧ (Hunch.ChunkedSequence.contents A xs).length = (xs.map List.length).sum","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":["round_trip","composition","cost_accounting"],"assumptions":["No index bound is required for split/rejoin.","Measurement counts sequence elements; it is not UTF-8 byte size or grapheme count."],"cost_metric":"custom","model_scope":"List of arbitrary-element chunks; contents is list flattening; splitAt uses take/drop on contents.","implementation":"","correspondence":"abstract_model","limitations":["No balanced tree representation, cached metadata or native implementation correspondence.","No runtime or memory bound."]}},"source":"import Std\nimport Batteries\nimport Lean.Elab.Tactic.Omega\n\nnamespace 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\ndef OA_statement : Prop := (∀ (A : Type) (n : Nat) (xs ys : List (List A)), Hunch.ChunkedSequence.contents A (xs ++ ys) = Hunch.ChunkedSequence.contents A xs ++ Hunch.ChunkedSequence.contents A ys ∧ (Hunch.ChunkedSequence.splitAt A n xs).1 ++ (Hunch.ChunkedSequence.splitAt A n xs).2 = Hunch.ChunkedSequence.contents A xs ∧ (Hunch.ChunkedSequence.contents A xs).length = (xs.map List.length).sum)\n\n#check OA_statement\n","proof":null}