## 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.

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?

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

But why not?

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

there is a proof of n = n by classical in there

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"

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

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):

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 nth 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 coeffs are different here?

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

No, those coeffs 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


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?

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):

so why does decidable_eq cause problem afterall?