# Zulip Chat Archive

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

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