Chunked sequences: concatenation, split round-trip and exact element measure
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
- round trip, composition, cost accounting
- Cost metric
- custom
- Model
- List of arbitrary-element chunks; contents is list flattening; splitAt uses take/drop on contents.
- Assumptions
- No index bound is required for split/rejoin. Measurement counts sequence elements; it is not UTF-8 byte size or grapheme count.
- Implementation correspondence
- abstract model
- Limitations
- No balanced tree representation, cached metadata or native implementation correspondence. No runtime or memory bound.
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.
Formal 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
Standard library — lists, arrays, maps · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 65c8b5fe5e8d97d87b554ee5e4ab010ddb7650f7cba418b00ea8c2e3b96c3fb5
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.