has_zero in lean4?

Stream: lean4

[tangentstorm]

How do I refer to has_zero in lean4? Looking at https://github.com/leanprover/lean4/search?q=HasZero I see it's defined in src/library/constants.cpp, and i see an example in the equation compiler test:

instance : HasZero Term := ⟨ofInt 0⟩

... but I can't seem to get that syntax to work:

inductive Bin where -- binary string
| B            -- infinite stream of zeros (high bits)
| O (x: Bin)   -- multiply by 2
| I (x: Bin)   -- multiply by 2 and add 1
  deriving Repr

namespace Bin

instance : HasZero Bin := ⟨B⟩

Am i missing something? (Incidentally, equations.lean doesn't pass the syntax-check for me, either. As far as I can tell, I have lean version 4.0.0 installed, and it does say lean4 in the lower right corner of vscode)

[Kevin Buzzard]

Version 4.0.0 is very old. I would start by upgrading to the current nightly to see if this fixes things.

[Henrik Böving]

First things first as you can see by a simple search through the documentation: https://leanprover-community.github.io/mathlib4_docs/ HasZero doesn't exist, we have a class like this in mathlib4 however docs4#Zero but it is definitely not built in so whatever you are looking at in the compiler is certainly not what you are looking for.

Furthermore your thing does very much pass the syntax check it does not pass the elaboration however (in general you should post the actual error you are seeing so we aren't just left guessing what is wrong) with:

function expected at
  HasZero
term has type
  ?m.781

which is because HasZero doesn't exist so the auto implicit mechanism figured it should be an implicit variable but the elaboration procedure figure there shoul dbe a function at work here, you can see this by the fact that your editor highlighted HasZero in blue in my case:
image.png
as opposed to the black which is reserved for already existing declarations.

[tangentstorm]

ok. thanks. sorry for not posting the error. will figure out how to upgrade and try again.

[tangentstorm]

Well, after:

elan default leanprover/lean4:nightly

i now get pages and pages of this message in the console:

Lean (version 4.0.0-nightly-2022-06-26, commit 5a0c3b8d803a, Release)
elan 1.4.1 (6a7f30d8e 2022-04-15)
PANIC at List.getLast! Init.Data.List.BasicAux:63:13: empty list
PANIC at List.head! Init.Data.List.BasicAux:31:12: empty list
PANIC at Lean.EnvExtensionInterfaceUnsafe.getState Lean.Environment:236:4: invalid environment extension has been accessed
PANIC at Lean.ScopedEnvExtension.getState Lean.ScopedEnvExtension:157:16: unreachable code has been reached
PANIC at Lean.EnvExtensionInterfaceUnsafe.getState Lean.Environment:236:4: invalid environment extension has been accessed
Error: index out of bounds
PANIC at Lean.EnvExtensionInterfaceUnsafe.getState Lean.Environment:236:4: invalid environment extension has been accessed
PANIC at Lean.ScopedEnvExtension.getState Lean.ScopedEnvExtension:157:16: unreachable code has been reached
PANIC at Lean.EnvExtensionInterfaceUnsafe.getState Lean.Environment:236:4: invalid environment extension has been accessed
Error: index out of bounds

i don't suppose there's something between nightly and stable I could try?
(it does seem to respond to commands intelligently, despite the errors...)

[tangentstorm]

these instructions did not include any steps to install mathlib4... maybe there's more i need to do before i should expect this to work?
image.png

[Henrik Böving]

You can select each nightly individually in your lean-toolchain file once you've created a lake project, version leanprover/lean4:nightly-2022-06-24 doesn't have these errors.

Regarding the installation of mathlib4 you have to declare it as a dependency in your lakefile.lean. You can also get the effects of Zero that you are interested in by declaring an instance : OfNat Bin n where the ofNat field of that instance will contain the value of type Bin that corresponds to the natural number n.

[tangentstorm]

mathlib4 doesn't compile under 06-24 ... seems to need 06-25 (or at least the file in mathlib that fails to compile is Data/List/Basic.lean, and the last change to that file is the bump to 06-25)...

so for posterity: if lean4:nightly doesn't work, use the version from here:
https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain

[Henrik Böving]

Yes if you want to be 100% sure your project will work with the mathlib version use their compiler version but again you can achieve the notational part of Zero with just OfNat instances which are built-in, Zero is part of the algebraic hierarchy.

[tangentstorm]

docs4#OfNat

[tangentstorm]

so, i have succ, so i can define ofNat recursively:

def ofNat : (n:Nat) → Bin
| 0 => Bin.B
| Nat.succ i => succ (ofNat i)

instance : OfNat Bin n := ⟨ofNat n⟩

This compiles, and #eval ofNat 6 gives back Bin.O (Bin.I (Bin.I (Bin.B))), which is what i expect.

So I guess I have a basic working answer here. :)