Inductive types for numbers, data, propositions.

What makes the foundations we use work are that the mathematical objects we need as well as their properties can be constructed in terms of inductive types and dependent function types. Similarly, proofs and terms need only a few rules to be constructed.

We will see how to define inductive types for many basic constructions: natural numbers, products, sums (disjoint unions) etc. We will also see the logical connectives ∧ and or as well as quantifiers constructed as inductive types. Further, we see how specific relations like ≤ can be defined as (indexed) inductive types.

inductive MyNat : Type

The natural numbers are defined inductively.

• zero : MyNat
• succ (n : MyNat) : MyNat

instance instReprMyNat : Repr MyNat

Equations

• instReprMyNat = { reprPrec := reprMyNat✝ }

def MyNat.add : MyNat → MyNat → MyNat

The addition function on natural numbers.

Equations

• MyNat.zero #+# x✝ = x✝
• n.succ #+# x✝ = (n #+# x✝).succ

instance MyNat.instAdd : Add MyNat

The addition operation + on natural numbers.

Equations

• MyNat.instAdd = { add := MyNat.add }

theorem MyNat.zero_add (n : MyNat) : MyNat.zero + n = n

Addition on the left by zero. This is by definition.

theorem MyNat.add_zero (n : MyNat) : n + MyNat.zero = n

Addition on the right by zero. This is by induction on n.

def MyNat.«term_#+#_» : Lean.TrailingParserDescr

Equations

• MyNat.«term_#+#_» = Lean.ParserDescr.trailingNode `MyNat.«term_#+#_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " #+# ") (Lean.ParserDescr.cat `term 66))

inductive MyProd (α : Type u) (β : Type v) : Type (max u v)

The product type is defined as an inductive type.

• pair {α : Type u} {β : Type v} (fst : α) (snd : β) : MyProd α β

structure MyProd' (α : Type u) (β : Type v) : Type (max u v)

The product type is defined as a structure.

• fst : α
• snd : β

def MyProd.fst {α : Type u} {β : Type v} : MyProd α β → α

The first projection of a product.

Equations

• (MyProd.pair a snd).fst = a

def MyProd.snd {α : Type u} {β : Type v} : MyProd α β → β

The second projection of a product.

Equations

• (MyProd.pair a snd).snd = snd

inductive MySum (α : Type u) (β : Type v) : Type (max u v)

The sum type, i.e., disjoint union is defined as an inductive type.

• inl {α : Type u} {β : Type v} (a : α) : MySum α β
• inr {α : Type u} {β : Type v} (b : β) : MySum α β

def MySum.eg₁ : MySum Nat String

An example of a term in a sum type.

Equations

• MySum.eg₁ = MySum.inl 1

def MySum.eg₂ : MySum Nat String

An example of a term in a sum type.

Equations

• MySum.eg₂ = MySum.inr "hello"

inductive MyUnit : Type

The Unit type, with a unique element, is defined inductively.

• star : MyUnit

def MyUnit.eg : MyUnit

Equations

• MyUnit.eg = MyUnit.star

inductive MyEmpty : Type

The empty type is defined inductively.

inductive MyFalse : Type

The false proposition is defined as an inductive type.

inductive MyAnd (a b : Prop) : Prop

The conjunction of two propositions is defined as an inductive type.

• mk {a b : Prop} (left : a) (right : b) : MyAnd a b

inductive MyOr (a b : Prop) : Type

The disjunction of two propositions is defined as an inductive type.

• inl {a b : Prop} (left : a) : MyOr a b
• inr {a b : Prop} (right : b) : MyOr a b

inductive MyTrue : Type

The true proposition is defined as an inductive type.

• trivial : MyTrue

inductive MyExists {α : Type u} (p : α → Prop) : Type u

The existential quantifier is defined as an inductive type.

• mk {α : Type u} {p : α → Prop} (w : α) (h : p w) : MyExists p