Questions on inferInstance

Stream: new members

[Kevin Cheung]

I have been working through the chapter on Type Claases in Theorem Proving in Lean 4 and had some trouble understanding inferInstance. I have a couple of questions.

Question 1.
In the following

#print inferInstance

@[reducible] def inferInstance.{u} : {α : Sort u} → [i : α] → α :=
fun {α} [i : α] => i

how should one interpret [i : α]? My understanding (probably faulty) is that it is related to type class but I don't quite understand this syntax, especially when it appears in the anoynmous function fun {α} [i : α] => i. I suppose that it is not an argument here, is that correct?

Question 2.
In what situations does one need inferInstance? I couldn't quite tell from the example in the book the intuition/motivation.

Any help or pointers greatly appreciated.

[Kevin Buzzard]

An input [a : T] in a theorem means "let the square bracket machine supply this input". The code variable (G : Type) [group G] means "let G be a type, and put the fact that G is a group into the square bracket machine", and now all theorems which require G to be a group are now available to you, as well as all theorems which require G to be e.g. a monoid or a semigroup, because the square bracket machine knows that a group is a monoid.

The square bracket machine is called the typeclass inference system, and it can be though of as a big database of standard facts (e.g. the reals are a field, the rationals are ordered, the integers are a group...) which can be added to with [...] assumptions.

The definition of inferInstance means that the code example : Field \R := inferInstance should compile, because the square bracket machine has to fill in the input [i : Field \R] but this instance is in mathlib, so the machine finds i and then returns i.

[Kevin Cheung]

I think I am getting it. Now, in the following

#check (@inferInstance Nat)

@inferInstance Nat : [i : Nat] → Nat

how does Lean treat [i : Nat]? (I guess one shouldn't be passing Nat to @inferInstance but I am just curious about what's going on here.)

[Matthew Ballard]

You only get access to [i : A] if your type is a class. Nat isn’t a class. Classes should be types where it is reasonable for Lean to fill the data from some “canonical” choice when your types are concrete.

[Kevin Buzzard]

how does Lean treat [i : Nat]?

#synth Nat -- type class instance expected
           --   ℕ

The square bracket system failed.

[Kevin Cheung]

Matthew Ballard said:

You only get access to [i : A] if your type is a class. Nat isn’t a class. Classes should be types where it is reasonable for Lean to fill the data from some “canonical” choice when your types are concrete.

I am not sure I completely understood the last sentence. Did what it say explains why the following doesn't lead to an error?

#eval (@inferInstance Nat 6)
6

[Kyle Miller]

Using @ and filling in the second argument is getting Lean to skip the checks that Nat is a typeclass. If you do #eval (inferInstance : Nat) you'll get "type class instance expected"

[Kyle Miller]

Here's another way to trick it: #eval inferInstance (i := 6). This is using that i is the name of the instance argument to inferInstance

[Kyle Miller]

I believe the check only happens if Lean is responsible for filling in an instance argument.

[Kyle Miller]

Lean isn't complaining with your example because Lean is taking your word for it that Nat is a typeclass

[Kevin Cheung]

Thanks for all the responses. They have been very helpful understanding the magic that Lean does.

[Kevin Cheung]

One last newbie question (for now). When one specifies a type hole _, how does one ask Lean to show the result of unification? (That is, what Lean fills it with?)

[Kyle Miller]

for Q2: usually inferInstance is unnecessary. I think pointing out is mostly to show you how you can query the instance database