How to use type classes

Stream: general

[Andrej Bauer]

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]

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]

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

[Andrej Bauer]

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

[Andrej Bauer]

So what would be the idomatic way of proving cow?

[Sebastien Gouezel]

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

[Eric Rodriguez]

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

[Andrej Bauer]

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

[Sebastien Gouezel]

replacing your intros with introsI should do the trick.

[Andrej Bauer]

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

[Sebastien Gouezel]

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

[Andrej Bauer]

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

[Sebastien Gouezel]

Otherwise, you may try

unfreeze_local_instances,
freeze_local_instances,

[Andrej Bauer]

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]

import tactic, maybe?

[Sebastien Gouezel]

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]

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]

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