Main internal data type for the rose tree machine (RTM)

This file contains the main internal data structure for the RTM, Data, a rose tree.

Main definitions and notations

• Data - the main data structure
• Data.size - the size of a Data object when encoded using parentheses, complexity results use this size as the main measure.
• Data.toBits - a parenthesized (balanced-bracket) serialization into List Bool, with length equal to Data.size, and injective (Data.toBits_injective).
• Data.recL - the main recursion principle for Data
• Data.inductionL - the main induction principle for Data

inductive Complexity.Data : Type

Rose-tree data structure, it allows us to encode most of Lean's data structures in a "natural" manner

• l : List Data → Data

@[implicit_reducible]

instance Complexity.instReprData : Repr Data

Equations

• Complexity.instReprData = { reprPrec := Complexity.instReprData.repr }

partial def Complexity.instReprData.repr : Data → ℕ → Std.Format

def Complexity.Data.decEq (a b : Data) : Decidable (a = b)

Decidable equality for Data, defined jointly with Data.listDecEq.

Equations

• (Complexity.Data.l xs).decEq (Complexity.Data.l ys) = match Complexity.Data.listDecEq xs ys with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

def Complexity.Data.listDecEq (xs ys : List Data) : Decidable (xs = ys)

Decidable equality for List Data, defined jointly with Data.decEq.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Data.listDecEq [] [] = isTrue Complexity.Data.listDecEq._proof_1✝
• Complexity.Data.listDecEq [] (head :: tail) = isFalse ⋯
• Complexity.Data.listDecEq (head :: tail) [] = isFalse ⋯

@[implicit_reducible]

instance Complexity.instDecidableEqData : DecidableEq Data

Equations

• Complexity.instDecidableEqData = Complexity.Data.decEq

@[implicit_reducible]

instance Complexity.instBEqData : BEq Data

Equations

• Complexity.instBEqData = inferInstance

instance Complexity.instLawfulBEqData : LawfulBEq Data

@[reducible, inline]

abbrev Complexity.Data.empty : Data

The empty Data node, Data.l [].

Equations

• Complexity.Data.empty = Complexity.Data.l []

def Complexity.Data.asList : Data → List Data

The list of children of a Data node.

Equations

• (Complexity.Data.l a).asList = a

theorem Complexity.Data.asList_empty : empty.asList = []

@[simp]

theorem Complexity.Data.asList_l (d : Data) : l d.asList = d

@[simp]

theorem Complexity.Data.l_asList (xs : List Data) : (l xs).asList = xs

@[irreducible]

def Complexity.Data.size : Data → ℕ

The encoding length of d, relevant for complexity. This is the encoded size assuming an encoding into parenthesized expressions.

Equations

• (Complexity.Data.l a).size = 2 + (List.map Complexity.Data.size a).sum

@[simp]

theorem Complexity.Data.size_le {d : Data} : 0 < d.size

@[simp]

theorem Complexity.Data.size_empty : empty.size = 2

@[simp]

theorem Complexity.Data.cons_size {h : Data} {t : List Data} : (l (h :: t)).size = h.size + (l t).size

theorem Complexity.Data.size_lt_of_mem {c : Data} {xs : List Data} (hc : c ∈ xs) : c.size < (l xs).size

@[irreducible]

def Complexity.Data.recL {motive : Data → Sort u_1} (nil : motive (l [])) (cons : (x : Data) → (xs : List Data) → motive x → motive (l xs) → motive (l (x :: xs))) (d : Data) : motive d

Recursion principle for Data.

Equations

• Complexity.Data.recL nil cons (Complexity.Data.l []) = nil
• Complexity.Data.recL nil cons (Complexity.Data.l (x_1 :: xs)) = cons x_1 xs (Complexity.Data.recL nil cons x_1) (Complexity.Data.recL nil cons (Complexity.Data.l xs))

theorem Complexity.Data.inductionL {motive : Data → Prop} (nil : motive (l [])) (cons : ∀ (x : Data) (xs : List Data), motive x → motive (l xs) → motive (l (x :: xs))) (d : Data) : motive d

Induction principle for Data, the Prop-valued companion to Data.recL.

Bitstring serialization

Data.toBits serializes a Data value into a List Bool using a parenthesized (balanced-bracket) encoding: false opens a node, its children are serialized in order, and true closes the node. This matches Data.size exactly (Data.length_toBits) and is injective (Data.toBits_injective), so any DataEncode instance yields an injective bitstring encoding (see Complexitylib.Encoding.DataEncode).

@[irreducible]

def Complexity.Data.toBits : Data → List Bool

Serialize Data into a bitstring with a parenthesized (balanced-bracket) encoding: false opens a node, the children are serialized in order, and true closes the node.

Equations

• (Complexity.Data.l a).toBits = false :: ((List.map Complexity.Data.toBits a).flatten ++ [true])

theorem Complexity.Data.toBits_l (xs : List Data) : (l xs).toBits = false :: ((List.map toBits xs).flatten ++ [true])

@[simp]

theorem Complexity.Data.length_toBits (d : Data) : d.toBits.length = d.size

def Complexity.Data.fromBitsStep : Option (List (List Data)) → Bool → Option (List (List Data))

One step of the stack-based Data.fromBits parser. The state is a stack of frames, each a list of the sibling nodes completed so far at that nesting depth (outermost frame at the bottom). Reading false opens a new (empty) frame; reading true closes the top frame into a Data.l node and appends it to its parent. none is a permanent failure state (an unmatched true).

Equations

• Complexity.Data.fromBitsStep none x✝ = none
• Complexity.Data.fromBitsStep (some stack) false = some ([] :: stack)
• Complexity.Data.fromBitsStep (some (kids :: parent :: rest)) true = some ((parent ++ [Complexity.Data.l kids]) :: rest)
• Complexity.Data.fromBitsStep (some stack) true = none

def Complexity.Data.fromBits (bits : List Bool) : Option Data

Decode a bitstring produced by Data.toBits back into a Data value, or none if it is not a valid single serialization. This is a left inverse of Data.toBits (Data.fromBits_toBits).

Equations

• Complexity.Data.fromBits bits = match List.foldl Complexity.Data.fromBitsStep (some [[]]) bits with | some [[d]] => some d | x => none

theorem Complexity.Data.foldl_fromBitsStep_toBits (d : Data) (top : List Data) (rest : List (List Data)) : List.foldl fromBitsStep (some (top :: rest)) d.toBits = some ((top ++ [d]) :: rest)

Running Data.fromBitsStep over d.toBits appends the decoded d to the top frame of the stack, leaving the rest of the stack untouched. This is the key lemma behind Data.fromBits_toBits.

@[simp]

theorem Complexity.Data.fromBits_toBits (d : Data) : fromBits d.toBits = some d

Data.fromBits recovers any value serialized by Data.toBits.

theorem Complexity.Data.toBits_injective : Function.Injective toBits

Data.toBits is injective: the parenthesized serialization determines the value. This follows from Data.fromBits being a left inverse.