Stream: new members

Topic: Notation for numerals

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.

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
All Messages (3)
-/


Yakov Pechersky (Mar 12 2021 at 19:55):

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

I see, thanks!

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.

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


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.

Eric Wieser (Mar 12 2021 at 20:04):

If you define has_div too you can support decimals too

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)


Kevin Buzzard (Mar 12 2021 at 20:09):

Just remember not to #check (0 : X)

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)

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


Kevin Buzzard (Mar 12 2021 at 20:26):

Are you sure that's pure 5??

Yakov Pechersky (Mar 12 2021 at 20:27):

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

Yakov Pechersky (Mar 12 2021 at 20:27):

local notation 𝟢 := type.zero

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


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


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