Binary trees are encodable

A binary tree is a W-type: its shapes are a leaf and a node labelled by a value, with no children and two children respectively. Mathlib's W-types over encodable shapes with finite encodable arities are encodable, so binary trees over an encodable type are too, and binary trees over a countable type are countable. Mathlib.Data.Tree.Basic provides neither instance.

Main declarations

• BinaryTree.toWType, BinaryTree.ofWType: a binary tree as a W-type and back.
• The Encodable and Countable instances for BinaryTree α.

[UPSTREAM] candidate for Mathlib.Data.Tree.Basic.

def BinaryTree.WArity {α : Type u_1} : Option α → Type

The arity of a binary-tree shape: a leaf has no children and a node two.

Equations

• BinaryTree.WArity none = Empty
• BinaryTree.WArity (some val) = Bool

@[instance_reducible]

instance BinaryTree.instFintypeWArity {α : Type u_1} (a : Option α) : Fintype (WArity a)

Equations

• BinaryTree.instFintypeWArity none = { elems := BinaryTree.instFintypeWArity._aux_1, complete := ⋯ }
• BinaryTree.instFintypeWArity (some val) = { elems := BinaryTree.instFintypeWArity._aux_4 val, complete := ⋯ }

@[instance_reducible]

instance BinaryTree.instEncodableWArity {α : Type u_1} (a : Option α) : Encodable (WArity a)

Equations

• BinaryTree.instEncodableWArity none = { encode := BinaryTree.instEncodableWArity._aux_1, decode := BinaryTree.instEncodableWArity._aux_3, encodek := ⋯ }
• BinaryTree.instEncodableWArity (some val) = { encode := BinaryTree.instEncodableWArity._aux_6 val, decode := BinaryTree.instEncodableWArity._aux_8 val, encodek := ⋯ }

def BinaryTree.toWType {α : Type u_1} : BinaryTree α → WType WArity

A binary tree as a W-type: a leaf has the shape none, a node the shape of its value, with its left subtree at true and its right subtree at false.

Equations

• BinaryTree.nil.toWType = WType.mk none Empty.elim
• (BinaryTree.node a l r).toWType = WType.mk (some a) fun (b : BinaryTree.WArity (some a)) => bif b then l.toWType else r.toWType

def BinaryTree.ofWType {α : Type u_1} : WType WArity → BinaryTree α

A W-type of binary-tree shapes as a binary tree.

Equations

• BinaryTree.ofWType (WType.mk none f) = BinaryTree.nil
• BinaryTree.ofWType (WType.mk (some a) f) = BinaryTree.node a (BinaryTree.ofWType (f true)) (BinaryTree.ofWType (f false))

theorem BinaryTree.ofWType_toWType {α : Type u_1} (t : BinaryTree α) : ofWType t.toWType = t

@[instance_reducible]

instance BinaryTree.instEncodable_linglib {α : Type u_1} [Encodable α] : Encodable (BinaryTree α)

Equations

• BinaryTree.instEncodable_linglib = Encodable.ofLeftInverse BinaryTree.toWType BinaryTree.ofWType ⋯

instance BinaryTree.instCountable_linglib {α : Type u_1} [Countable α] : Countable (BinaryTree α)