-0

Stream: new members

[Alex Zhang]

theorem test : (-0:ℕ) = 0 :=sorrygives me the error message: failed to synthesize type class instance for ⊢ has_neg ℕ. What does the error message mean? Does has_neg just mean -? (hovering over the error message does not give me any additional info)

[Mario Carneiro]

yes

[Mario Carneiro]

the natural numbers don't have a negation

[Kevin Buzzard]

The error message means that you wrote $-0$, Lean unfolded the notation and decided that you must be using a map neg : nat -> nat and then it looked in its database (the type class inference system) and (unsurprisingly) found no such map.

[Damiano Testa]

I was also confused by something similar: the natural number do not have neg, but they do have sub.

[Mario Carneiro]

We could define such a function, but it would be very useless since -x = 0

[Damiano Testa]

So, while what you wrote does not work this does:

#check (0 - 0)
-- 0 - 0 : ℕ

[Kevin Buzzard]

@Alex Zhang has_neg is a "notational typeclass", the simplest kind of typeclass. If you have any random term a of any type X, and you write -a, then Lean tries to find a so-called "instance" of has_neg X, which in practice means that it looks through all the stuff which has been imported and sees if anyone has defined a map neg : X -> X and told this map to the system using the instance command. You can read about classes and instances in chapter 10 of #tpil

[Kevin Buzzard]

The reason for this is the following two lines right at the beginning of core Lean 3:

class has_neg      (α : Type u) := (neg : α → α)
prefix -       := has_neg.neg

The first line makes the has_neg class, the second line attaches the notation $-$ to the class.

[Kevin Buzzard]

def X := ℕ

def X.neg : X → X := λ x, (37 : ℕ)

instance : has_neg X :=
{ neg := X.neg }

variable (x : X)

#check -x -- works

[Kevin Buzzard]

If you remove the instance line you'll get the same error as the one you were facing with nat.