Zulip Chat Archive

Stream: maths

Topic: Use instances with local hypothesis


view this post on Zulip Filippo A. E. Nuccio (Mar 05 2021 at 13:22):

I am trying to understand how instances work and I ran across the following examples.

lemma one {S : Type*} (hs : integral_domain S) : comm_cancel_monoid_with_zero S := by apply_instance

is OK, while

lemma two {S : Type*} [ring S] (f :  ≃+* S) : comm_cancel_monoid_with_zero S :=
begin
  have hs : integral_domain S, sorry,
  apply_instance
end

is not OK (a part from the fact that I can prove hs using f, but I've sorried it to be short). So I understand that when Lean looks for assumptions that would match instances, it looks in the hypothesis of the statement, but not on "new" ones. Is it really so? If yes, I have two questions:
1) What is the difference between an "assumed" hypothesis and one which has been "constructed" along the way?
2) How to apply_instance if the needed assumption was not part of the hypothesis, as in my lemma two?

view this post on Zulip Riccardo Brasca (Mar 05 2021 at 13:25):

For question 2, haveIor letI makes hs an instance, meaning that the system then finds it like it was written [...] in the statement.

view this post on Zulip Kevin Buzzard (Mar 05 2021 at 13:25):

The "system" which makes apply_instance work is called the type class inference system. It is initialised at the beginning of a proof in the following way: Lean looks at everything before the colon which is a term of a typeclass (like your first hs) and puts it into the system. Then, by default, it never puts anything else into the system.

To make your lemma 2 work you need to put haveI : integral_domain S (or probably letI : integral_domain S because I think it's data) -- this tactic specifically is designed to change the system.

view this post on Zulip Filippo A. E. Nuccio (Mar 05 2021 at 13:26):

Wow, perfect! Thanks (indeed, it works): the nice caveat is that it does not accept my sorry, the docs says

The syntax is the same as have, but the proof-omitted version is not supported. For this one must write have : t, { <proof> }, resetI, <proof>.

view this post on Zulip Kevin Buzzard (Mar 05 2021 at 13:27):

Note that, as Patrick reminded us yesterday (and Mario told me about a year ago), you don't need hs to be in square brackets in lemma 1 -- Lean just looks at everything before the colon. The reason you should put [integral_domain S] in square brackets instead is for people who want to use your lemma, not to help you prove it yourself.

view this post on Zulip Filippo A. E. Nuccio (Mar 05 2021 at 13:28):

Meaning it could be in curly ones? (You can also simply point at Patrick's chat)

view this post on Zulip Kevin Buzzard (Mar 05 2021 at 19:40):

Yes, any terms of type C where C is in a class, if they're defined before the colon, will end up in the instance cache. It doesn't matter what brackets are being used, I believe...


Last updated: May 14 2021 at 18:28 UTC