max resolution depth reached

Stream: maths

[Ashvni Narayanan]

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!

[Johan Commelin]

Is this on a branch of mathlib?

[Johan Commelin]

Can you share more code?

[Ashvni Narayanan]

Johan Commelin said:

Is this on a branch of mathlib?

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

[Johan Commelin]

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

[Ashvni Narayanan]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Ashvni Narayanan]

That line is commented out, though.

[Ashvni Narayanan]

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

[Johan Commelin]

Ashvni Narayanan said:

That line is commented out, though.

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

[Ashvni Narayanan]

Oh!

[Johan Commelin]

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

[Johan Commelin]

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

[Ashvni Narayanan]

Yeah, that does work. Thank you!