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