What does "apply_instance" do?

Stream: general

[Bernd Losert]

I'm looking at https://leanprover-community.github.io/mathlib_docs/order/filter/ultrafilter.html#ultrafilter.unique and it has an argument (hne : g.ne_bot . "apply_instance"). What exactly is this doing?

[Eric Wieser]

tactic#apply_instance

[Adam Topaz]

it will try to apply the tactic apply_instance if you dont provide a term for that variable.

[Eric Wieser]

But I suspect your question is actually "what does some_type . "some_tactic" mean", which is syntax for docs#auto_param

[Bernd Losert]

So if I don't supply the theorem a hne, it's going to try to get one via instance search?

[Adam Topaz]

yep

[Bernd Losert]

I see.

[Adam Topaz]

auto_params are heavily used in the category theory library with the tactic obviously (which is essentially tidy) to automatically prove that simple diagrams commute. It's very useful.

[Bernd Losert]

I think I've seen it used to supply some default proofs that the composition in a category is associative and that the identity works as expected.

[Bernd Losert]

Yep: (f ≫ g) ≫ h = f ≫ g ≫ h) . "obviously"

[Adam Topaz]

right, so if you omit that field, then lean will try to use prove associativity by itself using the tactic obviously

[Bernd Losert]

Yeah, that's pretty cool.

[Eric Wieser]

(hne : g.ne_bot . "apply_instance") is particularly unusual though since [hne : g.ne_bot] means almost the same thing