Coercions and lifts #

The elaborator tries to insert coercions automatically. Only instances of has_coe type class are considered in the process.

Lean also provides a "lifting" operator: ↑a. It uses all instances of has_lift type class. Every has_coe instance is also a has_lift instance.

We recommend users only use has_coe for coercions that do not produce a lot of ambiguity.

All coercions and lifts can be identified with the constant coe.

We use the has_coe_to_fun type class for encoding coercions from a type to a function space.

We use the has_coe_to_sort type class for encoding coercions from a type to a sort.

source

@[class]

structure has_lift (a : Sort u) (b : Sort v) :

Sort (max 1 (imax u v))

lift : a → b

Can perform a lifting operation ↑a.

Instances

source

@[class]

structure has_lift_t (a : Sort u) (b : Sort v) :

Sort (max 1 (imax u v))

lift : a → b

Auxiliary class that contains the transitive closure of has_lift.

Instances

We specify the universes in has_coe, has_coe_to_fun, and has_coe_to_sort explicitly in order to match exactly what appears in Lean4.

source

@[class]

structure has_coe (a : Sort u) (b : Sort v) :

Sort (max (max 1 u) v)

coe : a → b

Instances

source

@[class]

structure has_coe_t (a : Sort u) (b : Sort v) :

Sort (max 1 (imax u v))

coe : a → b

Auxiliary class that contains the transitive closure of has_coe.

Instances

source

@[class]

structure has_coe_to_fun (a : Sort u) (F : out_param (a → Sort v)) :

Sort (max (max 1 u) v)

coe : Π (x : a), F x

Instances

source

@[class]

structure has_coe_to_sort (a : Sort u) (S : out_param (Sort v)) :

Sort (max (max 1 u) v)

coe : a → S

Instances

source

def lift {a : Sort u} {b : Sort v} [has_lift a b] :

a → b

Equations

lift = has_lift.lift

source

def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] :

a → b

Equations

lift_t = has_lift_t.lift

source

def coe_b {a : Sort u} {b : Sort v} [has_coe a b] :

a → b

Equations

coe_b = has_coe.coe

source

def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] :

a → b

Equations

coe_t = has_coe_t.coe

source

def coe_fn_b {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] (x : a) :

b x

Equations

coe_fn_b = has_coe_to_fun.coe

User level coercion operators #

source

def coe {a : Sort u} {b : Sort v} [has_lift_t a b] :

a → b

Equations

coe = lift_t

source

def coe_fn {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] (x : a) :

b x

Equations

coe_fn = has_coe_to_fun.coe

source

def coe_sort {a : Sort u} {b : Sort v} [has_coe_to_sort a b] :

a → b

Equations

coe_sort = has_coe_to_sort.coe

Notation #

Transitive closure for `has_lift`, `has_coe`, `has_coe_to_fun` #

source

@[protected, instance]

def lift_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_lift_t b c] [has_lift a b] :

has_lift_t a c

Equations

lift_trans = {lift := λ (x : a), lift_t (lift x)}

source

@[protected, instance]

def lift_base {a : Sort u} {b : Sort v} [has_lift a b] :

has_lift_t a b

Equations

lift_base = {lift := lift _inst_1}

source

@[protected, instance]

def coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t b c] [has_coe a b] :

has_coe_t a c

Equations

coe_trans = {coe := λ (x : a), coe_t (coe_b x)}

source

@[protected, instance]

def coe_base {a : Sort u} {b : Sort v} [has_coe a b] :

has_coe_t a b

Equations

coe_base = {coe := coe_b _inst_1}

source

@[protected, instance]

def coe_option {a : Type u} :

has_coe_t a (option a)

We add this instance directly into has_coe_t to avoid non-termination.

Suppose coe_option had type (has_coe a (option a)). Then, we can loop when searching a coercion from α to β (has_coe_t α β) 1- coe_trans at (has_coe_t α β) (has_coe α ?b₁) and (has_coe_t ?b₁ c) 2- coe_option at (has_coe α ?b₁) ?b₁ := option α 3- coe_trans at (has_coe_t (option α) β) (has_coe (option α) ?b₂) and (has_coe_t ?b₂ β) 4- coe_option at (has_coe (option α) ?b₂) ?b₂ := option (option α)) ...

Equations

coe_option = {coe := λ (x : a), some x}

source

@[class]

structure has_coe_t_aux (a : Sort u) (b : Sort v) :

Sort (max 1 (imax u v))

coe : a → b

Auxiliary transitive closure for has_coe which does not contain instances such as coe_option.

They would produce non-termination when combined with coe_fn_trans and coe_sort_trans.

Instances

source

@[protected, instance]

def coe_trans_aux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t_aux b c] [has_coe a b] :

has_coe_t_aux a c

Equations

coe_trans_aux = {coe := λ (x : a), has_coe_t_aux.coe (coe_b x)}

source

@[protected, instance]

def coe_base_aux {a : Sort u} {b : Sort v} [has_coe a b] :

has_coe_t_aux a b

Equations

coe_base_aux = {coe := coe_b _inst_1}

source

@[protected, instance]

def coe_fn_trans {a : Sort u₁} {b : Sort u₂} {c : b → Sort v} [has_coe_to_fun b c] [has_coe_t_aux a b] :

has_coe_to_fun a (λ (x : a), c (has_coe_t_aux.coe x))

Equations

coe_fn_trans = {coe := λ (x : a), ⇑(has_coe_t_aux.coe x)}

source

@[protected, instance]

def coe_sort_trans {a : Sort u₁} {b : Sort u₂} {c : Sort v} [has_coe_to_sort b c] [has_coe_t_aux a b] :

has_coe_to_sort a c

Equations

coe_sort_trans = {coe := λ (x : a), ↥(has_coe_t_aux.coe x)}

source

@[protected, instance]

def coe_to_lift {a : Sort u} {b : Sort v} [has_coe_t a b] :

has_lift_t a b

Every coercion is also a lift

Equations

coe_to_lift = {lift := coe_t _inst_1}

Basic coercions #

source

@[protected, instance]

def coe_bool_to_Prop :

has_coe bool Prop

Equations

coe_bool_to_Prop = {coe := λ (y : bool), y = tt}

source

@[protected, instance]

def coe_sort_bool :

has_coe_to_sort bool Prop

Tactics such as the simplifier only unfold reducible constants when checking whether two terms are definitionally equal or a term is a proposition. The motivation is performance. In particular, when simplifying p -> q, the tactic simp only visits p if it can establish that it is a proposition. Thus, we mark the following instance as @[reducible], otherwise simp will not visit ↑p when simplifying ↑p -> q.

Equations