Zulip Chat Archive

Stream: general

Topic: Frozen local instance


view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 08:38):

What is going on in scenarios where Lean tells me failed to revert 'c', it is a frozen local instance and then I magically fix everything by calling tactic.unfreeze_local_instances?

view this post on Zulip Simon Hudon (Mar 12 2018 at 08:39):

There was recently a change in Lean where Lean is getting more rigid with its instance cache

view this post on Zulip Mario Carneiro (Mar 12 2018 at 08:39):

Since #1920 and the surrounding commits, lean no longer lets you mess with instances in the context that are "frozen", i.e. left of the colon. These are also the only instances which are used in typeclass inference

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 08:40):

Oh, so "frozen" just means left of the colon. Alrighty, thanks.

view this post on Zulip Mario Carneiro (Mar 12 2018 at 08:40):

By the way in mathlib, there is a name for this tactic: resetI. It also is bundled together with several other tactics like haveI and exactI

view this post on Zulip Moses Schönfinkel (Mar 12 2018 at 08:46):

resetI works like a charm and saves one control space, one down arrow and one enter; win-win

view this post on Zulip Moses Schönfinkel (Mar 19 2018 at 09:01):

What is the right way to avoid having to resetI in a scenario where I have lemma f {A : Type*} [X : something A] and I want to do cases X? Is doing this actively discouraged for some reason? Or am I misunderstanding the cause of getting the frozen local instance error?

view this post on Zulip Mario Carneiro (Mar 19 2018 at 09:01):

You could put X right of the colon

view this post on Zulip Moses Schönfinkel (Mar 19 2018 at 09:04):

Right, so that's it, thanks.

view this post on Zulip Mario Carneiro (Mar 19 2018 at 09:05):

Also, resetI is not a "code smell" or other poor practice you are making it out to be. Lean is doing an optimization that works in most cases, and to make it easy for tactic scripting it is assumed that you usually don't want to be resetting instances ('usually' meaning not after every tactic), but this requires the user to explicitly mark that they are doing this, which is a bit unpleasant to see and explain but would have otherwise been done automatically anyway.

view this post on Zulip Moses Schönfinkel (Mar 19 2018 at 09:09):

Good enough for me, I'll keep on resetIng relentlessly then.

view this post on Zulip Moses Schönfinkel (Mar 19 2018 at 09:09):

Thanks again :).

view this post on Zulip Sebastian Ullrich (Mar 19 2018 at 09:56):

@Moses Schönfinkel

Is doing this actively discouraged for some reason?

It actually is, see the issues discussed at https://github.com/leanprover/lean/commit/16f28315eeddf996f85bff96954cd31a94aa4562#diff-b9da5b9cf1417a3f4da2b3adda3eea2fR96

view this post on Zulip Mario Carneiro (Mar 19 2018 at 10:07):

Ah, that's true. This only is a problem if your typeclass instance is inferred in some function in your goal (in the decidable case this is like when you have an if in your goal and you try to clean it up by case on the decidable parameter). It falls under the more general heading "don't have non-canonical typeclass proofs in your functions, it's confusing"

view this post on Zulip Mario Carneiro (Mar 19 2018 at 10:09):

But that's not to say that it is disallowed, because sometimes you just have to do it, if your typeclass is some complicated inductive thing this may be the only option. But try to get rid of those functions as soon as possible after the cases


Last updated: May 08 2021 at 10:12 UTC