Zulip Chat Archive

Stream: lean4

Topic: OfNat instance not found


Adam Topaz (Feb 16 2022 at 13:09):

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 (Feb 16 2022 at 13:09):

You need to write OfNat α (nat_lit 1).

Adam Topaz (Feb 16 2022 at 13:10):

Ah ok, thanks

Gabriel Ebner (Feb 16 2022 at 13:11):

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 (Feb 16 2022 at 13:18):

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

Julian Berman (Feb 16 2022 at 13:44):

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 (Feb 16 2022 at 13:46):

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 (Feb 16 2022 at 13:46):

maybe we should make a of_nat macro for this

Julian Berman (Feb 16 2022 at 13:46):

Ahhh, ok that sort of makes sense, thanks!

Gabriel Ebner (Feb 16 2022 at 13:47):

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

Adam Topaz (Feb 16 2022 at 13:49):

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 00 and 11 ;)

Reid Barton (Feb 16 2022 at 14:09):

Who needs other numbers? :robot:

Gabriel Ebner (Feb 16 2022 at 14:10):

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

Kevin Buzzard (Feb 16 2022 at 14:52):

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

Mac (Feb 26 2022 at 22:36):

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


Last updated: Dec 20 2023 at 11:08 UTC