Binary addition

Stream: new members

[Mr Proof]

With the help of ChatGPT, I made some code that adds with binary numbers:

/-         Binary Numbers  Addition         -/

inductive Binary where
| start : Binary
| one : Binary -> Binary
| zero : Binary -> Binary

def BIN:=Binary.start

def binaryRepr : Binary → String
| Binary.one x =>  binaryRepr x ++ "1"
| Binary.zero x => binaryRepr x ++ "0"
| Binary.start => "b"

-- Define the Repr instance using the helper function
instance : Repr Binary :=
  { reprPrec := fun q _ => binaryRepr q }


/- Function to handle addition with carry -/
def addWithCarry : Binary -> Binary -> Bool -> Binary
| Binary.start, Binary.start, false => Binary.start
| Binary.start, Binary.start, true  => Binary.one Binary.start
| Binary.start, Binary.zero b, false => Binary.zero b
| Binary.start, Binary.zero b, true  => Binary.one b
| Binary.start, Binary.one b, false => Binary.one b
| Binary.start, Binary.one b, true  => Binary.zero (addWithCarry Binary.start b true)
| Binary.zero a, Binary.start, false => Binary.zero a
| Binary.zero a, Binary.start, true  => Binary.one a
| Binary.zero a, Binary.zero b, false => Binary.zero (addWithCarry a b false)
| Binary.zero a, Binary.zero b, true  => Binary.one (addWithCarry a b false)
| Binary.zero a, Binary.one b, false => Binary.one (addWithCarry a b false)
| Binary.zero a, Binary.one b, true  => Binary.zero (addWithCarry a b true)
| Binary.one a, Binary.start, false => Binary.one a
| Binary.one a, Binary.start, true  => Binary.zero (addWithCarry a Binary.start true)
| Binary.one a, Binary.zero b, false => Binary.one (addWithCarry a b false)
| Binary.one a, Binary.zero b, true  => Binary.zero (addWithCarry a b true)
| Binary.one a, Binary.one b, false => Binary.zero (addWithCarry a b true)
| Binary.one a, Binary.one b, true  => Binary.one (addWithCarry a b true)

/- Main addition function using the helper function -/
def Binary.add (A B : Binary) : Binary :=
  addWithCarry A B false

instance : HAdd Binary Binary Binary where
  hAdd:= Binary.add

-- Testing the function

#eval  BIN.one.zero + BIN.one.one.one

#eval BIN.one.zero.one.zero.one + BIN.one

Not sure if something like this is already in the Mathlib? (I assume so otherwise how did ChatGPT know how to write it?) Also, not sure what the point of it is. :smile:Is this good code or bad? :thinking:Probably needs some proofs that it is equivalent to the Natural numbers

[Eric Wieser]

docs#Num is mathlib's binary number type

[Eric Wieser]

But realistically you should probably just use Nat and docs#Nat.binaryRec or docs#Nat.binaryRec'

[Mr Proof]

Is there any information about how Lean stores natural numbers. I assume a proof with a number like 12345 doesn't store it as SSSSSSSSSSSS.....SSSSSSSSSSO. Does it "cheat" a little by using things outside the minimal type theory?
Or does it store it in some kind of binary or decimal list with Lean rules for multiplication?

[Andrew Yang]

According to the docstring of docs#Nat,

This type is special-cased by both the kernel and the compiler:

• The type of expressions contains "Nat literals" as a primitive constructor,
  and the kernel knows how to reduce zero/succ expressions to nat literals.

• If implemented naively, this type would represent a numeral n in unary as a
  linked list with n links, which is horribly inefficient. Instead, the
  runtime itself has a special representation for Nat which stores numbers up
  to 2^63 directly and larger numbers use an arbitrary precision "bignum"
  library (usually GMP).

[Mr Proof]

Hmmm... kind of feels like cheating. :thinking:I'm sure a "bignum" API could be implemented directly in Lean. But I guess there's bigger fish to fry.

[Eric Wieser]

Lean3 used a binary representation where 12345 was represented as a series of nested docs#bit0 s and docs#bit1 s, but this turned out to perform worse and be more confusing to manipulate in the goal view

[Henrik Böving]

Mr Proof said:

Hmmm... kind of feels like cheating. :thinking:I'm sure a "bignum" API could be implemented directly in Lean. But I guess there's bigger fish to fry.

There is a series of Lean types that have special representation in the type theory and/or compiler, there isn't really something to be gained from making these things explicit in Lean and sometimes it's also just straight up impossible

[Mario Carneiro]

Well, one thing to be gained would be a smaller TCB. But lean has other priorities, and there are alternative ways to eliminate this from the TCB (although they are not likely in the near term)

[cairunze cairunze]

this video by Prof. Buzzard seems related.
https://www.youtube.com/watch?v=9f7WQkKd6x0