Zulip Chat Archive

Stream: new members

Topic: Notation for numerals


view this post on Zulip Horatiu Cheval (Mar 12 2021 at 19:53):

Is there a notational typeclass that enables me to use numeral notation 0, 1, 2, ... for a custom type? I only know about has_zero but that only deals with the symbol 0.

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 19:53):

You also need has_one and has_add, and Lean will take it from there.

constant X : Type

#check (37 : X)
/-
failed to synthesize type class instance for
⊢ has_one X
scratch2.lean:3:8
failed to synthesize type class instance for
⊢ has_add X
All Messages (3)
-/

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 19:55):

And numerals to make true sense, I really hope addition in your type is associative.

view this post on Zulip Horatiu Cheval (Mar 12 2021 at 19:57):

I see, thanks!

view this post on Zulip Horatiu Cheval (Mar 12 2021 at 20:01):

I actually didn't intend to have an addition for this, I only want some particular terms denoted by 0, 1, 2, ..., (I only have a meaningful successor notion, for some subset of terms), so not every term is equal to a numeral in this sense.

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 20:01):

def foo : has_add  := λ x y, x + y + y + 37

attribute [instance, priority 100000] foo

#reduce 2 -- 40
#reduce 40 -- 5773

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 20:02):

well each term is encoded in binary, so you need to make sure that 2 = 1 + 1 for your definition of 1 and add, etc. You might be better off defining zero, one, two :-) Most types (like the reals) have the property that numerals work but not every terms is equal to a numeral.

view this post on Zulip Eric Wieser (Mar 12 2021 at 20:04):

If you define has_div too you can support decimals too

view this post on Zulip Eric Wieser (Mar 12 2021 at 20:05):

Hey, lean has binary!

variables (X : Type) [has_add X] [has_div X] [has_one X]
#check (0b10100 : X)
#check (0xFF : X)
#check (2.5 : X)

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 20:09):

Just remember not to #check (0 : X)

view this post on Zulip Horatiu Cheval (Mar 12 2021 at 20:22):

Ok, thank you all for the insights! Now after playing a little I realized the initial question wasn't really the best suited for my case. So, I have this:

inductive type
| zero : type
| arrow : type  type  type

infixr `↣` : 50 := type.arrow

def pure :   type
| 0 := type.zero
| (n + 1) := type.zero  pure n

Can I, for an n : ℕ, simply write n to mean pure n in a place where a type is expected? (I realize it's kind of pointless here, but still, out of curiosity)

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:25):

inductive type
| zero : type
| arrow : type  type  type

infixr `↣` : 50 := type.arrow

def pure :   type
| 0 := type.zero
| (n + 1) := type.zero  pure n

instance : has_zero type := pure 0
instance : has_one type := pure 1
instance : has_add type := type.arrow

example : type := 5

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 20:26):

Are you sure that's pure 5??

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:27):

Ah, you're right, it's not.

view this post on Zulip Yakov Pechersky (Mar 12 2021 at 20:27):

local notation `𝟢` := type.zero

#reduce (5 : type) -- (((𝟢↣𝟢)↣𝟢↣𝟢)↣(𝟢↣𝟢)↣𝟢↣𝟢)↣𝟢↣𝟢
#reduce _root_.pure 5 -- 𝟢↣𝟢↣𝟢↣𝟢↣𝟢↣𝟢

view this post on Zulip Mario Carneiro (Mar 12 2021 at 20:37):

def type.append : type  type  type
| type.zero t := t
| (t1  t2) t := t1  t2.append t
instance : has_add type := type.append

example : 5 = _root_.pure 5 := rfl

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 20:59):

Oh nice, I couldn't figure it out :-)


Last updated: May 13 2021 at 05:21 UTC