Zulip Chat Archive

Stream: general

Topic: Possible Bug


James Shaker (May 14 2019 at 04:34):

Hello, I’m one of @Scott Morrison 's students and I’ve got what could possibly be an issue in mathlib. I was wondering if others would be willing to take a look before I file a bug report on GitHub:

import ring_theory.algebra -- commenting this out fixes the problem

def power_series (α : Type) [comm_ring α] := ℕ → α

variables {α : Type} [comm_ring α]

def of_alpha (x : α) : power_series α
| 0 := x
| _ := 0

instance : has_coe α (power_series α) := ⟨of_alpha⟩

example (x : α) : power_series α := (x : power_series α) -- can't find defined instance

As described in the comments, the simple coercion from α to power_series α fails despite the instance being clearly defined on the line above. What’s more it works correctly when the algebra import is commented.

Johan Commelin (May 14 2019 at 04:35):

Where do you want to file a bug report? Lean doesn't take bug reports.... didn't Scott tell you this?

Johan Commelin (May 14 2019 at 04:36):

These kind of issues are really quite annoying. I don't spot anything obviously wrong.

Johan Commelin (May 14 2019 at 04:37):

Aaah I do!

Mario Carneiro (May 14 2019 at 04:41):

You shouldn't use has_coe for these kinds of coercions, it will cause lean to go in a loop

Mario Carneiro (May 14 2019 at 04:41):

There's some discussion about the coercion for option A in the file in core

Mario Carneiro (May 14 2019 at 04:41):

use has_coe_t instead

Mario Carneiro (May 14 2019 at 04:42):

I did not get a "can't find instance" error, I get a instance resolution depth overflow

Mario Carneiro (May 14 2019 at 04:47):

Oh, there is a bad instance in group_theory.coset, instance : has_coe α (quotient s) := ⟨mk⟩

James Shaker (May 14 2019 at 04:47):

Sorry that's the same issue I get, just forgot to include the specifics of the bug

James Shaker (May 14 2019 at 04:48):

has_coe_t doesn't seem to fix the issue

James Shaker (May 14 2019 at 04:49):

@Johan Commelin I think Scott was referring to posting an issue on the GitHub repo but I'm not 100% sure..

Johan Commelin (May 14 2019 at 04:51):

If you want to post issues, please post them here: https://github.com/leanprover-community/lean

Johan Commelin (May 14 2019 at 04:51):

Aaahrg! Stupid copy paste buffer fixed the link

Johan Commelin (May 14 2019 at 04:52):

Anyway, the best way to deal with such issues is by posting them here :grinning:

Mario Carneiro (May 14 2019 at 04:52):

this isn't a lean problem it's a mathlib problem

Mario Carneiro (May 14 2019 at 04:53):

it's some typeclass architecture bug

Mario Carneiro (May 14 2019 at 04:53):

but I suspect the result will be that you can't define this coercion

James Shaker (May 14 2019 at 04:54):

Should we just turn off that instance (in group_theory.coset)?

Mario Carneiro (May 14 2019 at 04:54):

working on it

Mario Carneiro (May 14 2019 at 04:54):

but I think the power_series coercion is also a bad instance

Mario Carneiro (May 14 2019 at 04:54):

for similar reasons

James Shaker (May 14 2019 at 04:54):

ok so it would be safe if I used has_coe_t?

James Shaker (May 14 2019 at 04:54):

for power_series?

Mario Carneiro (May 14 2019 at 04:55):

basically, lean will try to eagerly apply transitivity paths from the left for has_coe, so you end up reducing the problem has_coe A B to has_coe (power_series A) B and then has_coe (power_series (power_series A)) B, etc

Mario Carneiro (May 14 2019 at 04:55):

using has_coe_t will ensure that it will only apply the instance once

Mario Carneiro (May 14 2019 at 04:56):

it looks like removing the quotient_group.mk instance fixes the problem

James Shaker (May 14 2019 at 04:59):

Can I try PR-ing that, or are you already there?

Mario Carneiro (May 14 2019 at 05:04):

#1028

Johan Commelin (May 14 2019 at 05:08):

Can we use regexes to see if there are more of those evil instances in mathlib?

Mario Carneiro (May 14 2019 at 05:10):

Don't you know not to use regex for things it wasn't designed for? https://stackoverflow.com/a/1732454/890016

Kevin Buzzard (May 14 2019 at 17:54):

#1028

Even mathematicians, the most coe-est people around, usually use notation for passage to the quotient; they usually put some sort of bar over the thing they're coercing.

Chris Hughes (May 14 2019 at 17:57):

Do mathematicians use non injective coes?

Kevin Buzzard (May 14 2019 at 18:13):

That's an interesting question.

Kevin Buzzard (May 14 2019 at 18:14):

I think that sometimes mathematicians use the localization map RR[1/S]R\to R[1/S] as a coercion, perhaps because in most cases it's injective.

Reid Barton (May 14 2019 at 18:15):

How about ZZ/n\mathbb{Z} \to \mathbb{Z}/n

Kevin Buzzard (May 14 2019 at 18:17):

We coerce numerals but in general I might be tempted to write x\overline{x} for the image of xZx\in\mathbb{Z}. Or am I just being naive?

Reid Barton (May 14 2019 at 18:17):

I guess I had numerals in mind


Last updated: Dec 20 2023 at 11:08 UTC