coercion from ℚ to ℝ

Stream: maths

[Kevin Buzzard]

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]

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]

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]

coe is defeq to rat.cast

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

it's a missing instance

[Kevin Kappelmann]

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]

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]

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]

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]

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

[Kevin Kappelmann]

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

[Kenny Lau]

no idea

[Kevin Buzzard]

I asked about finset to set being coe_t not coe recently and got the same answer

[Kevin Kappelmann]

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 α)`.

[Kenny Lau]

aha!

[Kenny Lau]

algebra_tower should be algebra_t

[Kenny Lau]

@Johan Commelin

[Kenny Lau]

that's how you do transitive closures in Lean

[Kevin Kappelmann]

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

[Kevin Kappelmann]

@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]

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

[Kevin Kappelmann]

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

[Gabriel Ebner]

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]

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]

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]

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

[Patrick Massot]

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