Mathlib bump for "Operations for bit representation of ..."

Stream: std4

[Scott Morrison]

std4#366 has gone through now, and it has caused some breakages in Mathlib.

The adaptation PR is at #8700, but it is incomplete. Any assistance much appreciated.

(Pinging @Joe Hendrix as the author of std4#366.)

[Scott Morrison]

I've fixed a bit more. I'm hoping that a file with module doc "perhaps only of archaeological significance" is allowed to have some hacky proofs.

[Scott Morrison]

I've now either fixed everything, or commented out things that are broke but not used elsewhere in Mathlib.

I'd really like a resolution to this PR by tomorrow, so I can release v4.3.0. This PR will potentially hold it up as Mathlib and Std are out of sync.

Options:

• Someone enthusiastic about bitwise operations quickly patches these up.
• We leave the broken but unused theorems commented out for someone to fix later.
• We just delete these lemmas outright.

[Scott Morrison]

Now that lots of material about bitwise operations has moved up to Std, and changed in the process, the treatment of bitwise operations in Mathlib is looking pretty bedraggled. Someone taking care of it more generally would be great!

[Mario Carneiro]

Can we just rename the mathlib definitions for now and keep the theorems?

[Mario Carneiro]

(The theorems are also good candidates for proof_wanted in std BTW)

[Ruben Van de Velde]

Does anything in mathlib depend on bitwise operations?

[Scott Morrison]

Sadly yes, it is quite hard to rip this out.

[Scott Morrison]

If someone wanted to do a refactor to separate out the material that is used in other files, vs the rest, that would be great!

[Scott Morrison]

Okay, #8705 is the alternative bump PR, that keeps Mathlib's Nat.testBit, renaming it to Nat.testBit'.

[Scott Morrison]

It would be great if one of these (probably #8705) could be merged by tomorrow so I can do the v4.3.0 release. :-)

[Alex Keizer]

Mario Carneiro said:

(The theorems are also good candidates for proof_wanted in std BTW)

What does proof_wanted mean?

[Alex Keizer]

I fixed the broken proofs in #8700, so that one should be ready to merge

[Eric Wieser]

As I remark in this comment, it seems a shame that we're proving things from scratch in Std rather than copying across the in-some-cases neater mathlib proofs.

[Floris van Doorn]

Alex Keizer said:

What does proof_wanted mean?

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60proof_wanted.60

[Joe Hendrix]

Thank you @Scott Morrison, @Alex Keizer and others, per @Eric Wieser's comments, I'll look and see if any of the proofs that were affected and may have cleaner analogues in Mathlib. I tried to mine Mathlib for proofs when there were clear Mathlib analogues in std4#366.

binaryRec is a most significant to least-significant fold over nat and could be migrated now.

The reason for the std changes were primarily to ensure we had foundation for a high-performance translation from a nat-based representation to a bool-vector based representation for BitVec. This will be important for translating bit vector and uintX problems into SAT/SMT (which is a priority for the FRO).

I also personally wanted to move away from some of the bit, bit0 and bit1 focused proofs that made less sense to me in Lean 4 due to kernel-level Nat.

[Eric Wieser]

Note that docs#Nat.binaryRec' is also very useful; possibly more than the unprimed version

[Eric Wieser]

Aside from the name, it's not clear to me why removing bit from proofs is beneficial; it enables a pretty natural recursion on least-significant bits.

[Eric Wieser]

Certainly bit0 and bit1 should be eliminated; they're after all just remnants of the system that OfNat replaced

[Alex Keizer]

I've been contemplating a refactor that uses the RHS of bit_val as the definition of bit and replaces all uses of bit0 with bit false and bit1 with bit true in theorems, allowing us to get rid of bit1 and bit0. Would that be welcome?

[Ruben Van de Velde]

I'm not sure I see the point of that

[Alex Keizer]

bit0 and bit1 are deprecated, but are still used in the definition of (non-deprecated) bit, so in theorems we continuously have to turn of the deprecated linter. Furthermore, currently results that hold true for bit b in general have to be triplicated: once for bit and the concrete cases bit1 and bit0, because of the simp-lemma that rewrites bit true and bit false into the former

[Joe Hendrix]

The bit_val definition of bit seems like it may be useful. div2Induction plays a similar role to binaryRec but I found it sometimes tricky to decide which variable to induct on. I found myself preferring using eq_of_testbit_eq as a blunt tool when reasoning about two Nat expressions involving a mix of binary and arithmetic operations, and then simplifying using testBit simplification lemmas.

I'd really like to see omega land in Std and then see how much it can be used to simplify proofs. Some of these may be needed for Omega itself, but I suspect many do not. Once omega is landed and performs well, the lemmas we want to prioritize may change.

[Mario Carneiro]

Eric Wieser said:

Aside from the name, it's not clear to me why removing bit from proofs is beneficial; it enables a pretty natural recursion on least-significant bits.

I thought this made it to Std with a name like pushBit or shiftBit or something?

[Alex Keizer]

There was some discussion around a PR which suggested that, but I don't think it got merged

[Ruben Van de Velde]

Mario Carneiro said:

Eric Wieser said:

Aside from the name, it's not clear to me why removing bit from proofs is beneficial; it enables a pretty natural recursion on least-significant bits.

I thought this made it to Std with a name like pushBit or shiftBit or something?

https://github.com/leanprover/std4/pull/314

[Eric Wieser]

There's one more conflict between mathlib4 and std4 here;

-- mathlib4
def adc {n} (x y : BitVec n) : Bool → BitVec (n+1) :=

vs

-- std4
def adc (x y : BitVec w) : Bool → Bool × BitVec w :=

for now I've primed the mathlib name.

[Eric Wieser]

Regarding std4#314, mathlib already has a second name for docs#bit: docs#Std.BitVec.addLsb. We should merge them with whatever name Std decides on

[Alex Keizer]

addLsb is just an alias for flip bit, so it shouldn't be hard to drop it

[Eric Wieser]

.. or to drop bit, if we decide the other argument order is better

[Eric Wieser]

It seems Std also flipped the order of multiplication in docs#Nat.mul_add_mod such that it no longer matches docs#Nat.mul_add_mod_of_lt. Was this intentional? For now, I've reintroduced Nat.mul_add_mod'to mathlib to preserve the original statement

[Alex Keizer]

Eric Wieser said:

There's one more conflict between mathlib4 and std4 here;

-- mathlib4
def adc {n} (x y : BitVec n) : Bool → BitVec (n+1) :=

vs

-- std4
def adc (x y : BitVec w) : Bool → Bool × BitVec w :=

for now I've primed the mathlib name.

Should we deprecate the mathlib version, since it's trivially obtained from the std version?

[Alex Keizer]

In fact, there is more breakage in the BitVec.Lemmas file of mathlib, I'll have a look at that now

[Eric Wieser]

You might want to wait half an hour until a full cache is available

[Joe Hendrix]

Eric Wieser said:

It seems Std also flipped the order of multiplication in docs#Nat.mul_add_mod such that it no longer matches docs#Nat.mul_add_mod_of_lt. Was this intentional? For now, I've reintroduced Nat.mul_add_mod'to mathlib to preserve the original statement

Indeed, I don't know if there's an ideal choice, but I tried to consistently commute divisors in an expression to appear on the left of a multiply in other positions -- similar to Nat.div_add_mod.

[Eric Wieser]

That tends to be backwards overall, because when naming things in the non-commutative setting you don't have that luxury and have to put the multiplication on the right to match the division. Of course for % the concern is irrelevant, but for / it's not, and it's nice for the two to be consistent

[Eric Wieser]

Either way, this isn't something that needs to block the Std bump; I've sent #8700 to bors. We can always shuffle the names around in a future PR

[Eric Wieser]

(Arguably the ideal choice in the face of no clear winner is the one that doesn't break downstream users that already expect the name to mean a certain thing; though admittedly the damage in mathlib was minimal)

[Scott Morrison]

Thank you so much for all the work on #8700, @Eric Wieser. Very much appreciated.

[Eric Wieser]

Most of the credit here goes to @Alex Keizer, who actually fixed all the proofs; I just cleaned up