Tree Evaluation instances of all sizes

Cslib.TreeEval.Instance collects the instances of all value lengths and heights, and Cslib.TreeEval.encInstance encodes them injectively by Cslib.TreeEval.Tree.encode: the header determines the value length and the height, and the body determines the tree, as the table of a gate determines the gate.

Main definitions

• Cslib.TreeEval.Instance: an instance of some value length and height.
• Cslib.TreeEval.encInstance: the encoding of instances.

Main results

• Cslib.TreeEval.ell_lt_length_encNat_length_encInstance: for 1 ≤ I.height, the value length I.ell is strictly below the binary length of (encInstance I).length.
• Cslib.TreeEval.height_lt_length_encNat_length_encInstance: for 1 ≤ I.ell, the height I.height is strictly below the binary length of (encInstance I).length.

structure Cslib.TreeEval.Instance : Type

A Tree Evaluation instance of some value length and height.

• ell : ℕ

  The value length.

• height : ℕ

  The height.

• tree : Tree self.ell self.height

  The tree.

theorem Cslib.TreeEval.table_injective {ℓ : ℕ} {f g : Gate ℓ} (h : table f = table g) : f = g

The table of a gate determines the gate.

theorem Cslib.TreeEval.Tree.body_injective {ℓ h : ℕ} {T T' : Tree ℓ h} : T.body = T'.body → T = T'

The body determines the tree.

theorem Cslib.TreeEval.encode_injective {I J : Instance} (h : I.tree.encode = J.tree.encode) : I = J

def Cslib.TreeEval.encInstance : Instance ↪ List Bool

The encoding of instances.

@[simp]

theorem Cslib.TreeEval.encInstance_apply (I : Instance) : encInstance I = I.tree.encode

theorem Cslib.TreeEval.length_encInstance (I : Instance) : (encInstance I).length = I.ell + I.height + 2 + bodyLength I.ell I.height

theorem Cslib.TreeEval.two_le_length_encInstance (I : Instance) : 2 ≤ (encInstance I).length

Every encoded instance has at least the two delimiter zeroes of the header.

theorem Cslib.TreeEval.ell_lt_length_encNat_length_encInstance {I : Instance} (hH : 1 ≤ I.height) : I.ell < (Turing.MultiTapeTM.encNat (encInstance I).length).length

For 1 ≤ I.height, the value length I.ell is strictly less than the binary length of the encoded instance length.

theorem Cslib.TreeEval.height_lt_length_encNat_length_encInstance {I : Instance} (hℓ : 1 ≤ I.ell) : I.height < (Turing.MultiTapeTM.encNat (encInstance I).length).length

For 1 ≤ I.ell, the height I.height is strictly less than the binary length of the encoded instance length.