Defining my own numerals

Stream: lean4

[Brandon Brown]

I've defined my own nat type in the usual way:

inductive nat where
  | zero : nat
  | succ : nat → nat

And I want to somehow represent the repeated function composition e.g. nat.succ (nat.succ (nat.zero)) as a unary numeral system like 11111 (or some other arbitrary unicode character). How could I go about doing this in Lean4? Eventually I'd like to map this into a binary system again with my own non-standard numerals.

[Mario Carneiro]

You could make 1 or its unicode replacement a prefix operator, although you would need a 0 at the end to finish it off

[Brandon Brown]

That's clever, thanks. It's definitely more pleasant to look at that nat.succ. Is there a way to similarly map a custom notation to a term too like the infix/prefix command does for functions?

[Brandon Brown]

I can just define a new term like def c := nat.zero but it doesn't let me use arbitrary unicode, and it doesn't show up in the result of #reduce

[Brandon Brown]

Figured it out from looking at the Lean4 "lean4/src/Init/Notation.lean": I can use this notation:max "₀" => nat.zero

[Brandon Brown]

Although if I want to use the regular 0 numeral the default implementation cannot be overridden by setting the priority notation:max (priority := high) "0" => nat.zero
error: failed to synthesize instance OfNat nat 0

[Mario Carneiro]

I don't think you have to override the syntax for 0 if you just want to use 0; just implement OfNat nat 0

[Daniel Selsam]

This isn't pretty but here is one approach:

inductive nat where
  | zero : nat
  | succ : nat → nat

prefix "I|" => nat.succ
instance : OfNat nat (nat_lit 0) := ⟨nat.zero⟩

example : nat.succ (nat.succ (nat.succ nat.zero)) = I|I|I|0 := rfl

You might need to write a custom parser to support notation like m111 for 3, similar to the builtin parser for hex.

[Mario Carneiro]

if you use a non-identifier token it should be lexed as a sequence even if there are no spaces

[Mario Carneiro]

prefix "🅂" => nat.succ
instance : OfNat nat (nat_lit 0) := ⟨nat.zero⟩

example : nat.succ (nat.succ (nat.succ nat.zero)) = 🅂🅂🅂0 := rfl

[Mario Carneiro]

in lean 3 there was the ability to declare an identifier sequence as a token even if it is alphanumeric, using the precedence command. Does this still exist in lean 4?

[Mario Carneiro]

actually I take it back, you still need spaces around identifier tokens (except #print for some reason)

#printnat
-- inductive nat : Type
-- constructors:
-- nat.zero : nat
-- nat.succ : nat → nat

[Brandon Brown]

Thanks both.

local notation:max "z" => nat.zero
local prefix:max "s" => nat.succ
#reduce (s s s z) + (s s z) -- s s s s s z

Is fine for now until I figure out how to build a custom parser, which I may never do realistically hah

[Brandon Brown]

This also helps at least with printing.

def nat2str : nat → String :=
  fun
  | nat.zero => ""
  | nat.succ a => "1" ++ nat2str a

#eval nat2str (s s s z) -- "111"

instance : ToString nat where
  toString : nat → String := nat2str

#eval (s s s z) + (s s z) -- 11111

[François G. Dorais]

A slightly different variant:

instance : OfNat nat (nat_lit 0) := ⟨zero⟩

postfix:max "⁺" => succ

#reduce (succ (succ (succ zero))) -- zero⁺⁺⁺

instance : Repr nat :=
  let rec repr : nat → String
  | zero => "0"
  | succ n => repr n ++ "⁺"
  ⟨fun n _ => repr n⟩

#eval (succ (succ (succ zero))) -- 0⁺⁺⁺

def add : nat → nat → nat
| x, 0 => x
| x, y⁺ => (add x y)⁺

instance : Add nat := ⟨add⟩

example : 0⁺⁺⁺ + 0⁺⁺ = 0⁺⁺⁺⁺⁺ := rfl

[Sebastian Ullrich]

notation:max "🍎" => succ zero
prefix:max "🍎"   => succ

example : 🍎🍎🍎 + 🍎🍎 = 🍎🍎🍎🍎🍎 := rfl

[Kevin Buzzard]

I'm so adding this to my school talks