# Zulip Chat Archive

## Stream: general

### Topic: timeout when working with ideal of polynomial ring

#### Casper Putz (Aug 14 2019 at 14:17):

I was working with the following setup:

variables (α : Type*) [discrete_field α] variables (I : ideal (polynomial α))

For some reason I get a deterministic timeout whenever I do anything with `I`

. For example: this gives a timeout:

#check (I : submodule (polynomial α) (polynomial α))

But also writing down `I.carrier`

or a membership statement `p ∈ I`

gives a timeout. Working over an `integral_domain α`

or a `field α`

also causes the timeout. However, in the following setup I do not get a timeout:

variables (α : Type*) [comm_ring α] [division_ring α] [decidable_eq α] variables (I : ideal (polynomial α)) #check I.carrier

(While a `field`

is just a `comm_ring`

and `division_ring`

, so there must be some weird instance kicking in or something)

The problem is similar to the problem posted here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deterministic.20timeout.20with.20ideal.2Equotient.2Emk.

I tried increasing the class instance depth, and tried to find out what was happening using `trace.class_instances`

but I could not manage to find the problem. Anybody any idea of why this may happen (and how one could fix it)?

#### Rob Lewis (Aug 14 2019 at 20:20):

This is yet another type class issue. The temporary fix: `instance mpp : module (polynomial α) (polynomial α) := by apply_instance`

#### Kevin Buzzard (Aug 14 2019 at 20:36):

So what is happening here? Making `mpp`

an instance makes type class inference behave differently? Basically it finds it earlier? Could one use priorities to somehow fix this?

#### Rob Lewis (Aug 14 2019 at 20:46):

The logs are migraine inducing, so I don't have an exact answer. But basically yeah, if `mpp`

is the last instance added it's the first one tried, and the resolution path avoids some very costly search path. It's possible a local priority change could fix this instance, and I don't think we ever systematically adopted this idea from Floris (which we should): https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/more.20type.20class.20inference.20issues/near/167026105

#### Casper Putz (Aug 14 2019 at 21:06):

Thanks Rob for the quick fix!

#### Casper Putz (Aug 14 2019 at 21:11):

Ah that makes sense. I agree about the migraine haha. I saw it doing some weird stuff like using `discrete_field.to_local_ring.to_comm_ring`

instead of directly using that a field is a commutative ring

#### Scott Morrison (Aug 14 2019 at 21:29):

Hi Casper, if you're working on polynomials, and struggling with timeouts, you might be interested in completing the work I started on the `decidable_eq`

branch, stripping out all the decidability conditions from polynomials and multivariable polynomials. Unfortunately I haven't had time to finish, but I hope it's mostly downhill from where I got up to --- just fix the remaining errors!

#### Reid Barton (Aug 14 2019 at 21:55):

I didn't realize you had already started this, I was going to propose it as a possible fix as well.

#### Casper Putz (Aug 15 2019 at 08:38):

Hi Scott, I may actually do that! I think I will give it a look this weekend.

#### Scott Morrison (Sep 03 2019 at 05:08):

I made quite a bit more progress on this now, but still have problems in `power_series.lean`

and `free_comm_ring.lean`

. Any help (feel free to commit direct to the `decidable_eq`

branch) much appreciated.

#### Johan Commelin (Sep 03 2019 at 05:11):

I can probably help with `power_series`

, since I wrote it not too long ago.

#### Johan Commelin (Sep 03 2019 at 05:11):

What kind of problems are you seeing?

#### Johan Commelin (Sep 03 2019 at 07:10):

@Scott Morrison I already have errors for `mv_polynomial.C_add`

on L52 of `mv_polynomial.lean`

#### Johan Commelin (Sep 03 2019 at 07:11):

For some reason Lean doesn't agree that `C a`

is `single 0 a`

, even though it's true by definition. If I then hit it with another `refl`

it shuts up and moves on.

#### Johan Commelin (Sep 03 2019 at 07:11):

Stupid Lean...

#### Scott Morrison (Sep 03 2019 at 07:58):

Weird, that's working for me.

#### Johan Commelin (Sep 03 2019 at 08:08):

@Scott Morrison Where is the first error that you hit in power series?

#### Johan Commelin (Sep 03 2019 at 08:08):

L581?

#### Casper Putz (Sep 03 2019 at 08:10):

I will try to fix `free_comm_ring.lean`

. Did a bit already

#### Scott Morrison (Sep 03 2019 at 10:00):

@Johan Commelin, the first error I see is in `/src/ring_theory/power_series.lean`

at line 560:

/Users/scott/projects/lean/mathlib/src/ring_theory/power_series.lean:560:36: error: type mismatch at application mul_inv_of_unit (1 - φ) ?m_1 h term h has type 1 - coeff 0 φ = ↑u but is expected to have type coeff 0 (1 - φ) = ↑?m_1

#### Casper Putz (Sep 03 2019 at 10:31):

I fixed the errors in `free_comm_ring.lean`

#### Johan Commelin (Sep 03 2019 at 12:29):

The biggest source of errors in `power_series.lean`

seems to come from the fact that `single unit.star n`

is no longer defeq to `n`

, for `n : ℕ`

...

#### Johan Commelin (Sep 03 2019 at 12:30):

I'm not sure how that happened. Because this is a statement about `unit`

and `nat`

, which shouldn't be affected by polynomials going classical.

#### Mario Carneiro (Sep 03 2019 at 12:34):

basically you can't evaluate `single`

anymore by defeq

#### Johan Commelin (Sep 03 2019 at 12:34):

But why not?

#### Mario Carneiro (Sep 03 2019 at 12:34):

there is a proof of `n = n`

by classical in there

#### Johan Commelin (Sep 03 2019 at 12:35):

This is stupid

#### Mario Carneiro (Sep 03 2019 at 12:35):

it's something like `single unit.star n := if n = n then 1 else 0`

#### Mario Carneiro (Sep 03 2019 at 12:35):

where the `if`

is no longer decidable because classical

#### Mario Carneiro (Sep 03 2019 at 12:35):

solution: stop using defeq

#### Mario Carneiro (Sep 03 2019 at 12:36):

use `simp`

#### Johan Commelin (Sep 03 2019 at 12:36):

You might as well say, "stop using definitions"

#### Mario Carneiro (Sep 03 2019 at 12:36):

not at all

#### Johan Commelin (Sep 03 2019 at 12:36):

And `simp`

is slow... we learnt that.

#### Mario Carneiro (Sep 03 2019 at 12:36):

use definitional equations

#### Mario Carneiro (Sep 03 2019 at 12:36):

use `rw [single]`

#### Johan Commelin (Sep 03 2019 at 12:37):

Yep, but this `single`

is hidden behind 4 definitions...

#### Johan Commelin (Sep 03 2019 at 12:37):

And `rfl`

used to blast through them

#### Mario Carneiro (Sep 03 2019 at 12:37):

that's not a good thing

#### Johan Commelin (Sep 03 2019 at 12:37):

And now I need to `delta`

5 things, and than I can `rw finsupp.single_zero`

or something silly like that.

#### Mario Carneiro (Sep 03 2019 at 12:37):

Why are you unfolding 4 definitions?

#### Mario Carneiro (Sep 03 2019 at 12:38):

you should only ever need to unfold one at most at a time

#### Mario Carneiro (Sep 03 2019 at 12:38):

maybe two, but that's bad practice

#### Mario Carneiro (Sep 03 2019 at 12:38):

4 is abuse

#### Johan Commelin (Sep 03 2019 at 12:38):

Because `power_series.C`

is defined as `mv_power_series.C`

which is defined as `mv_power_series.monomial 0`

, and `power_series.monomial`

is defined as `mv_power_series.monomial`

, and I these definitions to commute by `rfl`

.

#### Mario Carneiro (Sep 03 2019 at 12:39):

What are you proving?

#### Johan Commelin (Sep 03 2019 at 12:39):

@[simp] lemma coeff_C_zero (a : α) : coeff 0 (C a) = a :=

#### Mario Carneiro (Sep 03 2019 at 12:40):

the proof should be `mv_power_series.coeff_C_zero`

#### Johan Commelin (Sep 03 2019 at 12:40):

by { convert coeff_monomial' 0 a, delta C mv_power_series.C monomial, rw finsupp.single_zero }

#### Mario Carneiro (Sep 03 2019 at 12:40):

that's one definition unfold

#### Johan Commelin (Sep 03 2019 at 12:41):

Your proof doesn't work

#### Johan Commelin (Sep 03 2019 at 12:41):

Because `single unit.star 0`

is not defeq to `0`

#### Mario Carneiro (Sep 03 2019 at 12:41):

I'm not 100% on the exact definitions of everything here, but you should be able to unfold things until it's a statement about `mv_polynomial`

, and then apply the appropriate lemma

#### Johan Commelin (Sep 03 2019 at 12:42):

Nope, even that doesn't work

#### Johan Commelin (Sep 03 2019 at 12:43):

This definition might be relevant:

/-- The `n`th coefficient of a formal power series.-/ def coeff (n : ℕ) : power_series α → α := mv_power_series.coeff (single () n)

#### Johan Commelin (Sep 03 2019 at 12:43):

This used to be harmless, but now it is not

#### Johan Commelin (Sep 03 2019 at 12:43):

Because of that `single () n`

tagging at the end

#### Johan Commelin (Sep 03 2019 at 12:44):

I can't understand why we can't have classical coefficients living together with a constructively decidable `unit`

and `nat`

#### Mario Carneiro (Sep 03 2019 at 12:44):

I see this in the file now:

@[simp] lemma coeff_monomial' (n : σ →₀ ℕ) (a : α) : coeff n (monomial n a) = a := if_pos rfl @[simp] lemma coeff_C_zero (a : α) : coeff 0 (C a : mv_power_series σ α) = a := coeff_monomial' 0 a

are you saying that the two `coeff`

s are different here?

#### Johan Commelin (Sep 03 2019 at 12:45):

No, those `coeff`

s are the same

#### Mario Carneiro (Sep 03 2019 at 12:45):

I can't understand why we can't have classical coefficients living together with a constructively decidable unit and nat

That's called accepting a `decidable_eq`

instance, and we tried that

#### Mario Carneiro (Sep 03 2019 at 12:45):

then what's the problem? they look defeq to me

#### Mario Carneiro (Sep 03 2019 at 12:45):

def C (a : α) : mv_power_series σ α := monomial 0 a

#### Johan Commelin (Sep 03 2019 at 12:45):

Yes...

#### Johan Commelin (Sep 03 2019 at 12:46):

But `power_series.C`

is no longer defeq to `power_series.monomial 0`

#### Mario Carneiro (Sep 03 2019 at 12:46):

why? Did the definition change?

#### Johan Commelin (Sep 03 2019 at 12:46):

No

#### Mario Carneiro (Sep 03 2019 at 12:46):

It says that it is defined as exactly that

#### Johan Commelin (Sep 03 2019 at 12:46):

Someone removed a `[decidable_eq α]`

. Em tasol.

#### Johan Commelin (Sep 03 2019 at 12:47):

Over here it says

/-- The constant formal power series.-/ def C : α → power_series α := mv_power_series.C

#### Mario Carneiro (Sep 03 2019 at 12:47):

oh, I was looking at the wrong C

#### Johan Commelin (Sep 03 2019 at 12:48):

I mean... I can fix these errors, but the barrier between `mv_power_series unit`

and `power_series`

just got a lot bigger. Because we don't have good definitional reductions anymore.

#### Mario Carneiro (Sep 03 2019 at 12:49):

I see, so the problem is that there is no theorem `power_series.C a = monomial 0 a`

#### Mario Carneiro (Sep 03 2019 at 12:49):

if you had that it would be a single rw

#### Johan Commelin (Sep 03 2019 at 12:50):

Aha... I guess that theorem was missing, because it used to be defeq...

#### Mario Carneiro (Sep 03 2019 at 12:51):

And the proof boils down to `single () 0 = 0`

, which should be in finsupp

#### Mario Carneiro (Sep 03 2019 at 12:52):

`single_zero`

#### Johan Commelin (Sep 03 2019 at 12:55):

Thanks for your patience

#### Kenny Lau (Dec 28 2019 at 07:07):

so why does `decidable_eq`

cause problem afterall?

#### Kenny Lau (Dec 28 2019 at 07:07):

(I was pointed to this topic by #1391)

Last updated: May 10 2021 at 18:22 UTC