timeout when working with ideal of polynomial ring

Stream: general

[Casper Putz]

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]

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

[Kevin Buzzard]

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]

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]

Thanks Rob for the quick fix!

[Casper Putz]

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]

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]

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

[Casper Putz]

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

[Scott Morrison]

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]

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

[Johan Commelin]

What kind of problems are you seeing?

[Johan Commelin]

@Scott Morrison I already have errors for mv_polynomial.C_add on L52 of mv_polynomial.lean

[Johan Commelin]

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]

Stupid Lean...

[Scott Morrison]

Weird, that's working for me.

[Johan Commelin]

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

[Johan Commelin]

L581?

[Casper Putz]

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

[Scott Morrison]

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

I fixed the errors in free_comm_ring.lean

[Johan Commelin]

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]

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]

basically you can't evaluate single anymore by defeq

[Johan Commelin]

But why not?

[Mario Carneiro]

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

[Johan Commelin]

This is stupid

[Mario Carneiro]

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

[Mario Carneiro]

where the if is no longer decidable because classical

[Mario Carneiro]

solution: stop using defeq

[Mario Carneiro]

use simp

[Johan Commelin]

You might as well say, "stop using definitions"

[Mario Carneiro]

not at all

[Johan Commelin]

And simp is slow... we learnt that.

[Mario Carneiro]

use definitional equations

[Mario Carneiro]

use rw [single]

[Johan Commelin]

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

[Johan Commelin]

And rfl used to blast through them

[Mario Carneiro]

that's not a good thing

[Johan Commelin]

And now I need to delta 5 things, and than I can rw finsupp.single_zero or something silly like that.

[Mario Carneiro]

Why are you unfolding 4 definitions?

[Mario Carneiro]

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

[Mario Carneiro]

maybe two, but that's bad practice

[Mario Carneiro]

4 is abuse

[Johan Commelin]

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]

What are you proving?

[Johan Commelin]

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

[Mario Carneiro]

the proof should be mv_power_series.coeff_C_zero

[Johan Commelin]

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

[Mario Carneiro]

that's one definition unfold

[Johan Commelin]

Your proof doesn't work

[Johan Commelin]

Because single unit.star 0 is not defeq to 0

[Mario Carneiro]

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]

Nope, even that doesn't work

[Johan Commelin]

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]

This used to be harmless, but now it is not

[Johan Commelin]

Because of that single () n tagging at the end

[Johan Commelin]

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

[Mario Carneiro]

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]

No, those coeffs are the same

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Yes...

[Johan Commelin]

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

[Mario Carneiro]

why? Did the definition change?

[Johan Commelin]

No

[Mario Carneiro]

It says that it is defined as exactly that

[Johan Commelin]

Someone removed a [decidable_eq α]. Em tasol.

[Johan Commelin]

Over here it says

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

[Mario Carneiro]

oh, I was looking at the wrong C

[Johan Commelin]

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]

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

[Mario Carneiro]

if you had that it would be a single rw

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

single_zero

[Johan Commelin]

Thanks for your patience

[Kenny Lau]

so why does decidable_eq cause problem afterall?

[Kenny Lau]

(I was pointed to this topic by #1391)