Instance not found

Stream: new members

[Pedro Minicz]

Lean isn't being able to find has_pow cardinal cardinal. I just updated Lean/mathlib. has_pow cardinal cardinal is defined as cardinal.has_pow.

import set_theory.cardinal

-- The following line gives an error: `cardinal.has_pow` already defined.
instance : has_pow cardinal cardinal := ⟨cardinal.power⟩

instance this_instance_is_ignored : has_pow cardinal cardinal := ⟨cardinal.power⟩

#check (by apply_instance : has_pow cardinal cardinal)

[Pedro Minicz]

I find this behavior pretty weird. I think it is kept unnoticed in set_theory/cardinal.lean because of the local notation (defined here):

local infixr ^ := @has_pow.pow cardinal cardinal cardinal.has_pow

[Reid Barton]

it's a universe issue

[Reid Barton]

universe u
#check (by apply_instance : has_pow cardinal.{u} cardinal.{u})   -- ok

[Pedro Minicz]

Indeed, thank you!

[Reid Barton]

the instance only applies when the universes are the same, but Lean doesn't know that that's the case you're interested in

[Pedro Minicz]

I see. Where can I read more about universes? Specifically, I would like to become more familiar with [...].{u}-like notations.

[Mario Carneiro]

They act like implicit arguments here

[Mario Carneiro]

the .{u} notation is how you specify them; usually it is .{_} and lean figures it out

[Mario Carneiro]

It's not completely obvious from #print what the order of universe arguments are, but you can just look for all free universe variables in the type of the definition

[Mario Carneiro]

if you #print cardinal you see def cardinal : Type (u+1) := so you know that cardinal takes one universe argument, labeled u in the original definition

[Reid Barton]

A comment about the purpose of that local notation certainly wouldn't hurt

[Mario Carneiro]

so cardinal.{0} : Type 1 and cardinal.{1} : Type 2 and so on

[Pedro Minicz]

Reid Barton said:

A comment about the purpose of that local notation certainly wouldn't hurt

Yes. The local notation is there to force the type of the digits (like 2 in ... ^ 2) being interpreted as cardinal instead of ℕ, from what I've gathered.

[Mario Carneiro]

if you #check cardinal you get cardinal : Type (u_1+1) because the universe is unspecified so once it unifies all metavariables and everything is still consistent, it just makes up variable names for everything else

[Mario Carneiro]

The local notation in cardinal is to solve exactly this universe issue

[Mario Carneiro]

although I think it was added after the fact, when has_pow first became a typeclass, so it has some flavor of a backward compatibility patch on the file