{"version":3,"kind":"module","module":{"id":2,"user_id":"cef483b5-8f5a-40e6-b0b3-f82d7a8be13a","title":"Chunked sequence semantics: concatenation, split, measure and splice","namespace":"ChunkedSequence","description":"Reusable reference semantics for a sequence stored as a list of chunks. Proves concatenation denotation, split/rejoin at any index, total element count and bounded splice length. Element positions are generic sequence elements, not UTF-8 bytes or grapheme clusters. This module does not model balancing, cached measures, logarithmic complexity, or a native rope implementation.","profile":"std","declarations":[{"kind":"definition","name":"contents","type":"(A : Type) → List (List A) → List A","value":"fun _ chunks => chunks.flatten"},{"kind":"definition","name":"splitAt","type":"(A : Type) → Nat → List (List A) → List A × List A","value":"fun A n chunks => ((contents A chunks).take n, (contents A chunks).drop n)"},{"kind":"definition","name":"splice","type":"(A : Type) → Nat → Nat → List (List A) → List (List A) → List A","value":"fun A n deleted inserted chunks => (contents A chunks).take n ++ contents A inserted ++ (contents A chunks).drop (n + deleted)"},{"kind":"lemma","name":"concat_contents","type":"∀ (A : Type) (xs ys : List (List A)), contents A (xs ++ ys) = contents A xs ++ contents A ys","value":"by\n  intro A xs ys\n  exact List.flatten_append"},{"kind":"lemma","name":"split_roundtrip","type":"∀ (A : Type) (n : Nat) (chunks : List (List A)), (splitAt A n chunks).1 ++ (splitAt A n chunks).2 = contents A chunks","value":"by\n  intro A n chunks\n  exact List.take_append_drop n (contents A chunks)"},{"kind":"lemma","name":"measure_correct","type":"∀ (A : Type) (chunks : List (List A)), (contents A chunks).length = (chunks.map List.length).sum","value":"by\n  intro A chunks\n  induction chunks with\n  | nil => rfl\n  | cons chunk rest ih => simp [contents] at ih ⊢"},{"kind":"lemma","name":"splice_length","type":"∀ (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","value":"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"}],"module_pins":[],"module_context":[],"module_hash":"9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc","status":"verified","check_log":"'_private.0.Hunch.ChunkedSequence.contents' does not depend on any axioms\n'_private.0.Hunch.ChunkedSequence.splitAt' does not depend on any axioms\n'_private.0.Hunch.ChunkedSequence.splice' does not depend on any axioms\n'_private.0.Hunch.ChunkedSequence.concat_contents' depends on axioms: [propext]\n'_private.0.Hunch.ChunkedSequence.split_roundtrip' does not depend on any axioms\n'_private.0.Hunch.ChunkedSequence.measure_correct' depends on axioms: [propext]\n'_private.0.Hunch.ChunkedSequence.splice_length' depends on axioms: [propext, Quot.sound]\n'_private.0.OA_target' does not depend on any axioms\nOA_target : OA_statement","axioms":["propext","Quot.sound"],"created_at":1791445329,"checked_at":1791445351,"hidden_at":null,"secondary_status":"not_run","secondary_details":null,"origin_submission_id":null,"origin_source_hash":null},"problem":{"statement":"True","profile":"std","module_context":[],"module_pins":[],"module_declarations":[{"kind":"definition","name":"contents","type":"(A : Type) → List (List A) → List A","value":"fun _ chunks => chunks.flatten"},{"kind":"definition","name":"splitAt","type":"(A : Type) → Nat → List (List A) → List A × List A","value":"fun A n chunks => ((contents A chunks).take n, (contents A chunks).drop n)"},{"kind":"definition","name":"splice","type":"(A : Type) → Nat → Nat → List (List A) → List (List A) → List A","value":"fun A n deleted inserted chunks => (contents A chunks).take n ++ contents A inserted ++ (contents A chunks).drop (n + deleted)"},{"kind":"lemma","name":"concat_contents","type":"∀ (A : Type) (xs ys : List (List A)), contents A (xs ++ ys) = contents A xs ++ contents A ys","value":"by\n  intro A xs ys\n  exact List.flatten_append"},{"kind":"lemma","name":"split_roundtrip","type":"∀ (A : Type) (n : Nat) (chunks : List (List A)), (splitAt A n chunks).1 ++ (splitAt A n chunks).2 = contents A chunks","value":"by\n  intro A n chunks\n  exact List.take_append_drop n (contents A chunks)"},{"kind":"lemma","name":"measure_correct","type":"∀ (A : Type) (chunks : List (List A)), (contents A chunks).length = (chunks.map List.length).sum","value":"by\n  intro A chunks\n  induction chunks with\n  | nil => rfl\n  | cons chunk rest ih => simp [contents] at ih ⊢"},{"kind":"lemma","name":"splice_length","type":"∀ (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","value":"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"}],"namespace":"ChunkedSequence"},"profile":"std","policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","proof":"by trivial","statement_hash":"494cd5346575cc8ca180c5212480b7f23c5adefc25326303724bc72576e2df9d","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 := (True)\n\ntheorem OA_target : OA_statement :=\n  by trivial\n\n#print axioms Hunch.ChunkedSequence.contents\n#print axioms Hunch.ChunkedSequence.splitAt\n#print axioms Hunch.ChunkedSequence.splice\n#print axioms Hunch.ChunkedSequence.concat_contents\n#print axioms Hunch.ChunkedSequence.split_roundtrip\n#print axioms Hunch.ChunkedSequence.measure_correct\n#print axioms Hunch.ChunkedSequence.splice_length\n#print axioms OA_target\n#check OA_target\n"}