Zulip Chat Archive

Stream: general

Topic: timeout when working with ideal of polynomial ring


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

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

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

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

view this post on Zulip Casper Putz (Aug 14 2019 at 21:06):

Thanks Rob for the quick fix!

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 05:11):

I can probably help with power_series, since I wrote it not too long ago.

view this post on Zulip Johan Commelin (Sep 03 2019 at 05:11):

What kind of problems are you seeing?

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

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 07:11):

Stupid Lean...

view this post on Zulip Scott Morrison (Sep 03 2019 at 07:58):

Weird, that's working for me.

view this post on Zulip Johan Commelin (Sep 03 2019 at 08:08):

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 08:08):

L581?

view this post on Zulip Casper Putz (Sep 03 2019 at 08:10):

I will try to fix free_comm_ring.lean. Did a bit already

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

view this post on Zulip Casper Putz (Sep 03 2019 at 10:31):

I fixed the errors in free_comm_ring.lean

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

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:34):

basically you can't evaluate single anymore by defeq

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:34):

But why not?

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:34):

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:35):

This is stupid

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:35):

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:35):

where the if is no longer decidable because classical

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:35):

solution: stop using defeq

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:36):

use simp

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:36):

You might as well say, "stop using definitions"

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:36):

not at all

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:36):

And simp is slow... we learnt that.

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:36):

use definitional equations

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:36):

use rw [single]

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:37):

Yep, but this single is hidden behind 4 definitions...

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:37):

And rfl used to blast through them

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:37):

that's not a good thing

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:37):

Why are you unfolding 4 definitions?

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:38):

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:38):

maybe two, but that's bad practice

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:38):

4 is abuse

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:39):

What are you proving?

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:39):

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:40):

the proof should be mv_power_series.coeff_C_zero

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:40):

that's one definition unfold

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:41):

Your proof doesn't work

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:41):

Because single unit.star 0 is not defeq to 0

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:42):

Nope, even that doesn't work

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:43):

This used to be harmless, but now it is not

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:43):

Because of that single () n tagging at the end

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

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:45):

No, those coeffs are the same

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:45):

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:45):

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

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:45):

Yes...

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:46):

But power_series.C is no longer defeq to power_series.monomial 0

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:46):

why? Did the definition change?

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:46):

No

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:46):

It says that it is defined as exactly that

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:46):

Someone removed a [decidable_eq α]. Em tasol.

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:47):

oh, I was looking at the wrong C

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

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:49):

if you had that it would be a single rw

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:50):

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

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:51):

And the proof boils down to single () 0 = 0, which should be in finsupp

view this post on Zulip Mario Carneiro (Sep 03 2019 at 12:52):

single_zero

view this post on Zulip Johan Commelin (Sep 03 2019 at 12:55):

Thanks for your patience

view this post on Zulip Kenny Lau (Dec 28 2019 at 07:07):

so why does decidable_eq cause problem afterall?

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