OfNat instance not found

Stream: lean4

[Adam Topaz]

I'm a little puzzled about the following code:

class HasOne (α : Type u) extends OfNat α 1

structure Foo (α : Type u) [HasOne α] :=
(a : α)
(h : a = 1) -- failed to synthesize instance OfNat α 1


class HasTwo (α : Type u) extends OfNat α 2

structure Bar (α : Type u) [HasTwo α] :=
(a : α)
(h : a = 2) -- failed to synthesize instance OfNat α 2

Why is lean having a hard time finding the OfNat instances at the lines with the comments?

[Gabriel Ebner]

You need to write OfNat α (nat_lit 1).

[Adam Topaz]

Ah ok, thanks

[Gabriel Ebner]

Also note that with these definitions you can't do extends HasOne α, HasTwo α. For this inheritence to work, the HasOne and HasTwo classes need to have one and two fields, resp:

class HasOne (α : Type u) where
  one : α

instance [HasOne α] : OfNat α (nat_lit 1) where
  ofNat := HasOne.one

[Adam Topaz]

I see. Thanks. I think I'll take a look at how things are set up in Mathlib4

[Julian Berman]

Gabriel Ebner said:

You need to write OfNat α (nat_lit 1).

I have made this mistake a few times myself too (forgetting nat_lit) -- what does it actually do when you leave it out?

[Gabriel Ebner]

It produces the term @OfNat α (@OfNat.ofNat Nat (nat_lit 1) _), which won't match @OfNat α (nat_lit 1) (which Lean searches for when you type 1).

[Mario Carneiro]

maybe we should make a of_nat macro for this

[Julian Berman]

Ahhh, ok that sort of makes sense, thanks!

[Gabriel Ebner]

I don't think we'll have many OfNat instances, so the utility of of_nat would be quite limited.

[Adam Topaz]

Mathlib4 already has such a macro:
https://github.com/leanprover-community/mathlib4/blob/9ea62cd8be727e9a01506729d72eece6fb38dc6d/Mathlib/Algebra/Group/Defs.lean#L9

It seems that it's only used for $0$ and $1$ ;)

[Reid Barton]

Who needs other numbers? :robot:

[Gabriel Ebner]

Are there situations where you want a 2, but (0+1)+1 doesn't work?

[Kevin Buzzard]

In maths (0+1)+1 would work fine for 2 :-)

[Mac]

I guess that one thing that CS and mathematics can agree is the only relevant digits are 0 and 1. Binary is king! XD