Zulip Chat Archive

Stream: general

Topic: Unknown error while type-checking with `use`


view this post on Zulip Kenji Nakagawa (Aug 16 2020 at 18:16):

For some reason, lean just dies after the use M line, and sometimes (eventually?), you can get unknown error while type-checking theorem (this might not be verbatim), although interestingly, using tauto at that point doesn't throw this error (also this seems to have been an error with a week ago mathlib, as well as current). Additionally, having R being an integral domain resolves this.

import ring_theory.fractional_ideal

lemma nonfield_has_prime (R : Type*) [comm_ring R] (nonfield : (I : ideal R),  < I  I <  ) : (P : ideal R), P.is_prime   < P :=
begin
  rcases nonfield with I, gt_bot, lt_top,
  have ne_top : I  , exact ne_of_lt lt_top,
  rcases ideal.exists_le_maximal I ne_top with M, maximal, gei,
  have hm := ideal.is_maximal.is_prime maximal,
  have gt_bot :  < M, exact gt_of_ge_of_gt gei gt_bot,
  use M,
   --exact ideal.is_maximal.is_prime maximal, exact gt_bot,
  --tauto,
end

view this post on Zulip Alex J. Best (Aug 16 2020 at 18:23):

Try refine ⟨M, _, _⟩, instead for now

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 18:25):

existsi M is something else which sometimes works

view this post on Zulip Bryan Gin-ge Chen (Aug 16 2020 at 18:30):

There's definitely something weird here. For me, the yellow bars just don't go away if the use M, line is present. If I comment it out then Lean quickly finishes.

view this post on Zulip Bryan Gin-ge Chen (Aug 16 2020 at 18:31):

existsi M and refine ⟨M, _, _⟩, work though.

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 19:20):

This is the well-known "use bug"; use was written because existsi was bad at type unification; I've never seen a situation where neither of them work ;-)

view this post on Zulip Rob Lewis (Aug 16 2020 at 19:45):

I think I've asked before for a #mwe of the "well-known use bug," preferably as a mathlib issue so it doesn't get lost. Ideally the example has fewer imports than this one.

view this post on Zulip Rob Lewis (Aug 16 2020 at 20:01):

The problem in this case is that the elaborator doesn't recognize that M itself isn't a proof of ∃ (P : ideal R), P.is_prime ∧ ⊥ < P. You can see that refine M times out too.

view this post on Zulip Rob Lewis (Aug 16 2020 at 20:02):

Why? I have no idea. The elaborator trace options aren't helping at all.

view this post on Zulip Mario Carneiro (Aug 16 2020 at 20:48):

Minimized:

example (R : Type*) [comm_ring R] : true :=
by { suffices M : submodule R R, exact M }

view this post on Zulip Mario Carneiro (Aug 16 2020 at 20:49):

It is fast if you provide ring or semiring instead

view this post on Zulip Mario Carneiro (Aug 16 2020 at 20:51):

It is also fast with R : Type instead of R : Type*, so maybe it has something to do with the universe unification

view this post on Zulip Rob Lewis (Aug 16 2020 at 20:54):

Hmm, with what imports? This is fast:

import algebra.module.submodule

example (R : Type*) [comm_ring R] : true :=
by { suffices M : submodule R R, exact M }

view this post on Zulip Mario Carneiro (Aug 16 2020 at 20:55):

import ring_theory.fractional_ideal

universe u
example (R : Type u) [comm_ring R] : true :=
by { suffices M : submodule R R, exact M }

view this post on Zulip Mario Carneiro (Aug 16 2020 at 20:57):

it's something in localization

view this post on Zulip Mario Carneiro (Aug 16 2020 at 20:59):

src#localization_map.coe_submodules

view this post on Zulip Rob Lewis (Aug 16 2020 at 20:59):

Looks like a coercion instance going wrong.

view this post on Zulip Mario Carneiro (Aug 16 2020 at 21:01):

yeah this is a bad instance, that coe can loop and it leaves f free

view this post on Zulip Mario Carneiro (Aug 16 2020 at 21:05):

#3832

view this post on Zulip Rob Lewis (Aug 16 2020 at 21:06):

Maybe add a comment explaining why it's not an instance?


Last updated: May 14 2021 at 07:19 UTC