Equality of integers

Stream: general

[Kind Bubble]

I am working with arrays of natural numbers and arrays of arrays of natural numbers. I was hoping to get a few of the basics... is there a table involving the names of the various properties of the integers?

I don't know very much about how this is handled, but I would imagine there is something to say about speed of testing equality here. Choose a base C for the decimal expansion of n : Nat and suppose that there is f : Nat -> Nat sending all but finitely many natural numbers to 0 such that n = sum f(i) C^i

There is a function m : Nat -> Nat sending n = sum f(i) C^i to max {n : f(i) isn't 0}. Say we make a table e : {0, ..., C} x {0, ..., C} -> Prop with t(C) time to look-up. Then knowledge of f above gives that = is O(m), m = m(f).

For some reason I thought there would be something better than this on first instinct, maybe something amortized constant time, O(1)+?

[Kind Bubble]

Definitional equality is maybe related to the O(term-length) complexity class.

[Eric Wieser]

What do you mean by "testing" equality? Do you mean in the sense of the VM:

#eval to_bool (1 + 1 = 2)

or the kernel:

example : 1 + 1 = 2 := rfl

[Kyle Miller]

Are you writing programs (in Lean 3? or in Lean 4?) or are you proving things about arrays of natural numbers?

[Kind Bubble]

This is Lean 4.

The test is the mentioned algorithm whose complexity time is O(m). This test is a function from binary representations whose length is recorded separately to 2. Here's something closer to Lean code:

def X := {(f : Nat -> {1, ..., C}, d = d(f) in N) // d = max(i :N , f(i) = 0) }
def toNat (x : X) := sum_over_N x.fst(i)
def Equality : X x X -> 2 ...

[Kind Bubble]

Oh, and I'm writing programs. Actually is there a turing machine library?

[Eric Wieser]

Can you make a #mwe (and once you have one, follow the instructions at #backticks to post it)? What you have isn't a #mwe because it doesn't include the definition of sum_over_N

[Kyle Miller]

Lean 4 uses libgmp to represent it's Nat type internally. That library stores numbers in base $2^{32}$ or base $2^{64}$ I believe (they call each digit in this representation a "limb"). I'm not sure I understand what you're asking exactly, but maybe this helps.

[Kyle Miller]

One resource for what exists in Lean 4 and mathlib4 is the mathlib4 documentation. Here's a link to the documentation for Nat itself, but there are lemmas about Nat throughout the library. docs4#Nat