Zulip Chat Archive

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?

Kenny Lau (Jul 11 2020 at 09:02):

no idea

Kevin Buzzard (Jul 11 2020 at 09:08):

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

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

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

aha!

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

algebra_tower should be algebra_t

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

@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: Dec 20 2023 at 11:08 UTC