10. Type Classes🔗

Type classes were introduced as a principled way of enabling ad-hoc polymorphism in functional programming languages. We first observe that it would be easy to implement an ad-hoc polymorphic function (such as addition) if the function simply took the type-specific implementation of addition as an argument and then called that implementation on the remaining arguments. For example, suppose we declare a structure in Lean to hold implementations of addition.

namespace Ex

structure Add (α : Type) where
  add : α → α → α

@Add.add : {α : Type} → Add α → α → α → α#check @Add.add

@Add.add : {α : Type} → Add α → α → α → α

end Ex

In the above Lean code, the field add has type Add.add : {α : Type} → Add α → α → α → α where the curly braces around the type α mean that it is an implicit argument. We could implement double by:

namespace Ex
structure Add (α : Type) where
  add : α → α → α

def double (s : Add α) (x : α) : α :=
  s.add x x

20#eval double { add := Nat.add } 10

100#eval double { add := Nat.mul } 10

20#eval double { add := Int.add } 10

end Ex

Note that you can double a natural number n by double { add := Nat.add } n. Of course, it would be highly cumbersome for users to manually pass the implementations around in this way. Indeed, it would defeat most of the potential benefits of ad-hoc polymorphism.

The main idea behind type classes is to make arguments such as Add α implicit, and to use a database of user-defined instances to synthesize the desired instances automatically through a process known as typeclass resolution. In Lean, by changing structure to class in the example above, the type of Add.add becomes:

namespace Ex

class Add (α : Type) where
  add : α → α → α

@Add.add : {α : Type} → [self : Add α] → α → α → α#check @Add.add

@Add.add : {α : Type} → [self : Add α] → α → α → α

end Ex

where the square brackets indicate that the argument of type Add α is instance implicit, i.e. that it should be synthesized using typeclass resolution. This version of add is the Lean analogue of the Haskell term add :: Add a => a -> a -> a. Similarly, we can register instances by:

namespace Ex
class Add (α : Type) where
  add : α → α → α

instance : Add Nat where
  add := Nat.add

instance : Add Int where
  add := Int.add

instance : Add Float where
  add := Float.add

end Ex

Then for n : Nat and m : Nat, the term Add.add n m triggers typeclass resolution with the goal of Add Nat, and typeclass resolution will synthesize the instance for Nat above. We can now reimplement double using an instance implicit by:

namespace Ex
class Add (α : Type) where
  add : α → α → α
instance : Add Nat where
 add := Nat.add
instance : Add Int where
 add := Int.add
instance : Add Float where
 add := Float.add

def double [Add α] (x : α) : α :=
  Add.add x x

@double : {α : Type} → [Add α] → α → α#check @double

@double : {α : Type} → [Add α] → α → α

20#eval double 10

20#eval double (10 : Int)

14.000000#eval double (7 : Float)

14.000000

482.000000#eval double (239.0 + 2)

482.000000

end Ex

In general, instances may depend on other instances in complicated ways. For example, you can declare an instance stating that if α has addition, then Array α has addition:

instance [Add α] : Add (Array α) where
  add x y := Array.zipWith (· + ·) x y

#[4, 6]#eval Add.add #[1, 2] #[3, 4]

#[4, 6]

#[4, 6]#eval #[1, 2] + #[3, 4]

#[4, 6]

Note that (· + ·) is notation for fun x y => x + y in Lean.

The example above demonstrates how type classes are used to overload notation. Now, we explore another application. We often need an arbitrary element of a given type. Recall that types may not have any elements in Lean. It often happens that we would like a definition to return an arbitrary element in a “corner case.” For example, we may like the expression head xs to be of type α when xs is of type List α. Similarly, many theorems hold under the additional assumption that a type is not empty. For example, if α is a type, ∃ x : α, x = x is true only if α is not empty. The standard library defines a type class Inhabited to enable type class inference to infer a “default” element of an inhabited type. Let us start with the first step of the program above, declaring an appropriate class:

namespace Ex

class Inhabited (α : Type u) where
  default : α

@Inhabited.default : {α : Type u_1} → [self : Inhabited α] → α#check @Inhabited.default

@Inhabited.default : {α : Type u_1} → [self : Inhabited α] → α

end Ex

Note Inhabited.default doesn't have any explicit arguments.

An element of the class Inhabited α is simply an expression of the form Inhabited.mk x, for some element x : α. The projection Inhabited.default will allow us to “extract” such an element of α from an element of Inhabited α. Now we populate the class with some instances:

namespace Ex
class Inhabited (a : Type _) where
 default : a

instance : Inhabited Bool where
  default := true

instance : Inhabited Nat where
  default := 0

instance : Inhabited Unit where
  default := ()

instance : Inhabited Prop where
  default := True

0#eval (Inhabited.default : Nat)

true#eval (Inhabited.default : Bool)

true

end Ex

You can use the command export to create the alias default for Inhabited.default.

namespace Ex
class Inhabited (a : Type _) where
 default : a
instance : Inhabited Bool where
 default := true
instance : Inhabited Nat where
 default := 0
instance : Inhabited Unit where
 default := ()
instance : Inhabited Prop where
 default := True

export Inhabited (default)

0#eval (default : Nat)

true#eval (default : Bool)

true

end Ex

10.1. Chaining Instances🔗

If that were the extent of type class inference, it would not be all that impressive; it would be simply a mechanism of storing a list of instances for the elaborator to find in a lookup table. What makes type class inference powerful is that one can chain instances. That is, an instance declaration can in turn depend on an implicit instance of a type class. This causes class inference to chain through instances recursively, backtracking when necessary, in a Prolog-like search.

For example, the following definition shows that if two types α and β are inhabited, then so is their product:

instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
  default := (default, default)

With this added to the earlier instance declarations, type class instance can infer, for example, a default element of Nat × Bool:

namespace Ex
class Inhabited (α : Type u) where
 default : α
instance : Inhabited Bool where
 default := true
instance : Inhabited Nat where
 default := 0
opaque default [Inhabited α] : α :=
 Inhabited.default

instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
  default := (default, default)

(0, true)#eval (default : Nat × Bool)

(0, true)

end Ex

Similarly, we can inhabit type function with suitable constant functions:

instance [Inhabited β] : Inhabited (α → β) where
  default := fun _ => default

As an exercise, try defining default instances for other types, such as List and Sum types.

The Lean standard library contains the definition inferInstance. It has type {α : Sort u} → [i : α] → α, and is useful for triggering the type class resolution procedure when the expected type is an instance.

inferInstance : Inhabited Nat#check (inferInstance : Inhabited Nat)

inferInstance : Inhabited Nat

Definition `foo` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.def foo : Inhabited (Nat × Nat) :=
  inferInstance

theorem ex : foo.default = (default, default) :=
  rfl

You can use the command #print to inspect how simple inferInstance is.

@[reducible] def inferInstance.{u} : {α : Sort u} → [i : α] → α :=
fun {α} [i : α] => i#print inferInstance

@[reducible] def inferInstance.{u} : {α : Sort u} → [i : α] → α :=
fun {α} [i : α] => i

10.2. ToString🔗

The polymorphic method toString has type {α : Type u} → [ToString α] → α → String. You implement the instance for your own types and use chaining to convert complex values into strings. Lean comes with ToString instances for most builtin types.

structure Person where
  name : String
  age  : Nat

instance : ToString Person where
  toString p := p.name ++ "@" ++ toString p.age

"Leo@542"#eval toString { name := "Leo", age := 542 : Person }

"Leo@542"

"(Daniel@18, hello)"#eval toString ({ name := "Daniel", age := 18 : Person }, "hello")

"(Daniel@18, hello)"

10.3. Numerals🔗

Numerals are polymorphic in Lean. You can use a numeral (e.g., 2) to denote an element of any type that implements the type class OfNat.

structure Rational where
  num : Int
  den : Nat
  inv : den ≠ 0

instance : OfNat Rational n where
  ofNat := { num := n, den := 1, inv := byn:Nat⊢ 1 ≠ 0 decideAll goals completed! 🐙 }

instance : ToString Rational where
  toString r := s!"{r.num}/{r.den}"

2/1#eval (2 : Rational)

2/1

2 : Rational#check (2 : Rational)

2 : Rational

2 : Nat#check (2 : Nat)

2 : Nat

Lean elaborates the terms (2 : Nat) and (2 : Rational) as @OfNat.ofNat Nat 2 (@instOfNatNat 2) and @OfNat.ofNat Rational 2 (@instOfNatRational 2) respectively. We say the numerals 2 occurring in the elaborated terms are raw natural numbers. You can input the raw natural number 2 using the macro nat_lit 2.

2 : Nat#check nat_lit 2

2 : Nat

Raw natural numbers are not polymorphic.

The OfNat instance is parametric on the numeral. So, you can define instances for particular numerals. The second argument is often a variable as in the example above, or a raw natural number.

                class Monoid (α : Type u) where
  unit : α
  op   : α → α → α

instance [s : Monoid α] : OfNat α (nat_lit 1) where
  ofNat := s.unit

def getUnit [Monoid α] : α :=
  1

10.4. Output Parameters🔗

By default, Lean only tries to synthesize an instance Inhabited T when the term T is known and does not contain missing parts. The following command produces the error typeclass instance problem is stuck, it is often due to metavariables because the type has a missing part (i.e., the _).

/--
error: typeclass instance problem is stuck, it is often due to metavariables
  Inhabited (Nat × ?m.2)
-/
#guard_msgs (error) in
#eval (inferInstance : Inhabited (Nat × _))

You can view the parameter of the type class Inhabited as an input value for the type class synthesizer. When a type class has multiple parameters, you can mark some of them as output parameters. Lean will start type class synthesizer even when these parameters have missing parts. In the following example, we use output parameters to define a heterogeneous polymorphic multiplication.

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

export HMul (hMul)

instance : HMul Nat Nat Nat where
  hMul := Nat.mul

instance : HMul Nat (Array Nat) (Array Nat) where
  hMul a bs := bs.map (fun b => hMul a b)

12#eval hMul 4 3

#[8, 12, 16]#eval hMul 4 #[2, 3, 4]

#[8, 12, 16]

end Ex

The parameters α and β are considered input parameters and γ an output one. Given an application hMul a b, after the types of a and b are known, the type class synthesizer is invoked, and the resulting type is obtained from the output parameter γ. In the example above, we defined two instances. The first one is the homogeneous multiplication for natural numbers. The second is the scalar multiplication for arrays. Note that you chain instances and generalize the second instance.

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

export HMul (hMul)

instance : HMul Nat Nat Nat where
  hMul := Nat.mul

instance : HMul Int Int Int where
  hMul := Int.mul

instance [HMul α β γ] : HMul α (Array β) (Array γ) where
  hMul a bs := bs.map (fun b => hMul a b)

12#eval hMul 4 3

#[8, 12, 16]#eval hMul 4 #[2, 3, 4]

#[8, 12, 16]

#[-6, 2, -8]#eval hMul (-2) #[3, -1, 4]

#[-6, 2, -8]

#[#[4, 6], #[0, 8]]#eval hMul 2 #[#[2, 3], #[0, 4]]

#[#[4, 6], #[0, 8]]

end Ex

You can use our new scalar array multiplication instance on arrays of type Array β with a scalar of type α whenever you have an instance HMul α β γ. In the last #eval, note that the instance was used twice on an array of arrays.

Output parameters are ignored during instance synthesis. Even when instance synthesis occurs in a context in which the values of output parameters are already determined, their values are ignored. Once an instance is found using its input parameters, Lean ensures that the already-known values of the output parameters match those which were found.

Lean also features semi-output parameters, which have some features of input parameters and some features of output parameters. Like input parameters, semi-output parameters are considered when selecting instances. Like output parameters, they can be used to instantiate unknown values. However, they do not do so uniquely. Instance synthesis with semi-output parameters can be more difficult to predict, because the order in which instances are considered can determine which is selected, but it is also more flexible.

10.5. Default Instances🔗

In the class HMul, the parameters α and β are treated as input values. Thus, type class synthesis only starts after these two types are known. This may often be too restrictive.

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

export HMul (hMul)

instance : HMul Int Int Int where
  hMul := Int.mul

def xs : List Int := [1, 2, 3]

/--
error: typeclass instance problem is stuck
  HMul Int ?m.2 (?m.11 y)

Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `HMul` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs (error) in
#eval fun y => xs.map (fun x => hMul x y)

end Ex

The instance HMul is not synthesized by Lean because the type of y has not been provided. However, it is natural to assume that the type of y and x should be the same in this kind of situation. We can achieve exactly that using default instances.

namespace Ex

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

export HMul (hMul)

@[default_instance]
instance : HMul Int Int Int where
  hMul := Int.mul

def xs : List Int := [1, 2, 3]

fun y => List.map (fun x => hMul x y) xs : Int → List Int#check fun y => xs.map (fun x => hMul x y)

fun y => List.map (fun x => hMul x y) xs : Int → List Int

end Ex

By tagging the instance above with the attribute [default_instance], we are instructing Lean to use this instance on pending type class synthesis problems. The actual Lean implementation defines homogeneous and heterogeneous classes for arithmetical operators. Moreover, a + b, a * b, a - b, a / b, and a % b are notations for the heterogeneous versions. The instance OfNat Nat n is the default instance (with priority 100) for the OfNat class. This is why the numeral 2 has type Nat when the expected type is not known. You can define default instances with higher priority to override the builtin ones.

structure Rational where
  num : Int
  den : Nat
  inv : den ≠ 0

@[default_instance 200]
instance : OfNat Rational n where
  ofNat := { num := n, den := 1, inv := byn:Nat⊢ 1 ≠ 0 decideAll goals completed! 🐙 }

instance : ToString Rational where
  toString r := s!"{r.num}/{r.den}"

2 : Rational#check 2

2 : Rational

Priorities are also useful to control the interaction between different default instances. For example, suppose xs has type List α. When elaborating xs.map (fun x => 2 * x), we want the homogeneous instance for multiplication to have higher priority than the default instance for OfNat α 2. This is particularly important when we have implemented only the instance HMul α α α, and did not implement HMul Nat α α. Now, we reveal how the notation a * b is defined in Lean.

namespace Ex

class OfNat (α : Type u) (n : Nat) where
  ofNat : α

@[default_instance]
instance (n : Nat) : OfNat Nat n where
  ofNat := n

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

class Mul (α : Type u) where
  mul : α → α → α

@[default_instance 10]
instance [Mul α] : HMul α α α where
  hMul a b := Mul.mul a b

infixl:70 " * " => HMul.hMul

end Ex

The Mul class is convenient for types that only implement the homogeneous multiplication.

10.6. Local Instances🔗

Type classes are implemented using attributes in Lean. Thus, you can use the local modifier to indicate that they only have effect until the current section or namespace is closed, or until the end of the current file.

                structure Point where
  x : Nat
  y : Nat

section

local instance : Add Point where
  add a b := { x := a.x + b.x, y := a.y + b.y }

def double (p : Point) :=
  p + p

end -- instance `Add Point` is not active anymore

/--
error: failed to synthesize instance of type class
  HAdd Point Point ?m.5

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
def triple (p : Point) :=
  p + p + p

You can also temporarily disable an instance using the attribute command until the current section or namespace is closed, or until the end of the current file.

                structure Point where
  x : Nat
  y : Nat

instance addPoint : Add Point where
  add a b := { x := a.x + b.x, y := a.y + b.y }

def double (p : Point) :=
  p + p

attribute [-instance] addPoint

/--
error: failed to synthesize instance of type class
  HAdd Point Point ?m.5

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
def triple (p : Point) :=
  p + p + p  -- Error: failed to synthesize instance

We recommend you only use this command to diagnose problems.

10.7. Scoped Instances🔗

You can also declare scoped instances in namespaces. This kind of instance is only active when you are inside of the namespace or open the namespace.

structure Point where
  x : Nat
  y : Nat

namespace Point

scoped instance : Add Point where
  add a b := { x := a.x + b.x, y := a.y + b.y }

def double (p : Point) :=
  p + p

end Point

-- instance `Add Point` is not active anymore

/--
error: failed to synthesize instance of type class
  HAdd Point Point ?m.3

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs (error) in
fun p => sorry : (p : Point) → ?m.6 p#check fun (p : Point) => p + p + p

fun p => sorry : (p : Point) → ?m.6 p

namespace Point

-- instance `Add Point` is active again
fun p => p + p + p : Point → Point#check fun (p : Point) => p + p + p

fun p => p + p + p : Point → Point

end Point

open Point -- activates instance `Add Point`

fun p => p + p + p : Point → Point#check fun (p : Point) => p + p + p

fun p => p + p + p : Point → Point

You can use the command open scoped <namespace> to activate scoped attributes but will not “open” the names from the namespace.

structure Point where
  x : Nat
  y : Nat

namespace Point

scoped instance : Add Point where
  add a b := { x := a.x + b.x, y := a.y + b.y }

def double (p : Point) :=
  p + p

end Point

open scoped Point -- activates instance `Add Point`

fun p => p + p + p : Point → Point#check fun (p : Point) => p + p + p

fun p => p + p + p : Point → Point

/--
error: Unknown identifier `double`
-/
#guard_msgs (error) in
fun p => sorry : (p : Point) → ?m.2 p#check fun (p : Point) => double p

fun p => sorry : (p : Point) → ?m.2 p

10.8. Decidable Propositions🔗

Let us consider another example of a type class defined in the standard library, namely the type class of Decidable propositions. Roughly speaking, an element of Prop is said to be decidable if we can decide whether it is true or false. The distinction is only useful in constructive mathematics; classically, every proposition is decidable. But if we use the classical principle, say, to define a function by cases, that function will not be computable. Algorithmically speaking, the Decidable type class can be used to infer a procedure that effectively determines whether or not the proposition is true. As a result, the type class supports such computational definitions when they are possible while at the same time allowing a smooth transition to the use of classical definitions and classical reasoning.

In the standard library, Decidable is defined formally as follows:

namespace Hidden

class inductive Decidable (p : Prop) where
  | isFalse (h : ¬p) : Decidable p
  | isTrue  (h : p)  : Decidable p

end Hidden

Logically speaking, having an element t : Decidable p is stronger than having an element t' : p ∨ ¬p; it enables us to define values of an arbitrary type depending on the truth value of p. For example, for the expression if p then a else b to make sense, we need to know that p is decidable. That expression is syntactic sugar for ite p a b, where ite is defined as follows:

namespace Hidden

def ite {α : Sort u}
    (c : Prop) [h : Decidable c]
    (t e : α) : α :=
  h.casesOn (motive := fun _ => α) (fun _ => e) (fun _ => t)

end Hidden

The standard library also contains a variant of ite called dite, the dependent if-then-else expression. It is defined as follows:

namespace Hidden

def dite {α : Sort u}
    (c : Prop) [h : Decidable c]
    (t : c → α) (e : Not c → α) : α :=
  Decidable.casesOn (motive := fun _ => α) h e t

end Hidden

That is, in dite c t e, we can assume hc : c in the “then” branch, and hnc : ¬c in the “else” branch. To make dite more convenient to use, Lean allows us to write if h : c then t else e instead of dite c (fun h : c => t h) (fun h : ¬c => e h).

Without classical logic, we cannot prove that every proposition is decidable. But we can prove that certain propositions are decidable. For example, we can prove the decidability of basic operations like equality and comparisons on the natural numbers and the integers. Moreover, decidability is preserved under propositional connectives:

@instDecidableAnd : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)#check @instDecidableAnd

@instDecidableAnd : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)

@instDecidableOr : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)#check @instDecidableOr

@instDecidableOr : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)

@instDecidableNot : {p : Prop} → [dp : Decidable p] → Decidable ¬p#check @instDecidableNot

@instDecidableNot : {p : Prop} → [dp : Decidable p] → Decidable ¬p

Thus we can carry out definitions by cases on decidable predicates on the natural numbers:

def step (a b x : Nat) : Nat :=
  if x < a ∨ x > b then 0 else 1

set_option pp.explicit true

def step : Nat → Nat → Nat → Nat :=
fun a b x =>
  @ite Nat (Or (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b))
    (@instDecidableOr (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b) (Nat.decLt x a) (Nat.decLt b x))
    (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))#print step

def step : Nat → Nat → Nat → Nat :=
fun a b x =>
  @ite Nat (Or (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b))
    (@instDecidableOr (@LT.lt Nat instLTNat x a) (@GT.gt Nat instLTNat x b) (Nat.decLt x a) (Nat.decLt b x))
    (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))

Turning on implicit arguments shows that the elaborator has inferred the decidability of the proposition x < a ∨ x > b, simply by applying appropriate instances.

With the classical axioms, we can prove that every proposition is decidable. You can import the classical axioms and make the generic instance of decidability available by opening the Classical namespace.

open Classical

Thereafter Decidable p has an instance for every p. Thus all theorems in the library that rely on decidability assumptions are freely available when you want to reason classically. In Axioms and Computation, we will see that using the law of the excluded middle to define functions can prevent them from being used computationally. Thus, the standard library assigns a low priority to the propDecidable instance.

namespace Hidden

open Classical

noncomputable scoped
instance (priority := low) propDecidable (a : Prop) : Decidable a :=
  choice <| match em a with
    | Or.inl h => ⟨isTrue h⟩
    | Or.inr h => ⟨isFalse h⟩

end Hidden

This guarantees that Lean will favor other instances and fall back on propDecidable only after other attempts to infer decidability have failed.

The Decidable type class also provides a bit of small-scale automation for proving theorems. The standard library introduces the tactic decide that uses the Decidable instance to solve simple goals, as well as a function decide that uses a Decidable instance to compute the corresponding Bool.

example : 10 < 5 ∨ 1 > 0 := by⊢ 10 < 5 ∨ 1 > 0
  decideAll goals completed! 🐙

example : ¬(True ∧ False) := by⊢ ¬(True ∧ False)
  decideAll goals completed! 🐙

example : 10 * 20 = 200 := by⊢ 10 * 20 = 200
  decideAll goals completed! 🐙

theorem ex : True ∧ 2 = 1 + 1 := by⊢ True ∧ 2 = 1 + 1
  decideAll goals completed! 🐙

theorem ex : True ∧ 2 = 1 + 1 :=
of_decide_eq_true (id (Eq.refl true))#print ex

theorem ex : True ∧ 2 = 1 + 1 :=
of_decide_eq_true (id (Eq.refl true))

@of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p#check @of_decide_eq_true

@of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p

decide : (p : Prop) → [h : Decidable p] → Bool#check @decide

decide : (p : Prop) → [h : Decidable p] → Bool

They work as follows. The expression decide p tries to infer a decision procedure for p, and, if it is successful, evaluates to either true or false. In particular, if p is a true closed expression, decide p will reduce definitionally to the Boolean true. On the assumption that decide p = true holds, of_decide_eq_true produces a proof of p. The tactic decide puts it all together to prove a target p. By the previous observations, decide will succeed any time the inferred decision procedure for p has enough information to evaluate, definitionally, to the isTrue case.

10.9. Managing Type Class Inference🔗

If you are ever in a situation where you need to supply an expression that Lean can infer by type class inference, you can ask Lean to carry out the inference using inferInstance:

Definition `foo` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.def foo : Add Nat := inferInstance

Definition `bar` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.def bar : Inhabited (Nat → Nat) := inferInstance

@inferInstance : {α : Sort u_1} → [i : α] → α#check @inferInstance

@inferInstance : {α : Sort u_1} → [i : α] → α

In fact, you can use Lean's (t : T) notation to specify the class whose instance you are looking for, in a concise manner:

inferInstance : Add Nat#check (inferInstance : Add Nat)

inferInstance : Add Nat

Sometimes Lean can't find an instance because the class is buried under a definition. For example, Lean cannot find an instance of Inhabited (Set α). We can declare one explicitly:

                def Set (α : Type u) := α → Prop

/--
error: failed to synthesize instance of type class
  Inhabited (Set α)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example : Inhabited (Set α) :=
  inferInstance

instance : Inhabited (Set α) :=
  inferInstanceAs (Inhabited (α → Prop))

At times, you may find that the type class inference fails to find an expected instance, or, worse, falls into an infinite loop and times out. To help debug in these situations, Lean enables you to request a trace of the search:

set_option trace.Meta.synthInstance true

If you are using VS Code, you can read the results by hovering over the relevant theorem or definition, or opening the messages window with CtrlShiftEnter.

You can also limit the search using the following options:

                set_option synthInstance.maxHeartbeats 10000
set_option synthInstance.maxSize 400

Option synthInstance.maxHeartbeats specifies the maximum amount of heartbeats per typeclass resolution problem. A heartbeat is the number of (small) memory allocations (in thousands), 0 means there is no limit. Option synthInstance.maxSize is the maximum number of instances used to construct a solution in the type class instance synthesis procedure.

Remember also that in both the VS Code and Emacs editor modes, tab completion works in set_option, to help you find suitable options.

As noted above, the type class instances in a given context represent a Prolog-like program, which gives rise to a backtracking search. Both the efficiency of the program and the solutions that are found can depend on the order in which the system tries the instance. Instances which are declared last are tried first. Moreover, if instances are declared in other modules, the order in which they are tried depends on the order in which namespaces are opened. Instances declared in namespaces which are opened later are tried earlier.

You can change the order that type class instances are tried by assigning them a priority. When an instance is declared, it is assigned a default priority value. You can assign other priorities when defining an instance. The following example illustrates how this is done:

                class Foo where
  a : Nat
  b : Nat

instance (priority := default + 1) i1 : Foo where
  a := 1
  b := 1

instance i2 : Foo where
  a := 2
  b := 2

example : Foo.a = 1 :=
  rfl

instance (priority := default + 2) i3 : Foo where
  a := 3
  b := 3

example : Foo.a = 3 :=
  rfl

10.10. Coercions using Type Classes🔗

The most basic type of coercion maps elements of one type to another. For example, a coercion from Nat to Int allows us to view any element n : Nat as an element of Int. But some coercions depend on parameters; for example, for any type α, we can view any element as : List α as an element of Set α, namely, the set of elements occurring in the list. The corresponding coercion is defined on the “family” of types List α, parameterized by α.

Lean allows us to declare three kinds of coercions:

from a family of types to another family of types
from a family of types to the class of sorts
from a family of types to the class of function types

The first kind of coercion allows us to view any element of a member of the source family as an element of a corresponding member of the target family. The second kind of coercion allows us to view any element of a member of the source family as a type. The third kind of coercion allows us to view any element of the source family as a function. Let us consider each of these in turn.

In Lean, coercions are implemented on top of the type class resolution framework. We define a coercion from α to β by declaring an instance of Coe α β. For example, we can define a coercion from Bool to Prop as follows:

instance : Coe Bool Prop where
  coe b := b = true

This enables us to use boolean terms in if-then-else expressions:

5#eval if true then 5 else 3

3#eval if false then 5 else 3

We can define a coercion from List α to Set α as follows:

def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union

def List.toSet : List α → Set α
  | []    => Set.empty
  | a::as => {a} ∪ as.toSet

instance : Coe (List α) (Set α) where
  coe a := a.toSet

def s : Set Nat := {1}

s ∪ [2, 3].toSet : Set Nat#check s ∪ [2, 3]

s ∪ [2, 3].toSet : Set Nat

We can use the notation ↑ to force a coercion to be introduced in a particular place. It is also helpful to make our intent clear, and work around limitations of the coercion resolution system.

def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
  | []    => Set.empty
  | a::as => {a} ∪ as.toSet
instance : Coe (List α) (Set α) where
  coe a := a.toSet

def s : Set Nat := {1}

let x := [2, 3].toSet;
s ∪ x : Set Nat#check let x := ↑[2, 3]; s ∪ x

let x := [2, 3].toSet;
s ∪ x : Set Nat

let x := [2, 3];
s ∪ x.toSet : Set Nat#check let x := [2, 3]; s ∪ x

let x := [2, 3];
s ∪ x.toSet : Set Nat

Lean also supports dependent coercions using the type class CoeDep. For example, we cannot coerce arbitrary propositions to Bool, only the ones that implement the Decidable typeclass.

instance (p : Prop) [Decidable p] : CoeDep Prop p Bool where
  coe := decide p

Lean will also chain (non-dependent) coercions as necessary. Actually, the type class CoeT is the transitive closure of Coe.

Let us now consider the second kind of coercion. By the class of sorts, we mean the collection of universes Type u. A coercion of the second kind is of the form:

    c : (x1 : A1) → ... → (xn : An) → F x1 ... xn → Type u

where F is a family of types as above. This allows us to write s : t whenever t is of type F a₁ ... aₙ. In other words, the coercion allows us to view the elements of F a₁ ... aₙ as types. This is very useful when defining algebraic structures in which one component, the carrier of the structure, is a Type. For example, we can define a semigroup as follows:

                structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)

instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b

In other words, a semigroup consists of a type, carrier, and a multiplication, mul, with the property that the multiplication is associative. The instance command allows us to write a * b instead of Semigroup.mul S a b whenever we have a b : S.carrier; notice that Lean can infer the argument S from the types of a and b. The function Semigroup.carrier maps the class Semigroup to the sort Type u:

structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b

Semigroup.carrier.{u} (self : Semigroup) : Type u#check Semigroup.carrier

Semigroup.carrier.{u} (self : Semigroup) : Type u

If we declare this function to be a coercion, then whenever we have a semigroup S : Semigroup, we can write a : S instead of a : S.carrier:

structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b

instance : CoeSort Semigroup (Type u) where
  coe s := s.carrier

example (S : Semigroup) (a b c : S) : (a * b) * c = a * (b * c) :=
  Semigroup.mul_assoc _ a b c

It is the coercion that makes it possible to write (a b c : S). Note that, we define an instance of CoeSort Semigroup (Type u) instead of Coe Semigroup (Type u).

By the class of function types, we mean the collection of Pi types (z : B) → C. The third kind of coercion has the form:

    c : (x₁ : A₁) → ... → (xₙ : Aₙ) → (y : F x₁ ... xₙ) → (z : B) → C

where F is again a family of types and B and C can depend on x₁, ..., xₙ, y. This makes it possible to write t s whenever t is an element of F a₁ ... aₙ. In other words, the coercion enables us to view elements of F a₁ ... aₙ as functions. Continuing the example above, we can define the notion of a morphism between semigroups S1 and S2. That is, a function from the carrier of S1 to the carrier of S2 (note the implicit coercion) that respects the multiplication. The projection Morphism.mor takes a morphism to the underlying function:

structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
  coe s := s.carrier

structure Morphism (S1 S2 : Semigroup) where
  mor : S1 → S2
  resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)

@Morphism.mor : {S1 : Semigroup} → {S2 : Semigroup} → Morphism S1 S2 → S1.carrier → S2.carrier#check @Morphism.mor

@Morphism.mor : {S1 : Semigroup} → {S2 : Semigroup} → Morphism S1 S2 → S1.carrier → S2.carrier

As a result, it is a prime candidate for the third type of coercion.

structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
  coe s := s.carrier
structure Morphism (S1 S2 : Semigroup) where
  mor : S1 → S2
  resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)

instance (S1 S2 : Semigroup) :
    CoeFun (Morphism S1 S2) (fun _ => S1 → S2) where
  coe m := m.mor

theorem resp_mul {S1 S2 : Semigroup} (f : Morphism S1 S2) (a b : S1)
        : f (a * b) = f a * f b :=
  f.resp_mul a b

example (S1 S2 : Semigroup) (f : Morphism S1 S2) (a : S1) :
      f (a * a * a) = f a * f a * f a :=
  calc f (a * a * a)
    _ = f (a * a) * f a := byS1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a * a) = f.mor (a * a) * f.mor a rw [resp_mul fS1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a) * f.mor a = f.mor (a * a) * f.mor a]All goals completed! 🐙
    _ = f a * f a * f a := byS1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a) * f.mor a = f.mor a * f.mor a * f.mor a rw [resp_mul fS1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor a * f.mor a * f.mor a = f.mor a * f.mor a * f.mor a]All goals completed! 🐙

With the coercion in place, we can write f (a * a * a) instead of f.mor (a * a * a). When the Morphism, f, is used where a function is expected, Lean inserts the coercion. Similar to CoeSort, we have yet another class CoeFun for this class of coercions. The parameter γ is used to specify the function type we are coercing to. This type may depend on the type we are coercing from.