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

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: Dec 20 2023 at 11:08 UTC