mathlib3 documentation

core / init.coe

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 of this typeclass
Instances of other typeclasses for has_lift
  • has_lift.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for has_lift_t
  • has_lift_t.has_sizeof_inst

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 of this typeclass
Instances of other typeclasses for has_coe
  • has_coe.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for has_coe_t
  • has_coe_t.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for has_coe_to_fun
  • has_coe_to_fun.has_sizeof_inst
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 of this typeclass
Instances of other typeclasses for has_coe_to_sort
  • has_coe_to_sort.has_sizeof_inst
source
def lift {a : Sort u} {b : Sort v} [has_lift a b] :
a → b
Equations
source
def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] :
a → b
Equations
Instances for lift_t
Instances for ↥lift_t
source
def coe_b {a : Sort u} {b : Sort v} [has_coe a b] :
a → b
Equations
source
def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] :
a → b
Equations
source
def coe_fn_b {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] (x : a) :
b x
Equations

User level coercion operators #

source
@[reducible]
def coe {a : Sort u} {b : Sort v} [has_lift_t a b] :
a → b
Equations
source
@[reducible]
def coe_fn {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] (x : a) :
b x
Equations
source
@[reducible]
def coe_sort {a : Sort u} {b : Sort v} [has_coe_to_sort a b] :
a → b
Equations

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
source
@[protected, instance]
def lift_base {a : Sort u} {b : Sort v} [has_lift a b] :
has_lift_t a b
Equations
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
source
@[protected, instance]
def coe_base {a : Sort u} {b : Sort v} [has_coe a b] :
has_coe_t a b
Equations
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
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 of this typeclass
Instances of other typeclasses for has_coe_t_aux
  • has_coe_t_aux.has_sizeof_inst
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
source
@[protected, instance]
def coe_base_aux {a : Sort u} {b : Sort v} [has_coe a b] :
has_coe_t_aux a b
Equations
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
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
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

Basic coercions #

source
@[protected, instance]
def coe_bool_to_Prop  :
has_coe bool Prop
Equations
source
@[protected, instance, reducible]
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
source
@[protected, instance]
def coe_decidable_eq (x : bool) :
decidable ↑x
Equations
source
@[protected, instance]
def coe_subtype {a : Sort u} {p : a → Prop} :
has_coe {x // p x} a
Equations

Basic lifts #

source
@[protected, instance]
def lift_fn {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] :
has_lift (a₁ → b₁) (a₂ → b₂)

Remark: we can't use [has_lift_t a₂ a₁] since it will produce non-termination whenever a type class resolution problem does not have a solution.

Equations
source
@[protected, instance]
def lift_fn_range {a : Sort ua} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [has_lift_t b₁ b₂] :
has_lift (a → b₁) (a → b₂)
Equations
source
@[protected, instance]
def lift_pi_range {α : Sort u} {A : α → Sort ua} {B : α → Sort ub} [Π (i : α), has_lift_t (A i) (B i)] :
has_lift (Π (i : α), A i) (Π (i : α), B i)

A dependent version of lift_fn_range.

Equations
source
@[protected, instance]
def lift_fn_dom {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b : Sort ub} [has_lift a₂ a₁] :
has_lift (a₁ → b) (a₂ → b)
Equations
source
@[protected, instance]
def lift_pair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t a₁ a₂] [has_lift_t b₁ b₂] :
has_lift (a₁ × b₁) (a₂ × b₂)
Equations
source
@[protected, instance]
def lift_pair₁ {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [has_lift_t a₁ a₂] :
has_lift (a₁ × b) (a₂ × b)
Equations
source
@[protected, instance]
def lift_pair₂ {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t b₁ b₂] :
has_lift (a × b₁) (a × b₂)
Equations
source
@[protected, instance]
def lift_list {a : Type u} {b : Type v} [has_lift a b] :
has_lift (list a) (list b)
Equations