## Stream: maths

### Topic: coercion from ℚ to ℝ

#### Kevin Buzzard (Jan 19 2020 at 09:22):

What's the canonical name for the coercion from rat to real? I had imagined coe, but

instance : is_semiring_hom (coe : ℚ → ℝ) := by apply_instance


times out.

instance : is_semiring_hom (rat.cast : ℚ → ℝ) := by apply_instance


works fine, but I need that it's injective and rat.cast_injective works with coe. Which one am I supposed to be using?

#### Kevin Buzzard (Jan 19 2020 at 09:27):

import data.set.basic set_theory.schroeder_bernstein
import data.set.countable
import ring_theory.algebraic
import data.polynomial
import data.rat.default
import data.real.basic data.real.cardinality
import tactic.linarith tactic.fin_cases

noncomputable theory
local attribute [instance] classical.prop_decidable


might be relevant here (this is work of a student)

#### Patrick Massot (Jan 19 2020 at 09:30):

In such an algebraic context I would say rat.cast is what you want. Here you are really using that ℝ is a division ring, not the fact that it contains ℚ.

#### Mario Carneiro (Jan 19 2020 at 09:34):

coe is defeq to rat.cast

#### Mario Carneiro (Jan 19 2020 at 09:34):

It is written using coe, but the lemmas have rat.cast based names

#### Kevin Buzzard (Jan 19 2020 at 09:38):

I know they're defeq but I got that timeout. Is it a missing instance then?

#### Kevin Buzzard (Jan 19 2020 at 09:40):

A student wants to pass from Q[X] to R[X] a lot

#### Mario Carneiro (Jan 19 2020 at 10:13):

it's a missing instance

#### Kevin Kappelmann (Jul 10 2020 at 22:13):

Kinda related to this topic. I am failing to coerce a structure containing a rational number to a structure containing a discrete_linear_ordered_field (or a division_ring for that matter):

import algebra.continued_fractions.computation.basic

namespace generalized_continued_fraction
open generalized_continued_fraction as gcf

variables {α : Type*} [discrete_linear_ordered_field α]

-- set_option pp.all true
-- #check rat.cast_coe

-- works
#check (↑(⟨0, rat.mk 1 2⟩ : ℤ × ℚ) : ℤ × α)

/-
failed to synthesize type class instance for
...
has_lift_t (gcf.int_fract_pair ℚ) (gcf.int_fract_pair α)
-/
#check (↑(⟨0, rat.mk 1 2⟩ : int_fract_pair ℚ) : int_fract_pair α


In algebra.continued_fractions.computation.basic, I have

structure int_fract_pair := (b : ℤ) (fr : K)

variables {K β : Type*} [has_coe K β]

/-- Coerce a pair by coercing the fractional component. -/
instance has_coe_to_int_fract_pair : has_coe (int_fract_pair K) (int_fract_pair β) :=
⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩


I thought the coercion should work via rat.cast_coe but it does not seem to get picked up. I also swear this worked ~half a year ago :')

#### Scott Morrison (Jul 11 2020 at 01:46):

I did just change the imports in a way that may have affected some coercions. Try import data.[nat|int|rat].cast and see if one of those helps, or post a #mwe and I'll have a look.

#### Kevin Kappelmann (Jul 11 2020 at 08:50):

Changing the imports does not help. Here is a self-contained example with only a data.rat.cast import:

import data.rat.cast

variable (α : Type*)

structure my_pair := (b : ℤ) (fr : α)

variable {α}

namespace my_pair

section coe

/- Fix another type β and assume α can be converted to β. -/
variables {β : Type*} [has_coe α β]

instance has_coe_to_my_pair : has_coe (my_pair α) (my_pair β) :=
⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩

@[simp, norm_cast]
lemma coe_to_my_pair {b : ℤ} {fr : α} :
(↑(my_pair.mk b fr) : my_pair β) = my_pair.mk b (↑fr : β) :=
rfl

end coe

variable [discrete_linear_ordered_field α]

/-
failed to synthesize type class instance for
...
has_lift_t (my_pair ℚ) (my_pair α)
-/
#check (↑(⟨0, rat.mk 1 2⟩ : my_pair ℚ) : my_pair α)

-- works
#check (↑(⟨0, rat.mk 1 2⟩ : ℤ × ℚ) : ℤ × α)

end my_pair


#### Kenny Lau (Jul 11 2020 at 08:56):

import data.rat.cast

variable (α : Type*)

structure my_pair := (b : ℤ) (fr : α)

variable {α}

namespace my_pair

section coe

/- Fix another type β and assume K can be converted to β. -/
variables {β : Type*}

instance [has_coe α β] : has_coe (my_pair α) (my_pair β) :=
⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩

instance [has_coe_t α β] : has_coe_t (my_pair α) (my_pair β) :=
⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩

end coe

variable [discrete_linear_ordered_field α]

#check rat.cast_coe

-- works
#check ((⟨0, rat.mk 1 2⟩ : my_pair ℚ) : my_pair α)

-- works
#check (↑(⟨0, rat.mk 1 2⟩ : ℤ × ℚ) : ℤ × α)

end my_pair


#### Kenny Lau (Jul 11 2020 at 08:56):

the issue is that rat.cast_coe uses has_coe_t instead of has_coe

#### Kevin Kappelmann (Jul 11 2020 at 09:02):

Is this on purpose or should that be changed to has_coe?

no idea

#### Kevin Kappelmann (Jul 11 2020 at 09:08):

In data.nat.cast there is a note:

Coercions such as nat.cast_coe that go from a concrete structure such as
ℕ to an arbitrary ring α should be set up as follows:

@[priority 900] instance : has_coe_t ℕ α := ⟨...⟩

It needs to be has_coe_t instead of has_coe because otherwise type-class
inference would loop when constructing the transitive coercion ℕ → ℕ → ℕ → ....
The reduced priority is necessary so that it doesn't conflict with instances
such as has_coe_t α (option α).


aha!

#### Kenny Lau (Jul 11 2020 at 09:14):

algebra_tower should be algebra_t

@Johan Commelin

#### Kenny Lau (Jul 11 2020 at 09:14):

that's how you do transitive closures in Lean

#### Kevin Kappelmann (Jul 11 2020 at 09:14):

Here's the commit that introduced this https://github.com/leanprover-community/mathlib/commit/06bae3e11245a3b0147709986ae7da7e9a5e35e6

#### Kevin Kappelmann (Jul 11 2020 at 09:17):

@Gabriel Ebner is the right solution in this case to then add both of the following instances?

instance [has_coe α β] : has_coe (my_pair α) (my_pair β) :=
⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩

instance [has_coe_t α β] : has_coe_t (my_pair α) (my_pair β) :=
⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩


#### Gabriel Ebner (Jul 11 2020 at 09:20):

I'm not a big fan of coercions in the first place, so my first reaction would be "add neither".

#### Kevin Kappelmann (Jul 11 2020 at 09:21):

And insert functions going from one type to another explicitly? This would give me big headaches in my case

#### Gabriel Ebner (Jul 11 2020 at 09:24):

Rereading this thread. At the very least I'd specialize it to coercions from rationals to rings. I.e. don't add has_coe* instances that have [has_coe*] arguments.

#### Kevin Kappelmann (Jul 11 2020 at 09:33):

What's the issue with pushing the coercions through the structure? I supposed the instances will not be applicable/picked up by the elaborator anyway in case one is not talking about my_pairs, which will be the case most of the time.

#### Gabriel Ebner (Jul 11 2020 at 09:37):

My distrust and dislike of coercions is based on spending too much time looking at ↑x and wondering what the types are and what the coercion does. The fewer coercion instances the better IMHO.

#### Patrick Massot (Jul 11 2020 at 09:42):

You're living in the past Gabriel, we now have widgets which will tell you everything hidden by those funny up arrows!

#### Patrick Massot (Jul 11 2020 at 09:42):

This is currently the greatest applications of the new widgets IMO.

Last updated: May 11 2021 at 16:22 UTC