Zulip Chat Archive

Stream: general

Topic: Coercion


view this post on Zulip Ned Summers (Jul 23 2018 at 11:15):

For context, in Scott Morrison's category theory code he introduces isomorphism as the structure:

structure Isomorphism {C : Type u} [category.{u v} C] (X Y : C) :=
  (morphism : X ⟶ Y)
  (inverse : Y ⟶ X)
  (witness_1 : morphism ≫ inverse = 𝟙 X . obviously)
  (witness_2 : inverse ≫ morphism = 𝟙 Y . obviously)

This seems like a perfectly fine way of doing this. Later in the document he uses

instance Isomorphism_coercion_to_morphism : has_coe (Isomorphism.{u v} X Y) (X ⟶ Y) :=
{ coe := Isomorphism.morphism }

I can't seem to figure out what a coercion actually is, or what it's use is. It seems like it might be useful. I'm currently trying to state and prove a theorem where a morphism is shown to be an isomorphism and this looks like a promising way of moving from isomorphic objects to isomorphisms. Help much appreciated.

view this post on Zulip Patrick Massot (Jul 23 2018 at 11:45):

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes

view this post on Zulip Ned Summers (Jul 23 2018 at 11:54):

Thanks

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:56):

A coercion is just a way of moving from one type to another by applying a function which you don't want to continually mention, you just want Lean to do it automatically. See that the coercion is defined using instance not definition? That means "define it, and let the type class inference system use it". The type class inference system will then apply it whenever necessary.

view this post on Zulip Chris Hughes (Jul 23 2018 at 19:58):

Shouldn't that be a has_coe_to_fun not a has_coe?

view this post on Zulip Mario Carneiro (Jul 23 2018 at 23:56):

No, because the target isn't a function type (that arrow is not a regular arrow)

view this post on Zulip Anthony Bordg (Oct 05 2018 at 11:07):

Hi,
in the current library is there already a coercion to see a field as a comm_semiring ?
One can combine field.to_comm_ring with comm_ring.to_comm_semiring, but maybe there is a more direct way.
Thanks

view this post on Zulip Johan Commelin (Oct 05 2018 at 11:09):

The typeclass system should do that for you. Usually you don't need to touch it.

view this post on Zulip Johan Commelin (Oct 05 2018 at 11:10):

If you really need it:

instance {K : Type*} [field K] : comm_semiring K := by apply_instance

view this post on Zulip Johan Commelin (Oct 05 2018 at 11:10):

You can usually also insert the by apply_instance into your proofs if you need it.

view this post on Zulip Anthony Bordg (Oct 05 2018 at 11:28):

The typeclass system should do that for you. Usually you don't need to touch it.

The typeclass system doesn't help here, but the code you gave me with "instance" works fine.
Thank you @Johan Commelin

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 14:48):

This instance code is exactly using the type class inference system to construct the term which you asked for. But usually the type class inference system can be trusted to handle this question completely, and users don't have to construct this term at all. Why did you want this coercion?

view this post on Zulip Anthony Bordg (Oct 05 2018 at 16:35):

This instance code is exactly using the type class inference system to construct the term which you asked for. But usually the type class inference system can be trusted to handle this question completely, and users don't have to construct this term at all. Why did you want this coercion?

@Kevin Buzzard I want to use polynomial.eval with a field (the default argument is a commutative semiring).

view this post on Zulip Johan Commelin (Oct 05 2018 at 16:36):

That should work out of the box

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:36):

Are these typeclasses not just all resolved using type class inference?

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:40):

import data.polynomial
definition KX (K : Type) [field K] := polynomial K

It just works when you do it this way @Anthony Bordg

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:43):

import data.polynomial

definition KX (K : Type) [field K] := polynomial K

open polynomial

variables {K : Type} [field K] [decidable_eq K]

lemma eval_works (k : K) : eval k X = k := by simp

Last updated: May 16 2021 at 05:21 UTC