Zulip Chat Archive

Stream: new members

Topic: Invoking instances explicitly


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:28):

Can you give a #mwe?

view this post on Zulip Yakov Pechersky (Mar 03 2021 at 22:30):

Have you done

haveI : char_p F 0  := of_char_zero your_hypothesis,

view this post on Zulip Adam Topaz (Mar 03 2021 at 22:30):

import algebra.char_p.basic

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

view this post on Zulip Adam Topaz (Mar 03 2021 at 22:31):

So the typeclass system will find the instance automatically.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 03 2021 at 22:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jakob Scholbach (Mar 03 2021 at 22:43):

OK, learned another thing -- thank you all!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Mar 03 2021 at 22:58):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 04 2021 at 08:04):

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

view this post on Zulip 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.

view this post on Zulip 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