Zulip Chat Archive

Stream: maths

Topic: coercion from ℚ to ℝ


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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 .

view this post on Zulip Mario Carneiro (Jan 19 2020 at 09:34):

coe is defeq to rat.cast

view this post on Zulip Mario Carneiro (Jan 19 2020 at 09:34):

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

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 09:38):

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

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 09:40):

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

view this post on Zulip Mario Carneiro (Jan 19 2020 at 10:13):

it's a missing instance

view this post on Zulip 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 :')

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 11 2020 at 08:56):

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

view this post on Zulip Kevin Kappelmann (Jul 11 2020 at 09:02):

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

view this post on Zulip Kenny Lau (Jul 11 2020 at 09:02):

no idea

view this post on Zulip 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

view this post on Zulip 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 α)`.

view this post on Zulip Kenny Lau (Jul 11 2020 at 09:14):

aha!

view this post on Zulip Kenny Lau (Jul 11 2020 at 09:14):

algebra_tower should be algebra_t

view this post on Zulip Kenny Lau (Jul 11 2020 at 09:14):

@Johan Commelin

view this post on Zulip Kenny Lau (Jul 11 2020 at 09:14):

that's how you do transitive closures in Lean

view this post on Zulip Kevin Kappelmann (Jul 11 2020 at 09:14):

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

view this post on Zulip 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 : β)⟩⟩

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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