Nat and Int bitwise

Stream: general

[Shreyas Srinivas]

Hello all, I am porting heaplang from iris in Rocq to lean. Some of the binary operations there are bitwise operations on integers. For sound design reasons, iris-lean cannot depend on mathlib, which is there the Bitwise operations for Nat and Int reside. Is there a chance of these files getting upstreamed? These operations sound like they are basic enough to be in Std.

CC : Upstreaming experts @Kim Morrison ?

[Shreyas Srinivas]

more context here : #iris-lean > Heaplang @ 💬

[Markus Himmel]

Bitwise operations on Nat are already part of core; if there are specific lemmas you are missing we can add them.

The standard library team has previously discussed adding bitwise operations on Int, but we came to the conclusion that these are not important enough to warrant inclusion in the standard library. Of course, we do have bitwise operations on finite integers (Int64 etc. as well as BitVec).

[Shreyas Srinivas]

Currently we need bitwise operations for Int which seem to be defined here : https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Int/Bitwise.html#Int.bitwise_and

[Shreyas Srinivas]

The idea is that I would like the heaplang in iris-lean to be faithful to the version in Rocq

[Shreyas Srinivas]

and this file depends on Mathlib.Data.Nat.Bitwise

[Shreyas Srinivas]

and I am guessing upstreaming is not out of the question since the module docstring says "Possibly only of archaeological significance."

[Kim Morrison]

You could make a (perhaps temporary) lean-int-bitwise repository to contain these. I think they could happily be removed from Mathlib if they have another home.

[Eric Wieser]

These could presumably move to batteries instead?

[Shreyas Srinivas]

Kim Morrison said:

You could make a (perhaps temporary) lean-int-bitwise repository to contain these. I think they could happily be removed from Mathlib if they have another home.

The issue is, some of the bitwise stuff for Nat is already in Std as Markus says. So it might be easier to just upstream them at least to Batteries.