Coercions

Sometimes you have a term of a type, and you really want it to have another type (because that’s what we do in maths; we are liberal with our types, unlike Lean). For example you might have a natural number n : ℕ but a function f : ℝ → ℝ (like Real.sqrt or similar), and you want to consider f n. This is problematic in a strongly typed language like Lean: n has type Nat and not Real, so f n does not make sense. However, if you try it…

import Mathlib.Tactic

def a : ℕ := 37

#check Real.sqrt a -- real.sqrt ↑a : ℝ

…it works anyway! But actually looking more closely, something funny is going on; what is that ↑ by the a? That up-arrow is Lean’s notation for the completely obvious function from ℕ to ℝ which doesn’t have a name in mathematics but which Lean needs to apply in order for everything to typecheck.

Coercion to function

Here’s another example of something which shouldn’t work but which does:

import Mathlib.Tactic

variable (G H : Type) [Group G] [Group H] (φ : G →* H) (g : G)

#check φ g -- ↑φ g : H

Here φ is a group homomorphism, so in particular it is not a function, it is a pair consisting of a function and a proof that the function preserves multiplication. But we treat it as a function and it works anyway, because there is a coercion from the type G →* H to the type G → H, indicated by an arrow.

Coercion to type

A subset of the reals is a term, not a type. The type is Set ℝ of all subsets of the reals, so here s : Set ℝ is a term, not a type, and so a : s shouldn’t even make sense. But if you look carefully, you see that the type of a is in fact ↑s, because s has been coerced from a term to the corresponding subtype {x : ℝ // x ∈ s}.

import Mathlib.Tactic

example (s : Set ℝ) (a : s) : a = a := by
  /-
  s : Set ℝ
  a : ↑s
  ⊢ a = a
  -/
  rfl

A term of the subtype {x : ℝ // x ∈ s} is a pair consisting of a term x : ℝ and a proof that x ∈ s.