bit0 deprecated

Stream: mathlib4

[Jireh Loreaux]

Lean 4 tells me docs4#bit0 has been deprecated. What should I use in it's place?

[Jireh Loreaux]

Actually, it would be really nice if this information were included in the warning itself.

[Alex J. Best]

There's no direct replacement, the way numerals work has been changed completely and uses docs4#OfNat rather than nested bit0 and bit1's applied to zero. So most likely those lemmas can be left unported

[Alex J. Best]

I don't know whether its better to just port it to the deprecated statement for now or leave it out completely

[Jireh Loreaux]

Well, this is how docs#cast_pos_num is implemented, so that the very least I think I would need a new way to cast to a Nat.

[Mario Carneiro]

You can just use 2 * n and 2 * n + 1

[Mario Carneiro]

or n <<< 1 and n <<< 1 ||| 1 if you want to do it CS style

[Jireh Loreaux]

Can the @[deprecated] attribute take an optional string with extra details about the deprecation (e.g, "use X instead" or "there is no replacement")

[Mario Carneiro]

that is what the identifier is intended to be

[Mario Carneiro]

@[deprecated foo] means "use foo instead"

[Mario Carneiro]

but I agree it would make sense to have a string literal version as well

[Jireh Loreaux]

Sorry, I misspoke earlier, I need a new way to cast (from pos_num) to any type α with a 1 and +, I'm not casting to a Nat here. So the 2 * doesn't work.

[Mario Carneiro]

that's a + a and a + a + 1, like bit0 and bit1 are implemented

[Jireh Loreaux]

well, sure, but then shouldn't I just use bit0 and bit1? Or is the point that I should roll it manually because they are deprecated?

[Mario Carneiro]

Alternatively, you could say that this whole function is deprecated, and then use bit0 and bit1 despite the deprecation warning

[Mario Carneiro]

The point of the warning is to alert people to the fact that numeral representation has changed and bit0/bit1 have gone from a central part of how numbers work to a weird way to double a number which might be occasionally useful

[Mario Carneiro]

if we still need the functions for those other purposes when all is said and done I think it's okay to undeprecate it

[Jireh Loreaux]

So is our feeling that this issue doesn't really apply to data.num.basic because this was already a fringe representation?

[Mario Carneiro]

yeah, num itself is deprecated

[Mario Carneiro]

It existed to facilitate more efficient kernel computation of nat arithmetic, but this is no longer necessary in lean 4 because Nat.add is overridden in the kernel to use GMP or bignums

[Mario Carneiro]

I think it's still useful if you want to make use of the inductive presentation of numbers provided by pos_num (especially if you are using it for purposes other than numbers like indexing into a binary tree), but it is even more fringe than it used to be

[Joseph Myers]

I think the real question here is the Lean 4 way of implementing whatever simplification of expressions involving numerals the bit0 and bit1 lemmas were intended to enable (if marked as simp lemmas). For a complicated case see the series of lemmas in data.fin.vec_notation, tests in test/matrix.lean such as the following

example {a b c d e f g h : α} : ![a, b, c, d, e, f, g, h] 5 = f := by simp
example {a b c d e f g h : α} : ![a, b, c, d, e, f, g, h] 7 = h := by simp
example {a b c d e f g h : α} : ![a, b, c, d, e, f, g, h] 37 = f := by simp
example {a b c d e f g h : α} : ![a, b, c, d, e, f, g, h] 99 = d := by simp

(where any individual case is also true by rfl, but having simp handle them is definitely convenient as part of a larger expression). But there are surely plenty of simpler cases of such lemmas as well (which may not all have testcases present). E.g. neg_pow_bit0 and neg_pow_bit1 in algebra.group_power.ring are probably intended for simplifying powers with a numeral as the exponent.

[Mario Carneiro]

This sort of thing is handled by unification hints (yes those!) for problems of the form ?a + k = n where k and n are literals

[Mario Carneiro]

so you should be able to add a simp lemma for decomposing the head and tail of a vector and it will prove those lemmas

[Yury G. Kudryashov]

Is it possible to write a lemma that simplifies (-a) ^ n to a ^ n if n is an even numeral literal?

[Yury G. Kudryashov]

In Lean 3, it was docs#neg_pow_bit0

[Yury G. Kudryashov]

If not, what is the right translation of this lemma to Lean 4? Something involving norm_num? If yes, then how?

[Yury G. Kudryashov]

@Mario Carneiro :up:

[Mario Carneiro]

No, I don't think this works anymore

[Mario Carneiro]

it is possible we could get 2 * ?n =?= 10 to unify to ?n =?= 5 and then use a simp lemma for this

[Yury G. Kudryashov]

Can we simplify even/odd on Nat? If yes, then we can have lemmas assuming Even n/Odd n.

[Mario Carneiro]

ah, yes that might actually work, since Even 10 can be proved by simp (config := {decide := true})

[Yury G. Kudryashov]

Is decide := true the default setting now?

[Yury G. Kudryashov]

I see that

example : ¬Even 25394535 := by simp only

works (once we have a DecidablePred).

[Reid Barton]

I guess this works in reasonable time because of special Nat support in the kernel?

[Heather Macbeth]

Yury G. Kudryashov said:

Is decide := true the default setting now?

Yes, although there is some debate about whether this should be kept in mathlib:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.20only.60.20does.20decidable.20checks.3F

[Yury G. Kudryashov]

Reid Barton said:

I guess this works in reasonable time because of special Nat support in the kernel?

This is my guess too.

[Violeta Hernández]

On this note. What's the deal with bitwise functions in Mathlib 4?

[Violeta Hernández]

The file Data/Nat/Bitwise says it's "possibly only of archeological significance"

[Violeta Hernández]

I just finished proving that the binary addition of numbers has the expected digits and it's really disappointing if this has no place in Mathlib

[Mario Carneiro]

We certainly want bitwise operations and types, but the implementation in lean 3 is unlikely to be the final word

[Mario Carneiro]

Also it is most likely to end up in std, not mathlib

[Mario Carneiro]

I don't see this "possibly only of archeological significance" quote in mathlib4

[Mario Carneiro]

Basically bitwise stuff needs a redesign for lean 4 and no one has had the time to do it

[Eric Wieser]

Isn't the idea that bit0 and bit1 are useless, but docs4#Nat.bit isn't?

[Mario Carneiro]

that too. My impression was that Violeta was talking about bitwise operators more generally

[Violeta Hernández]

Violeta Hernández said:

The file Data/Nat/Bitwise says it's "possibly only of archeological significance"

My bad, it's Init/Data/Int/Bitwise

[Violeta Hernández]

Eric Wieser said:

Isn't the idea that bit0 and bit1 are useless, but docs4#Nat.bit isn't?

This seems like a contradiction

[Violeta Hernández]

I'm not a big fan of just replacing bit0 and bit1 by 2 * x and 2 * x + 1

[Violeta Hernández]

For one, it runs into the problem of "there's more than one obvious way to write it down", the other of course being x + x, x + x + 1

[Violeta Hernández]

And also, even though it's very natural to chain these as bit0 (bit1 x), etc, it's much less natural to chain 2 * (2 * x + 1)

[Violeta Hernández]

One may be tempted to simplify as 4 * x + 2, but then we lose the ability to apply any bit0 lemmas

[Violeta Hernández]

I understand if bit0 and bit1 are no longer relevant to the Lean kernel but I believe they're still quite nice to have for bitwise operations

[Mario Carneiro]

Violeta Hernández said:

And also, even though it's very natural to chain these as bit0 (bit1 x), etc, it's much less natural to chain 2 * (2 * x + 1)

The point is that we are actively discouraging chains of bit0 / bit1 as a way to write numerals

[Mario Carneiro]

that is of course the reason they are named that way

[Mario Carneiro]

If you are nesting bitN functions you are probably doing it wrong, and with one layer it's just 2 * x and 2 * x + 1 which is a lot more mathematically familiar and allows the use of the usual ring theorems

[Mario Carneiro]

But again, there is some necessary design work to figure out how to do this all cleanly, and the result of said design work may in the end be to use bit0/bit1. It's hard to say at this point whether we will want it long term or switch to something else, and the main point of the discouraged tag on the functions is to extricate them from being load bearing parts of mathlib so that we can make design changes more easily

[Violeta Hernández]

Mario Carneiro said:

If you are nesting bitN functions you are probably doing it wrong, and with one layer it's just 2 * x and 2 * x + 1 which is a lot more mathematically familiar and allows the use of the usual ring theorems

Some auxiliary results in the addition theorem used bit0 (bit 1 x) and similar, so I wouldn't be so sure

[Wrenna Robson]

Just want to say that I agree with Violeta that having bit0 and bit1 is quite nice for bitwise-op reasons.

[Wrenna Robson]

I think one can use shiftl' though probably?

[Eric Wieser]

Can you use docs#Nat.bit ?

[Wrenna Robson]

Also works I suppose. Though that does use bit1 and bit0, which are meant to be deprecated...

[Eric Wieser]

Sure, but that's an implementation detail