## Stream: new members

### Topic: Invoking instances explicitly

#### Jakob Scholbach (Mar 03 2021 at 22:26):

For some integral domain F, I have a hypothesis char_zero F. I would like to infer char_p F 0 using

instance char_p.of_char_zero (α : Type u) [semiring α] [char_zero α] : char_p α 0 :


If I write apply char_p.of_char_zero etc., it does not work. I guess this is because that fact is declared as an instance, not a lemma. How do I invoke this instance explicitly in order to gain a new hypothesis char_p F 0 in this case?

#### Eric Wieser (Mar 03 2021 at 22:28):

Can you give a #mwe?

#### Yakov Pechersky (Mar 03 2021 at 22:30):

Have you done

haveI : char_p F 0  := of_char_zero your_hypothesis,


#### Adam Topaz (Mar 03 2021 at 22:30):

import algebra.char_p.basic

example (α : Type*) [semiring α] [char_zero α] : char_p α 0 := by apply_instance


#### Adam Topaz (Mar 03 2021 at 22:31):

So the typeclass system will find the instance automatically.

#### Adam Topaz (Mar 03 2021 at 22:34):

Here's a little game you can play to see that this actually works inside a proof:

import algebra.char_p.basic

example (α : Type*) [semiring α] [char_zero α] : char_p α 0 := by apply_instance

def foo {α : Type*} [semiring α] [char_p α 0] : α := 0

lemma this_is_a_thing (α : Type*) [semiring α] [char_zero α] : true :=
begin
have := (foo : α),
sorry
end


#### Kevin Buzzard (Mar 03 2021 at 22:35):

The idea is that "the system" (the type class inference system) is supposed to deal with all the terms of type X if X is a so-called "class". It is doing this all the time -- if you write [ring R] and then want to use add_zero to prove r + 0 = r, for some r : R, Lean has a problem, because #check @add_zero shows this:

add_zero : ∀ {M : Type u_1} [_inst_1 : add_monoid M] (a : M), a + 0 = a


In other words, add_zero is a theorem which applies to all add_monoids. But R is a ring, which to Lean means that there is a term _inst_1 : ring R which is known to the type class system. However the type class system also knows that every ring is an add_monoid, as can be checked like this:

example (R : Type) [ring R] : add_monoid R := by apply_instance


so the lemma applies automatically, because the type class system does the job of finding the correct term of type add_monoid R which add_zero needs as an input.

example (R : Type) [ring R] (r : R) : r + 0 = r := add_zero r -- works!


#### Jakob Scholbach (Mar 03 2021 at 22:37):

@Eric Wieser :

import algebra.char_p.basic
import algebra.char_zero

lemma aux (F: Type) [integral_domain F] (hq : true ∧ char_zero F) : char_p F 0 :=
begin
have hyp : char_zero F := hq.2,
-- here I want to apply char_p.of_char_zero to hyp,
sorry
end


(I know the assumption hq with the true \and  is a bit stupid. If I remove the true \and  bit, then apply char_p.of_char_zero,precisely works, but if I generate the hypothesis hyp in the middle of the proof it won't work.

#### Adam Topaz (Mar 03 2021 at 22:40):

import algebra.char_p.basic
import algebra.char_zero

lemma aux (F: Type) [integral_domain F] (hq : true ∧ char_zero F) : char_p F 0 :=
begin
haveI := hq.2,
apply_instance
end


#### Adam Topaz (Mar 03 2021 at 22:40):

The fooI instances let you introduce instances to the typeclass system inside a tactic block.

#### Kevin Buzzard (Mar 03 2021 at 22:42):

char_zero is a class, but you didn't put it in square brackets before the colon, so the type class inference system ignored it. The usual way to get something into the system is square brackets before the colon, and haveI is a way to add things in the middle of a proof. Another useful one is resetI which adds all the instances of the classes which are hypotheses.

#### Kevin Buzzard (Mar 03 2021 at 22:43):

import algebra.char_p.basic
import algebra.char_zero

lemma aux (F: Type) [integral_domain F] (hq : true ∧ char_zero F) : char_p F 0 :=
begin
cases hq with h1 h2, -- now h2 : char_zero F is an assumption
resetI, -- now it's in the type class system
apply_instance -- works
end


#### Jakob Scholbach (Mar 03 2021 at 22:43):

OK, learned another thing -- thank you all!

#### Adam Topaz (Mar 03 2021 at 22:44):

The issue you originally faced was that [char_zero F] was a required instance in char_p.of_char_zero, and you didn't have that in context. If you want to do things fully explicitly, you can do something like this:

import algebra.char_p.basic
import algebra.char_zero

lemma aux (F: Type) [integral_domain F] (hq : true ∧ char_zero F) : char_p F 0 :=
begin
have claim := hq.2,
exact @char_p.of_char_zero F _ hq.2
end


#### Kevin Buzzard (Mar 03 2021 at 22:46):

Type class inference took me a long time to master. A lot of the examples in the docs are pretty non-mathematical. This is the reason I mentioned the ring example. Another example is notation: instance has_add X := ⟨foo⟩ makes x + y mean foo x y, because + is notation for has_add.add, and if you #check @has_add.add you'll see that it asks the type class inference system for a term of type has_add X, which the instance has put there.

#### Jakob Scholbach (Mar 03 2021 at 22:50):

@Kevin Buzzard : yes, if you are going to expand the Mathematics in Lean documentary, please do include such explanations.

#### Jakob Scholbach (Mar 03 2021 at 22:52):

I didn't know the haveI (nor resetI), and it also doesn't seem to be discussed in the Theorem Proving in Lean doc.

#### Kevin Buzzard (Mar 03 2021 at 22:53):

No, these things are well-kept secrets ;-) They are part of mathlib and were introduced after TPIL was written.

#### Adam Topaz (Mar 03 2021 at 22:53):

@Jakob Scholbach do you know about the tactic documentation here? https://leanprover-community.github.io/mathlib_docs/tactics.html

#### Kevin Buzzard (Mar 03 2021 at 22:54):

Just keep asking here if you are not sure about anything -- you see that four people had responded to your question within ten minutes of you asking.

#### Jakob Scholbach (Mar 03 2021 at 22:56):

Yes, I am grateful for all your immediate help -- absolutely stellar! Do you guys never sleep? :)
@Adam Topaz , I stumbled over it once, but didn't realize its importance yet. I will try to digest it then; thanks again.

#### Adam Topaz (Mar 03 2021 at 22:57):

Some of us are in the western hemisphere :) I don't know why all these people in Europe are still awake! :rofl:

#### Kevin Buzzard (Mar 03 2021 at 22:58):

I'm preparing my lecture on quotients in Lean for tomorrow!

#### Johan Commelin (Mar 04 2021 at 05:29):

I see that the problem is already solved, but @Jakob Scholbach how did you end up with hq : true ∧ char_zero F? Because that's not supposed to happen :wink: :smiley:

#### Patrick Massot (Mar 04 2021 at 07:49):

Kevin Buzzard said:

char_zero is a class, but you didn't put it in square brackets before the colon, so the type class inference system ignored it.

Technically this explanation is wrong. The kind of brackets you use in a def or statement matters only when using it.

import algebra.char_p.basic
import algebra.char_zero

lemma aux (F: Type) (hi : integral_domain F) (hq : char_zero F) : char_p F 0 :=
begin
apply_instance, -- works
end


The way Lean picks up instance assumptions when elaborating the part right of the colon (and what is in the system at the beginning of the proof) seems to be simply looping through the context and looking for type classes, but not looking inside inductive constructors like Jakob's and.

#### Kevin Buzzard (Mar 04 2021 at 08:04):

Aah yes, I've been confused by this before. Thanks!

#### Jakob Scholbach (Mar 04 2021 at 10:14):

@Johan Commelin : Yes, sure, this was a bit silly; this was just in order to have a minimal example. In the real situation I had a conjunction like p = 1 \and char_zero F, in the process of writing down some basic lemmas about the exponential characteristic.

#### Johan Commelin (Mar 04 2021 at 10:17):

Ok, understood. But whenever possible you should try to split such conjunctions into two separate hypotheses. Then you can feed [char_zero F] to TC.

Last updated: May 08 2021 at 19:11 UTC