Chunked sequence semantics: concatenation, split, measure and splice

Module verified

verified

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.

Namespace: Hunch.ChunkedSequence

SHA-256: 9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc

Definitions and named lemmas

namespace Hunch.ChunkedSequence
def contents : ((A : Type) → List (List A) → List A) :=
  fun _ chunks => chunks.flatten

def splitAt : ((A : Type) → Nat → List (List A) → List A × List A) :=
  fun A n chunks => ((contents A chunks).take n, (contents A chunks).drop n)

def splice : ((A : Type) → Nat → Nat → List (List A) → List (List A) → List A) :=
  fun A n deleted inserted chunks => (contents A chunks).take n ++ contents A inserted ++ (contents A chunks).drop (n + deleted)

theorem concat_contents : (∀ (A : Type) (xs ys : List (List A)), contents A (xs ++ ys) = contents A xs ++ contents A ys) :=
  by
    intro A xs ys
    exact List.flatten_append

theorem split_roundtrip : (∀ (A : Type) (n : Nat) (chunks : List (List A)), (splitAt A n chunks).1 ++ (splitAt A n chunks).2 = contents A chunks) :=
  by
    intro A n chunks
    exact List.take_append_drop n (contents A chunks)

theorem measure_correct : (∀ (A : Type) (chunks : List (List A)), (contents A chunks).length = (chunks.map List.length).sum) :=
  by
    intro A chunks
    induction chunks with
    | nil => rfl
    | cons chunk rest ih => simp [contents] at ih ⊢

theorem 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) :=
  by
    intro A n deleted inserted chunks hn hd
    simp only [splice, List.length_append, List.length_take, List.length_drop]
    omega

end Hunch.ChunkedSequence

Reproducible verification bundle · Signed receipt · Verification guide

Report module

Checker output

'_private.0.Hunch.ChunkedSequence.contents' does not depend on any axioms
'_private.0.Hunch.ChunkedSequence.splitAt' does not depend on any axioms
'_private.0.Hunch.ChunkedSequence.splice' does not depend on any axioms
'_private.0.Hunch.ChunkedSequence.concat_contents' depends on axioms: [propext]
'_private.0.Hunch.ChunkedSequence.split_roundtrip' does not depend on any axioms
'_private.0.Hunch.ChunkedSequence.measure_correct' depends on axioms: [propext]
'_private.0.Hunch.ChunkedSequence.splice_length' depends on axioms: [propext, Quot.sound]
'_private.0.OA_target' does not depend on any axioms
OA_target : OA_statement

To use this module, pin {"id":2,"hash":"9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc"} in your target’s modules array. Only independently verified modules can be used.