open scoped UInt64.CommRing

Stream: mathlib4

[Geoffrey Irving]

One used to be able to do open scoped UInt64.CommRing to be able to use ring with UInt64. Is this gone now? I can't find the commit that removed it, so I'm not sure what replaces the functionality.

[Kim Morrison]

@Geoffrey Irving, this is a Mathlib question (as CommRing is defined there). I removed these instances back at v4.20. Are you able to just use grind instead of ring for this? It should work with UInt64 out of the box.

[Eric Wieser]

Why were these instances removed from mathlib?

[Eric Wieser]

Looking at https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean it seems that the docstring still promises the instances exist

[Eric Wieser]

Geoffrey Irving said:

I can't find the commit that removed it

https://github.com/leanprover-community/mathlib4/commit/7d6781bab0100467855789de1053ccabeed34520

[Kim Morrison]

I'm disinclined to have material about UIntX in Mathlib, as it's not particularly germane to mathematics. Downstream users who need ring for UIntX (but for whom grind doesn't suffice), if such exist, can let us know! Geoffrey's question indicates such users may exist, but let's wait to see if grind works for them.

[Kim Morrison]

(For the usual reasons; stuff that breaks on upgrades, but it not relevant to the scope of Mathlib, should not be in Mathlib, because it creates real maintenance costs.)

[Eric Wieser]

I've attempted to restore the missing instances, which identified a bunch of missing theorems in core in the process

[Eric Wieser]

This isn't just about grind, without these instanecs you can't work with Matrix _ _ UInt8 etc

[Robin Arnez]

I assume you're supposed to use ZMod 256 etc. instead?

[Eric Wieser]

#27540

[Eric Wieser]

One other argument for having these instances is that lemmas like docs#pow_succ and docs#pow_mul can be used

[Geoffrey Irving]

@Eric Wieser I’m happy to review this, but good to get to agreement between you and @Kim Morrison before I do that.

As some context, I’m using these as part of https://github.com/girving/interval. It’s certainly possible that grind will work (might take a few days to find time to try), but as you there are a ton of downstream lemmas that require the instances and currently won’t work.

[Eric Wieser]

Kim Morrison said:

as it's not particularly germane to mathematics

I would argue that mathlib should strive to instantiate every typeclass it defines for every possible type in its dependencies, at least in cases where those instances are obviously canonical, as they are for CommMonoid UInt8 for instance.

[Notification Bot]

This topic was moved here from #lean4 > open scoped UInt64.CommRing by Eric Wieser.

[Eric Wieser]

(since Kim Morrison said "this is a Mathlib question")

[Kim Morrison]

Eric Wieser said:

Kim Morrison said:

as it's not particularly germane to mathematics

I would argue that mathlib should strive to instantiate every typeclass it defines for every possible type in its dependencies, at least in cases where those instances are obviously canonical, as they are for CommMonoid UInt8 for instance.

I disagree; I think Mathlib shouldn't mention BitVec, IntX, or UIntX at all. It just causes pain all round to have unnecessary instances/lemmas in Mathlib about these things. (We've already been through several rounds of this, when upgrading the theory in core and having to deal with unused but broken code in Mathlib.)

[Eric Wieser]

What does "unused" / "unecessary" mean here? We have a user in this thread, and we have theorems in mathlib that need these instances to apply. If AddCommGroup UInt8 doesn't live in mathlib, where should it live?

[Eric Wieser]

I understand that bumping is hard work, and sometimes commenting out barely-used code is a necessary evil to get new Lean versions released; but I don't think that process should be used to argue against un-commenting it after fixing it.

[Kim Morrison]

I'm still not convinced we have a user who needs this. grind should handle whatever ring can do with UIntX (I pre-emptively agree it can't yet do what ring_nf can!)

[Eric Wieser]

Here's a theorem that can only be solved by grind with #27540 (and probably open scoped UInt64.CommRing):

import Mathlib

abbrev Coord := UInt8 × UInt8

theorem foo (p q : Coord) : p - (p + q) + q = 0 := by
  grind

[Eric Wieser]

Admittedly this particular one can be fixed in a different way in core as well, but only while we're using core types throughout

[Kim Morrison]

I don't object #27540 strongly enough to want to block it being merged. I just want us to be cautious here about adding material that we might later regret having in Mathlib.

[Eric Wieser]

It turns out I did miss something, and in the process identified an instance diamond in BitVec

[Eric Wieser]

Here it turns out that the definition in core has a worse defeq, and no API was provided to convert it to the good one!

[Geoffrey Irving]

Aside: Is there grind_nf, by analogy to ring_nf?

[Kim Morrison]

No. We're thinking about it, but it won't happen immediately.

[Geoffrey Irving]

I've now update all of my UInt64-related proofs. grind worked to replace ring exactly 0 times, and indeed I basically never got it to work for anything UInt64-related. But fortunately the modifications required to fix stuff wasn't too bad (replacing sub_zero with UInt64.sub_zero and such in lots and lots of places). Overall a solid mid result. :)

Mostly what I did instead of ring where something complicated was going on was to write some custom simp sets to turn UInt64 and Int64 related expressions into expressions over either BitVec (to be dispatched with bv_decide) or Int/Nat (to be dispatched with omega). This provided some nice simplifications in a few places: bv_decide is great.

[Eric Wieser]

Could I ping for a review on #27581 to fix ring?

[Eric Wieser]

I think it was already approved transitively by Kim via a dependent PR

[Henrik Böving]

Geoffrey Irving said:

Mostly what I did instead of ring where something complicated was going on was to write some custom simp sets to turn UInt64 and Int64 related expressions into expressions over either BitVec (to be dispatched with bv_decide) or Int/Nat (to be dispatched with omega). This provided some nice simplifications in a few places: bv_decide is great.

bv_decide should be capable to solve UInt64 and Int64 builtin operations on its own, do you have an example of where you needed more simplifications?

[Geoffrey Irving]

Eric Wieser said:

Could I ping for a review on #27581 to fix ring?

Looks good, approved! Sorry for delay.

[Geoffrey Irving]

@Henrik Böving Here are two different bv_decide error messages depending on which imports I use:

import Std.Tactic.BVDecide.Syntax

/-- None of the hypotheses are in the supported BitVec fragment after applying preprocessing.
There are three potential reasons for this:
1. If you are using custom BitVec constructs simplify them to built-in ones.
2. If your problem is using only built-in ones it might currently be out of reach.
   Consider expressing it in terms of different operations that are better supported.
3. The original goal was reduced to False and is thus invalid. -/
theorem basic (n : UInt64) : n.toInt64.toUInt64 = n := by bv_decide

import Mathlib

/-- The prover found a potentially spurious counterexample:
- It abstracted the following unsupported expressions as opaque variables: [n.toInt64.toUInt64]
Consider the following assignment:
n.toInt64.toUInt64 = 18446744073709551615
n = 9223372036854775807 -/
theorem basic (n : UInt64) : n.toInt64.toUInt64 = n := by bv_decide

[Geoffrey Irving]

Any way to get rid of Lean.ofReduceBool for bv_decide, by the way? I ended up only using it <10 times, which is fortunate since I forgot it introduces a compiler dependency. If it's unavoidable I'll try to replace the bv_decides with omegas.

[Henrik Böving]

You're not supposed to import .Syntax but the whole module, if you do that you get the same error message. The reason here is that we forgot to tag some lemmas in core, I'll see it fixed on Tuesday

[Henrik Böving]

Geoffrey Irving said:

Any way to get rid of Lean.ofReduceBool for bv_decide, by the way? I ended up only using it <10 times, which is fortunate since I forgot it introduces a compiler dependency. If it's unavoidable I'll try to replace the bv_decides with omegas.

No

[Henrik Böving]

Fixed at https://github.com/leanprover/lean4/pull/9721

[Eric Wieser]

Can I get a delegation on #27540? It was previously bors merged, but that was before the dependencies landed so I'm not sure if I should just merge it myself.

[Geoffrey Irving]

If delegation is something I can do, can you refresh my memory on what it means and how I would do it?

[Eric Wieser]

It is not