nat.bit / nat.binary_rec

Stream: mathlib4

[Ruben Van de Velde]

data.nat.basic (mathlib4#729) uses nat.bit and nat.binary_rec which depend on bit0/bit1, which are deprecated. Thoughts?

[Yaël Dillies]

The consensus is that we could reintroduce them. They are just less central as before.

[Ruben Van de Velde]

The annoying bit (ahem) is that they exist but give deprecation warnings

[Jireh Loreaux]

I have encountered (two?) places that used nat.binary_rec and in each place I have just reimplemented it from scratch. See for intance Data.Num.Basic.

[Jireh Loreaux]

For things which explicitly use bit0 and bit1, I have been marking those declarations as deprecated but turning off the deprecation linter for those declarations.

[Anatole Dedecker]

I've just encountered this problem while porting Logic/Equiv/Nat (and in particular docs#equiv.nat_sum_nat_equiv_nat_apply). So while we definitely don't need this anymore from a technical point of view, maybe there is still a mathematical point in having operations for manipulating natural numbers in binary. What should we do?

[Anatole Dedecker]

In particular, wouldn't these come up again in the computability library?

[Mario Carneiro]

yes, the concept of decomposition into binary isn't going anywhere

[Mario Carneiro]

it's just the specific functions bit0 and bit1 that may be reconsidered

[Mario Carneiro]

On Nat there is a much more sensible way to write those functions, namely 2*n and 2*n + 1

[Anatole Dedecker]

Okay so I decided to use bit false and bit true instead because bit is not tagged as deprectated. I realize this is a bit stupid because bit is defined in terms of bit0 and bit1, but I figured it would be best to "stop" the deprecation-zone at the definition of bit. That way, when we want to get rid of them definitively, we only have to provide the definition of bit, which seems like it would be useful anyway to write 2*n + (b : Nat). Does that sound right?

[Ruben Van de Velde]

I'd be inclined to make changes like that after the port

[Mario Carneiro]

yes, I think we aren't ready to do a bit0/bit1 refactor yet

[Mario Carneiro]

let's wait until we have all the dependent code available so that we can assess what kind of refactor makes sense

[Mario Carneiro]

for now it's just deprecation-tagging to find all the dependents

[Anatole Dedecker]

Okay so I'll stay with bit0 and bit1 then

[Reid Barton]

Just to confirm, bit is not being deprecated right?
Just asking because @Chris Hughes marked the statement

theorem test_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b

as deprecated in mathlib4#1159, but I don't understand why.

[Chris Hughes]

I don't think it was me, I think it was someone else working on the PR. There are a whole bunch of deprecated attributes in that file to satisfy the linter

[Reid Barton]

Hmm, I checked git blame on the PR branch for that line

[Chris Hughes]

It probably was me then. The only reason I would have done it was to satisfy the linter. If the linter doesn't complain about that lemma then it was a mistake.

[Reid Barton]

OK, thanks!