Structural laws for the existing framed list decoder

TheoremParsing a framed head leaves the raw remainder#✓fully proved

Parsing a framed head leaves exactly the raw remainder, including any later framing failure. The decoder's fuel does not alter this law.

theorem blocks_delimit (p r : List Bool) :
    undelimitBlocks (delimit p ++ r) =
      (undelimitBlocks r).map (p :: ·)

Uses 5 · Used by 1

Statement usesSelf-delimiting form of a bitstring · Parsing a list of booleans into self-delimiting blocks

Proof usesParsing a self-delimiting block · Parsing one self-delimiting block · Bounded parsing of self-delimiting blocks

Used byList decoder consumes one raw payload at a time

TheoremList decoder consumes one raw payload at a time#✓fully proved

The canonical list decoder consumes one raw payload at a time. Both element failure and later framing failure are retained exactly.

theorem decode_list_delimit {α : Type} [MetaMathlibExt.BitstringEncoding α]
    (p r : List Bool) :
    bitDecode (α := List α) (delimit p ++ r) =
      (bitDecode (α := α) p).bind (fun a =>
        (bitDecode (α := List α) r).map (a :: ·))

Uses 9 · Used by 3

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesParsing a framed head leaves the raw remainder

Used byPair-list projector main loop emits both lists in reverse · Projected pair lists total at most four times the input length · Pair-list projector fails on malformed input in linear time

TheoremMalformed first frame makes list decoding fail#✓fully proved

A nonempty input with a malformed first frame fails list decoding. Empty input is excluded because it is the valid empty list.

theorem decode_list_none_of_undelimit_none {α : Type}
    [MetaMathlibExt.BitstringEncoding α] {x : List Bool}
    (hx : x ≠ []) (h : undelimit x = none) :
    bitDecode (α := List α) x = none

Uses 8

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.