Zulip Chat Archive

Stream: general

Topic: Possible Bug


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

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

view this post on Zulip Johan Commelin (May 14 2019 at 04:36):

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

view this post on Zulip Johan Commelin (May 14 2019 at 04:37):

Aaah I do!

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:41):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:41):

use has_coe_t instead

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:47):

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

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

view this post on Zulip James Shaker (May 14 2019 at 04:48):

has_coe_t doesn't seem to fix the issue

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

view this post on Zulip Johan Commelin (May 14 2019 at 04:51):

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

view this post on Zulip Johan Commelin (May 14 2019 at 04:51):

Aaahrg! Stupid copy paste buffer fixed the link

view this post on Zulip Johan Commelin (May 14 2019 at 04:52):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:52):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:53):

it's some typeclass architecture bug

view this post on Zulip Mario Carneiro (May 14 2019 at 04:53):

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

view this post on Zulip James Shaker (May 14 2019 at 04:54):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:54):

working on it

view this post on Zulip Mario Carneiro (May 14 2019 at 04:54):

but I think the power_series coercion is also a bad instance

view this post on Zulip Mario Carneiro (May 14 2019 at 04:54):

for similar reasons

view this post on Zulip James Shaker (May 14 2019 at 04:54):

ok so it would be safe if I used has_coe_t?

view this post on Zulip James Shaker (May 14 2019 at 04:54):

for power_series?

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:55):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 04:56):

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

view this post on Zulip James Shaker (May 14 2019 at 04:59):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 05:04):

#1028

view this post on Zulip Johan Commelin (May 14 2019 at 05:08):

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

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

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

view this post on Zulip Chris Hughes (May 14 2019 at 17:57):

Do mathematicians use non injective coes?

view this post on Zulip Kevin Buzzard (May 14 2019 at 18:13):

That's an interesting question.

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

view this post on Zulip Reid Barton (May 14 2019 at 18:15):

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

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

view this post on Zulip Reid Barton (May 14 2019 at 18:17):

I guess I had numerals in mind


Last updated: May 11 2021 at 00:31 UTC