Zulip Chat Archive

Stream: general

Topic: deterministic timeout with ideal.quotient.mk

Aditya Agarwal (Mar 01 2019 at 07:20):

I am getting a deterministic timeout when I try to state ideal.quotient.mk (ideal.span (singleton (C r))) p = 0 in the context of an integral domain.
@Scott Morrison has constructed a minimal example here : https://github.com/chocolatier/theoremproving/blob/master/src/timeout-mwe.lean , And done some debugging work.

variables {α : Type} [integral_domain α]
lemma timeout {p : polynomial α} {r : α} : ideal.quotient.mk (ideal.span (singleton (C r))) p = 0 := sorry

times out, but replacing integral_domain αwith comm_ring αmakes it work. Setting trace.class_instances true shows that the type class resolution is going crazy in the integral domain case.

Specifically, it is trying to find an instance of has_zero but it gets stuck in the path that searches for @no_zero_divisors.to_has_zero, and never tries any other branch.

I'm not sure why this is happening or how to fix it.

Mario Carneiro (Mar 01 2019 at 07:21):

did you try increasing the instance depth?

Aditya Agarwal (Mar 01 2019 at 07:26):

I've tried

set_option class.instance_max_depth 1000000

but it still times out.

Scott Morrison (Mar 05 2019 at 02:27):

Hi @Chris Hughes and @Kenny Lau, do you know what could be going on here?

Kenny Lau (Mar 05 2019 at 02:27):

does ideal.span take two arguments?

Kenny Lau (Mar 05 2019 at 02:28):

what is singleton?

Scott Morrison (Mar 05 2019 at 02:29):

There's a gist of the typeclass resolution for 0 on the rhs going nuts here: https://gist.githubusercontent.com/semorrison/fc7fd83ee0da4a875db083c01ef7a0fc/raw/80e4adb669a5be6a9b4e602972e48d0d054bae1d/gistfile1.txt

Kenny Lau (Mar 05 2019 at 02:29):

I'm half convinced that ideal isn't the problem, polynomial is

Kenny Lau (Mar 05 2019 at 02:34):

I have no idea why it doesn't work

Last updated: Dec 20 2023 at 11:08 UTC