Encodings into Data

This file defines the class that is used to encode arbitrary data structures into Data, so that RTMs (rose tree machines) can operate on them.

Instances are provided for convenience for Data itself, Bool, List α, Option α, α × β, and ℕ (binary encoding via List Bool)

Every DataEncode instance also yields a bitstring encoding DataEncode.bitstringEncode, by serializing the target Data value with Data.toBits. Since both the DataEncode instance and Data.toBits are injective, bitstringEncode is injective too (DataEncode.bitstringEncode_injective).

class Complexity.DataEncode (α : Type) : Type

Encoding of types into Data.

• encode : α → Data

  Encode a value of α as Data.

• h_inj : Function.Injective encode

  The encoding is injective, so distinct values never collide.

@[implicit_reducible]

instance Complexity.instDataEncodeData : DataEncode Data

Equations

• Complexity.instDataEncodeData = { encode := fun (b : Complexity.Data) => b, h_inj := Complexity.instDataEncodeData._proof_2 }

@[simp]

theorem Complexity.DataEncode_encode_data (d : Data) : DataEncode.encode d = d

@[implicit_reducible]

instance Complexity.instDataEncodeBool : DataEncode Bool

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.instDataEncodeList (α : Type) [DataEncode α] : DataEncode (List α)

Equations

• Complexity.instDataEncodeList α = { encode := fun (xs : List α) => Complexity.Data.l (List.map Complexity.DataEncode.encode xs), h_inj := ⋯ }

@[simp]

theorem Complexity.DataEncode_list_nil {α : Type} [DataEncode α] : DataEncode.encode [] = Data.l []

@[simp]

theorem Complexity.DataEncode_list_eq_nil_iff_nil {α : Type} [DataEncode α] (xs : List α) : DataEncode.encode xs = Data.empty ↔ xs = []

@[simp]

theorem Complexity.DataEncode_list_tail {α : Type} [DataEncode α] (xs : List α) : (DataEncode.encode xs).asList.tail = (DataEncode.encode xs.tail).asList

@[implicit_reducible]

instance Complexity.instDataEncodeOption (α : Type) [DataEncode α] : DataEncode (Option α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.DataEncode_Option_empty {α : Type} [DataEncode α] (x : Option α) : (DataEncode.encode x == Data.empty) = x.isNone

@[implicit_reducible]

instance Complexity.instDataEncodeProd (α β : Type) [DataEncode α] [DataEncode β] : DataEncode (α × β)

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DataEncode_pair {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) : DataEncode.encode (a, b) = Data.l [DataEncode.encode a, DataEncode.encode b]

@[implicit_reducible]

instance Complexity.instDataEncodeNat : DataEncode ℕ

Equations

• Complexity.instDataEncodeNat = { encode := fun (x : ℕ) => Complexity.DataEncode.encode x.bits, h_inj := Complexity.instDataEncodeNat._proof_1 }

def Complexity.DataEncode.bitstringEncode {α : Type} [DataEncode α] (a : α) : List Bool

Encode a value into a bitstring (List Bool) by first encoding it into Data and then serializing that with the parenthesized Data.toBits. This is the class-inferrable bitstring encoding available for any type with a DataEncode instance.

Equations

• Complexity.DataEncode.bitstringEncode a = (Complexity.DataEncode.encode a).toBits

theorem Complexity.DataEncode.bitstringEncode_def {α : Type} [DataEncode α] (a : α) : bitstringEncode a = (encode a).toBits

theorem Complexity.DataEncode.bitstringEncode_injective {α : Type} [DataEncode α] : Function.Injective bitstringEncode

The bitstring encoding is injective: distinct values yield distinct bitstrings. This composes the injectivity of the DataEncode instance with that of Data.toBits.