Invoking instances explicitly

Stream: new members

[Jakob Scholbach]

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]

Can you give a #mwe?

[Yakov Pechersky]

Have you done

haveI : char_p F 0  := of_char_zero your_hypothesis,

[Adam Topaz]

import algebra.char_p.basic

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

[Adam Topaz]

So the typeclass system will find the instance automatically.

[Adam Topaz]

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]

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]

@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]

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]

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

[Kevin Buzzard]

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]

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]

OK, learned another thing -- thank you all!

[Adam Topaz]

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]

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]

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

[Jakob Scholbach]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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]

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

[Jakob Scholbach]

@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]

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.