Zulip Chat Archive

Stream: maths

Topic: max resolution depth reached


view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 14:37):

I am writing a have statement in a proof, and I get the following error:

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

Any help is appreciated! Thank you!

view this post on Zulip Johan Commelin (Oct 20 2020 at 14:39):

Is this on a branch of mathlib?

view this post on Zulip Johan Commelin (Oct 20 2020 at 14:39):

Can you share more code?

view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 14:41):

Johan Commelin said:

Is this on a branch of mathlib?

Yeah, it is on dd-iff. I will just update it.

view this post on Zulip Johan Commelin (Oct 20 2020 at 14:42):

Ok. Once you've done that, please post a link that points precisely to the line where you get this error.

view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 14:43):

https://github.com/leanprover-community/mathlib/blob/e45059d0160da6e058b638902c374e85c39a21ac/src/ring_theory/dedekind_domain.lean#L250

view this post on Zulip Johan Commelin (Oct 20 2020 at 14:47):

Does it help if you write down the type of the have statement?

view this post on Zulip Johan Commelin (Oct 20 2020 at 14:51):

Aha, the error is actually on the change line above it

view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 14:52):

That line is commented out, though.

view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 14:54):

Also, I managed to make the line work, but it shows me something completely different. It should show me something of the form M*P ≤ N*P , but instead, it shows me ?m_1 ∈ ↑↑p * ?m_2 and gives me 3 additional goals..

view this post on Zulip Johan Commelin (Oct 20 2020 at 15:02):

Ashvni Narayanan said:

That line is commented out, though.

Yes, and I get a different error from what you wrote in the top post.

view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 15:03):

Oh!

view this post on Zulip Johan Commelin (Oct 20 2020 at 15:04):

This works:

lemma is_dedekind_domain_inv.is_dedekind_domain (h : is_dedekind_domain_inv A) :
  is_dedekind_domain A :=
begin
  rcases h with h1, h2⟩,
  refine h1, _, _, _⟩,
  { unfold is_noetherian_ring,
    fconstructor,
    change  (I : ideal A), I.fg,
    rintros I,
  --   fconstructor,
    sorry, },
  { unfold dimension_le_one,
    rintros p nz hp,
    have hpinv := h2 p,
    have hpmax := exists_le_maximal p hp.1,
    rcases hpmax with M, hM1, hM2⟩,
    specialize h2 M,
    specialize hpinv ((coe_ne_bot A p).1 nz),
    specialize h2 ( (coe_ne_bot A M).1 (max_ideal_ne_bot A M hM1 h1)),
    set I := (M : fractional_ideal (fraction_ring.of A))⁻¹ *
      (p : fractional_ideal (fraction_ring.of A)) with hI,
    have f : (M : fractional_ideal (fraction_ring.of A)) * I = (p : fractional_ideal (fraction_ring.of A)),
    { change M * ((M)⁻¹ * p) = p,
      rw [ mul_assoc, h2, one_mul], },
    by_cases hp : p = M,
    { rwa hp, },
    exfalso,
    have g : I  (p : fractional_ideal (fraction_ring.of A)),
    { apply frac_ideal_le_ideal A M _ _ _ f,
      sorry },
    rw <-subtype.coe_le_coe at g,
    rw hI at g,
    norm_cast at g,
    change ((M)⁻¹ * p)  p at g,
    -- have g' := submodule.mul_le_mul_left g (↑M).coe,
    sorry, },
  -- { sorry, },
end

view this post on Zulip Johan Commelin (Oct 20 2020 at 15:05):

I changed the let I to a set I ... with hI

view this post on Zulip Ashvni Narayanan (Oct 20 2020 at 15:11):

Yeah, that does work. Thank you!


Last updated: May 12 2021 at 08:14 UTC