coe and lift

Stream: new members

[Alex Zhang]

I saw the following code:

/-- Can perform a lifting operation `↑a`. -/
class has_lift (a : Sort u) (b : Sort v) :=
(lift : a → b)

/-- Auxiliary class that contains the transitive closure of has_lift. -/
class has_lift_t (a : Sort u) (b : Sort v) :=
(lift : a → b)

class has_coe (a : Sort u) (b : Sort v) :=
(coe : a → b)

/-- Auxiliary class that contains the transitive closure of has_coe. -/
class has_coe_t (a : Sort u) (b : Sort v) :=
(coe : a → b)

[Alex Zhang]

What are the differences between coe and lift?

[Alex Zhang]

If I am declaring an instance about coercion
instance my_instance: ... A B:=, should I use has_coe or has_coe_t for ...?

[Kevin Buzzard]

You're looking at the implementation details of how coercions actually work. There are more details in #tpil but as an end user I have never had to worry about these. Note that all those definitions are "the same", but the classes are used in different ways.

[Alex Zhang]

Hi, Kevin! How about the second question, for an end user?

[Kevin Buzzard]

If you're defining a coercion you should use has_coe, and then start worrying about these things if something doesn't work. The little up arrow is has_coe.coe . (actually it's just coe)

[Eric Wieser]

Often #lint will tell you if you are using has_coe but should be using has_coe_t

[Alex Zhang]

import tactic

universe u
variables α β : Type u
variable f : α → ℕ

variable h :α = β
include h

instance β_to_α: has_coe β α := ⟨λ b,by rw h; exact b⟩
lemma aux: (β → ℕ)=(α → ℕ):= by {rw h}
instance fun_to_fun : has_coe (α → ℕ) (β → ℕ) :=
⟨λ f, by rw aux;assumption⟩

theorem want (b : β): (f: (β → ℕ)) b = f ↑b := sorry

The statement of the theorem reports an error:maximum class-instance resolution depth has been reached.
Is it possible to somehow fix it?

[Alex Zhang]

The same error occurs if I change fun_to_fun to

instance fun_to_fun : has_coe (α → ℕ) (β → ℕ) :=
⟨λ f x, f (↑x:α)⟩

[Kevin Buzzard]

The coercion will never trigger because the type class inference system handles coercions and the type class inference system will not be able to find a proof that alpha = beta because = is not a typeclass.

[Alex Zhang]

Is there a minor fix that makes the code works (I am just exploring things in Lean)?