Inductive types and trees

As we have seen, inductive types are given by constructors. To fully understand these, we must understand:

• What are the allowed types of the constructors?
• What are the corresponding types of the rec functions?
• What identities are satisfied by these?

Since the constructs give elements of T, they must be (dependent) functions with codomain T, or (dependent) functions with codomain (dependent) functions with codomain T, etc. Thus, possible types of constructors are:

• T.
• If X (= ... → T) is a possible type and A is defined in the context, then A → X.
• If X (= ... → T) is a possible type, then T → X.
• If X (= ... → T) is a possible type and A is defined in the context, then (A → T) → X is a possible type (we can generalize to A → B → T etc. and families).

Parameterized inductive types

We also have parametrized inductive types like lists, where we are defining a family of types List α for each α. In this case, the constructors can depend on the parameter α.

To be precise, a family of types is one of:

• A type T : Type u.
• Given a type A and a family of types X, the type A → X.
• Given a type A, and, for each a : A, a family of types X a, the type Π (a : A), X a = (a: A) → X a.
• Given a type A and a family of types X, the type List A → X (this is in Lean, but not, for example in Homotopy Type Theory).

Indexed inductive types

This is a more subtle notion. We will return to this later. We have already seen an example of this: MyNat.le is an indexed inductive type.

Trees

We see various kinds of trees, giving various inductive types.

inductive BinTree (α : Type) : Type

• leaf {α : Type} (label : α) : BinTree α
• node {α : Type} : BinTree α → BinTree α → BinTree α

instance instInhabitedBinTree {a✝ : Type} [Inhabited a✝] : Inhabited (BinTree a✝)

Equations

• instInhabitedBinTree = { default := BinTree.leaf default }

instance instReprBinTree {α✝ : Type} [Repr α✝] : Repr (BinTree α✝)

Equations

• instReprBinTree = { reprPrec := reprBinTree✝ }

def BinTree.eg₁ : BinTree ℕ

Equations

• BinTree.eg₁ = BinTree.leaf 3

def BinTree.eg₂ : BinTree ℕ

Equations

• BinTree.eg₂ = (BinTree.leaf 3).node (BinTree.leaf 4)

def BinTree.eg₃ : BinTree ℕ

Equations

• BinTree.eg₃ = ((BinTree.leaf 3).node (BinTree.leaf 4)).node (BinTree.leaf 5)

def BinTree.toList {α : Type} : BinTree α → List α

Equations

• (BinTree.leaf a).toList = [a]
• (a.node a_1).toList = a.toList ++ a_1.toList

def BinTree.sum : BinTree ℕ → ℕ

Equations

• (BinTree.leaf a).sum = a
• (t₁.node t₂).sum = t₁.sum + t₂.sum

noncomputable def BinTree.sum' : BinTree ℕ → ℕ

Equations

• BinTree.sum' = BinTree.rec (fun (a : ℕ) => a) fun (_t₁ _t₂ : BinTree ℕ) (sum₁ sum₂ : ℕ) => sum₁ + sum₂

theorem BinTree.sum'_leaf (a : ℕ) : (BinTree.leaf a).sum' = a

theorem BinTree.sum'_node (t₁ t₂ : BinTree ℕ) : (t₁.node t₂).sum' = t₁.sum' + t₂.sum'

inductive BinTree' (α : Type) : Type

• node {α : Type} : BinTree' α → BinTree' α → BinTree' α
• leaf {α : Type} (label : α) : BinTree' α

instance instInhabitedBinTree' {a✝ : Type} [Inhabited a✝] : Inhabited (BinTree' a✝)

Equations

• instInhabitedBinTree' = { default := BinTree'.leaf default }

instance instReprBinTree' {α✝ : Type} [Repr α✝] : Repr (BinTree' α✝)

Equations

• instReprBinTree' = { reprPrec := reprBinTree'✝ }

def natListSum : List ℕ → ℕ

Equations

• natListSum [] = 0
• natListSum (head :: tail) = head + natListSum tail

inductive BoolTree (α : Type) : Type

• leaf {α : Type} (a : α) : BoolTree α
• node {α : Type} : (Bool → BoolTree α) → BoolTree α

def BoolTree.eg₁ : BoolTree ℕ

Equations

• BoolTree.eg₁ = BoolTree.leaf 3

def BoolTree.eg₂ : BoolTree ℕ

Equations

• BoolTree.eg₂ = BoolTree.node fun (x : Bool) => BoolTree.leaf 3

def BoolTree.eg₃ : BoolTree ℕ

Equations

• BoolTree.eg₃ = BoolTree.node fun (b : Bool) => if b = true then BoolTree.leaf 3 else BoolTree.leaf 4

def BoolTree.toList {α : Type} : BoolTree α → List α

Equations

• (BoolTree.leaf a).toList = [a]
• (BoolTree.node f).toList = (f true).toList ++ (f false).toList

def BoolTree.toBinTree {α : Type} : BoolTree α → BinTree α

Equations

• (BoolTree.leaf a).toBinTree = BinTree.leaf a
• (BoolTree.node f).toBinTree = (f true).toBinTree.node (f false).toBinTree

def BoolTree.ofBinTree {α : Type} : BinTree α → BoolTree α

Equations

• BoolTree.ofBinTree (BinTree.leaf a) = BoolTree.leaf a
• BoolTree.ofBinTree (a.node a_1) = BoolTree.node fun (b : Bool) => if b = true then BoolTree.ofBinTree a else BoolTree.ofBinTree a_1

inductive ListTree (α : Type) : Type

• leaf {α : Type} (a : α) : ListTree α
• node {α : Type} : List (ListTree α) → ListTree α

instance instInhabitedListTree {a✝ : Type} : Inhabited (ListTree a✝)

Equations

• instInhabitedListTree = { default := ListTree.node default }

instance instReprListTree {α✝ : Type} [Repr α✝] : Repr (ListTree α✝)

Equations

• instReprListTree = { reprPrec := reprListTree✝ }

def ListTree.eg₁ : ListTree ℕ

Equations

• ListTree.eg₁ = ListTree.leaf 3

def ListTree.eg₂ : ListTree ℕ

Equations

• ListTree.eg₂ = ListTree.node [ListTree.leaf 3, ListTree.leaf 4]

def ListTree.eg₃ : ListTree ℕ

Equations

• ListTree.eg₃ = ListTree.node [ListTree.node [ListTree.leaf 3, ListTree.leaf 4], ListTree.leaf 5]

def ListTree.eg₄ : ListTree ℕ

Equations

• ListTree.eg₄ = ListTree.node []

@[irreducible]

def ListTree.toList {α : Type} : ListTree α → List α

Equations

• (ListTree.leaf a).toList = [a]
• (ListTree.node []).toList = []
• (ListTree.node (t :: ts)).toList = t.toList ++ (ListTree.node ts).toList

Lean is pragmatic and allows imperative programming. We can define the sum of a list. Technically, this is in a monad.

def listSumNat (l : List ℕ) : ℕ

Equations

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

def listSumNat' (l : List ℕ) : ℤ

Equations

• listSumNat' l = List.foldl (fun (sum : ℤ) (n : ℕ) => sum + ↑n) 0 l

def evens : List ℕ → List Bool

Equations

• evens = List.map fun (n : ℕ) => n % 2 == 0

def evensProp : List ℕ → List Prop

Equations

• evensProp = List.map fun (n : ℕ) => n % 2 = 0

def listTill : ℕ → List ℕ

Equations

• listTill 0 = []
• listTill n.succ = n :: listTill n

def listTillFlat (n : ℕ) : List ℕ

Equations

• listTillFlat n = (listTill n).flatMap listTill

inductive FinTree (α : Type) : Type

• leaf {α : Type} (a : α) : FinTree α
• node {α : Type} {n : ℕ} : (Fin n → FinTree α) → FinTree α

def FinTree.ofBinTree {α : Type} : BinTree α → FinTree α

Equations

• FinTree.ofBinTree (BinTree.leaf a) = FinTree.leaf a
• FinTree.ofBinTree (a.node a_1) = FinTree.node fun (k : Fin 2) => match k with | ⟨0, _pf⟩ => FinTree.ofBinTree a | ⟨1, _pf⟩ => FinTree.ofBinTree a_1

def FinTree.eg : FinTree ℕ

Equations

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

opaque CantorTree.T' : Type

inductive CantorTree.T : Type

• node : (CantorTree.T' → Bool) → CantorTree.T

axiom CantorTree.TisT' : CantorTree.T = CantorTree.T'

The idea of Cantor's theorem is to show that we can define p: T → Bool such that p (node p) ≠ p p. If not for the positivity condition, we could define p (node x) = ¬ x (node x).

def CantorTree.flip : CantorTree.T → Bool

Equations

• CantorTree.flip (CantorTree.T.node p) = !p (CantorTree.TisT' ▸ CantorTree.T.node p)

def CantorTree.flip' : CantorTree.T' → Bool

Equations

• CantorTree.flip' = Eq.rec (motive := fun (x : Type) (h : CantorTree.T = x) => x → Bool) CantorTree.flip CantorTree.TisT'

theorem CantorTree.flip_contra : CantorTree.flip (CantorTree.T.node CantorTree.flip') = !CantorTree.flip' (CantorTree.TisT' ▸ CantorTree.T.node CantorTree.flip')