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.recL - the main recursion principle for Data
• Data.inductionL - the main induction principle for Data

inductive Complexity.RoseTreeMachine.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.RoseTreeMachine.instReprData : Repr Data

Equations

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

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

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

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

Equations

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

def Complexity.RoseTreeMachine.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.RoseTreeMachine.Data.listDecEq [] [] = isTrue Complexity.RoseTreeMachine.Data.listDecEq._proof_1
• Complexity.RoseTreeMachine.Data.listDecEq [] (head :: tail) = isFalse ⋯
• Complexity.RoseTreeMachine.Data.listDecEq (head :: tail) [] = isFalse ⋯

@[implicit_reducible]

instance Complexity.RoseTreeMachine.instDecidableEqData : DecidableEq Data

Equations

• Complexity.RoseTreeMachine.instDecidableEqData = Complexity.RoseTreeMachine.Data.decEq

@[implicit_reducible]

instance Complexity.RoseTreeMachine.instBEqData : BEq Data

Equations

• Complexity.RoseTreeMachine.instBEqData = inferInstance

instance Complexity.RoseTreeMachine.instLawfulBEqData : LawfulBEq Data

@[reducible, inline]

abbrev Complexity.RoseTreeMachine.Data.empty : Data

The empty Data node, Data.l [].

Equations

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

def Complexity.RoseTreeMachine.Data.asList : Data → List Data

The list of children of a Data node.

Equations

• (Complexity.RoseTreeMachine.Data.l xs).asList = xs

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

@[simp]

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

@[simp]

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

@[irreducible]

def Complexity.RoseTreeMachine.Data.size : Data → ℕ

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[irreducible]

def Complexity.RoseTreeMachine.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

• One or more equations did not get rendered due to their size.
• Complexity.RoseTreeMachine.Data.recL nil cons (Complexity.RoseTreeMachine.Data.l []) = nil

theorem Complexity.RoseTreeMachine.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.

@[reducible, inline]

abbrev Complexity.RoseTreeMachine.TapeIndex : Type

Index of a tape cell used by the rose tree machine's execution model.

Equations

• Complexity.RoseTreeMachine.TapeIndex = ℕ