Numbers

[dselsam]

The number-mismatch is more problematic than I realized at first. Lean3 uses zero, one, bit0 and bit1, whereas Lean4 uses OfNat α n. It is not trivial to auto-convert during the porting. I tried making OfNat instances from has_zero, has_one, and has_add, but I don't see a good way to support reasonably efficient kernel computation with it.

class HasZero (α : Type u) := (zero : α)
class HasOne  (α : Type u) := (one : α)

universes u
variable {α : Type u} [HasZero α] [HasOne α] [Add α]

def bit0 (x : α) : α := x + x
def bit1 (x : α) : α := bit0 x + HasOne.one

instance [HasOne α] : Inhabited α := ⟨HasOne.one⟩

def nat2bitsFuelAux (fuel n : Nat) : α :=
  match fuel with
  | 0        => arbitrary
  | fuel + 1 =>
    if n == 0 then arbitrary
    else if n == 1 then HasOne.one
    else if n % 2 == 1 then bit1 (nat2bitsFuelAux fuel (n / 2))
    else bit0 (nat2bitsFuelAux fuel (n / 2))

-- note: partial and wf don't compute in the kernel
def nat2bitsFuel (n : Nat) : α := nat2bitsFuelAux 10 n

-- even simple arithmetic will cause `nat2bitsFuelAux` to be unfolded until it runs out of fuel.
-- even with fuel=10 (which is not enough to port mathlib), the following is very slow:
example : (nat2bitsFuel 2 : α) + (nat2bitsFuel 2 : α) = nat2bitsFuel 4 := rfl

The auto-porter could construct concrete instances for concrete n, but it does not seem to be possible for typeclass resolution to do this in general after the port.

[dselsam]

Mario proposed the following: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/226330232. The proposal is fleshed out in the subsequent comments.

[dselsam]

Mario proposed the following: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/226330232. The proposal is fleshed out in the subsequent comments.

This proposal has been prototyped here: https://github.com/dselsam/lean4/tree/postinst

[dselsam]

Plan: simply wrap the bit0/bit1 numerals with ofNat during the port, and have new developments use the well-founded instance.

[dselsam]

Re-opening, as Yury points out that the plan above will still cause unfortunate issues: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport.3Anumbers/near/231540532