Zulip Chat Archive

Stream: general

Topic: How to use type classes


Andrej Bauer (Sep 10 2021 at 13:51):

Why is it that in the following code apply_instance works ok in the proof of rabbit, but not in cow? The only difference is the presence of a couple of intros? This is presenting a bit of a stumbling block, is there relevant documentation that explains what's going on?

instance decidable_precompose {α β : Type}
  (p : β  Prop) (f : α  β) [h : decidable_pred p] : decidable_pred (p  f) :=
by { intro, apply h }

def rabbit (α β : Type) (p : α  β  Prop) [h : decidable_pred p] : decidable_pred (p  sum.inl)
 :=
by apply_instance

def cow (α β : Type) :  (p : α  β  Prop) [h : decidable_pred p] , decidable_pred (p  sum.inl)
 :=
 begin
   intros p h,
   apply_instance
 end

Sebastien Gouezel (Sep 10 2021 at 13:54):

Instances are only recognized as such when they are left of the colon, as in rabbit. If you want to use instances that were introduced in the course of a proof, use resetI.

Johan Commelin (Sep 10 2021 at 13:57):

Reason: performance, there is a cache somewhere that is "frozen" once the proof starts.

Andrej Bauer (Sep 10 2021 at 13:57):

Ah, very good. And also very impenetrable. Is this somewhere in the docs?

Andrej Bauer (Sep 10 2021 at 13:58):

So what would be the idomatic way of proving cow?

Sebastien Gouezel (Sep 10 2021 at 13:58):

Beginning of https://leanprover-community.github.io/mathlib_docs/tactics.html, for instance

Eric Rodriguez (Sep 10 2021 at 13:58):

https://leanprover-community.github.io/mathlib_docs/tactics.html#Instance%20cache%20tactics

Andrej Bauer (Sep 10 2021 at 13:59):

So if I have this right, the trick is to add I strategically in the right place.

Sebastien Gouezel (Sep 10 2021 at 14:00):

replacing your intros with introsI should do the trick.

Andrej Bauer (Sep 10 2021 at 14:01):

Uhm, unknown identifier 'resetI'. Are we talking Lean 3 or 4? I am on Lean 3.

Sebastien Gouezel (Sep 10 2021 at 14:02):

We're talking Lean 3. Are you using mathlib? Otherwise, there is a core version, but its syntax is less friendly.

Andrej Bauer (Sep 10 2021 at 14:03):

That's it, we're not using mathlib. Although we might as well. Thanks.

Sebastien Gouezel (Sep 10 2021 at 14:04):

Otherwise, you may try

unfreeze_local_instances,
freeze_local_instances,

Andrej Bauer (Sep 10 2021 at 14:08):

Actually, we are using mathlib. The machine sees tactic.unfreeze_local_instances but not unfreeze_local_instances, and knows nothing about introsI. Should I be import-ing something?

Sebastien Gouezel (Sep 10 2021 at 14:08):

import tactic, maybe?

Sebastien Gouezel (Sep 10 2021 at 14:09):

import tactic

instance decidable_precompose {α β : Type}
  (p : β  Prop) (f : α  β) [h : decidable_pred p] : decidable_pred (p  f) :=
by { intro, apply h }

def rabbit (α β : Type) (p : α  β  Prop) [h : decidable_pred p] : decidable_pred (p  sum.inl)
 :=
by apply_instance

def cow (α β : Type) :  (p : α  β  Prop) [h : decidable_pred p] , decidable_pred (p  sum.inl)
 :=
 begin
   introsI p h,
   apply_instance
 end

works for me

Kevin Buzzard (Sep 10 2021 at 14:09):

I think unfreeze_local_instances is not in the interactive tactic namespace, I've always written tactic.unfreeze_local_instances (until the I stuff came along)

Jannis Limperg (Sep 10 2021 at 15:52):

docs#tactic.interactive.unfreezingI is the preferred way to do unfreeze_local_instances ... freeze_local_instances. (This instance cache business is indeed very annoying. I believe Lean 4 thankfully dropped it.)


Last updated: Dec 20 2023 at 11:08 UTC