More bitwise in Numbers.Natural.Abstract

[Villetaneuse]

Added:

• strong_induction_le in NOrder (not sure about this one)
• Even_Odd_induction in NBits (not sure about capitalization)
• land_(even|odd)_(even|odd), land_le_[lr]
• ldiff_(even|odd)_(even|odd), ldiff_le_l
• le_div2_diag_l
• le_shiftl and shiftr_le (not sure about names here)
• ones_0 and ones_succ

related to #17043: there, the lemmas are in a new file NArith.Nbitwise and proved with lia
@andres-erbsen lnot_ones_same is already there, named lnot_ones; I've not looked into Positive yet.

Questions:

• should this effort be more general (write similar lemmas for lxor, lor, ...)?
• What do you think of Integer? Should I try to give the most general statements in NatInt?

I don't think it's a final product, but I feel that I need some feedback now.

Fixes / closes #????

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.

• Opened overlay pull requests.

[andres-erbsen]

Thank you for prototyping a Numbers-based proof for these lemmas! Overall looking nice; let's try to make it happen. I am not sure whether the supporting lemmas newly added in this PR are important to expose for use outside Numbers, but maybe they are, and regardless I think we want them non-Local for use in other Numbers files.

I would be willing to assign (and merge after working out minor details) but I'll give other stdlib devs the opportunity since this design is substantially influenced by my own work and independent review is good or something.

Naming brainstorming

Hmm, this is one of the cases where syntax-tree-based naming does not lead to unique naming choices. I will throw out some alternatives.

Even_Odd_induction

How about bits_ind or binary_induction? This definition does not mention Odd at all, so I'd prefer not to include it.

Can this definition be used with induction .. using, or is there a mundane or fundamental blocker?

land_(even|odd)_(even|odd)

land_double_..., land_succ_double_... ? Could even state in terms of these definitions for consistency, but I don't feel strongly.

le_div2_diag_l

I think the _l and _diag are redundant (would there be another diag lemma with _r?). Alternative ideas:
div2_upper_bound (like for mod)? div2_range (following fiat-crypto)? range_div2 (following HoTT naming guidelines)? Just le_div2_diag?

le_shiftl and shiftr_le (not sure about names here)

shiftl_upper_bound? shiftl_range? range_shiftl? le_shiftl_r and le_shiftr_l? Not sure either.

Minor

Parenthesizing function applications that appear as arguments to infix operations shouldn't be necessary (function application binds tighter).

Using - instead of { is fine as the rest of the file also does.

The proofs look fine on their own.

High-level approach

@coq/stdlib-maintainers @proux01 the Numbers-based proofs here are 5x longer than the lia-based proofs versions here, and I'd guess they took more than 5x as long to create (thanks again @Villetaneuse!). I think this comparison is a clear indication that we would benefit from separate Require-able modules for as little and as much of NArith as possible, perhaps NArithMinimal (NArithBase?) and NArithMaximal (NArith?). Porting lia-based proofs to the current structure is needless friction for development and maintenance. (I don't think we should block this PR on it, but I would like to find a way forward here)

[JasonGross]

Regarding high-level approach: I think the ultimate goal here should maybe be to provide a bitblast tactic that can (a) turn bitwise goals and hypotheses into equivalent boolean ones and then (b) discharge with btauto or similar. And then have a library of "convenience lemmas" that are all proven with bitblast, and a core library of "specs of each operation in terms of testbit".

I'm not sure what the appropriate way to handle addition and multiplication would be---maybe turn every concrete number into a sum of powers of two, distribute multiplication over addition, turn multiplication by a power of two into left shift, have a rule that turns x + y into x | y when x & y = 0? Or I guess we want (x + y) = x | y + x & y?

Thoughts? (Apologies if this PR is the wrong place for this discussion and it belongs in a PR or CEP)

[andres-erbsen]

@JasonGross I think your high-level idea is different from the one I raised, but dependent on it: a bitwise-reasoning tactic would almost surely depend on Z through lia for side condiitons. Zbitwise.v has a tactic that kinda matches what you have in mind, I try not to call it bitblasting to avoid confusion with the easier known-width case. And yes, any separate discussion space would probably be preferred.

[MSoegtropIMC]

I am also a fan of a split level approach: files with really basic stuff on top of which come tools like lia, bit blasting, you name it, on top of which come the user facing lemma library.

With the current structure a major problem ist that many useful lemmas, which could go into the library, are proven in a richer context, so that porting them to the standard library frequently requires a complete rewrite. This is bad.

[Villetaneuse]

Mostly to @andres-erbsen:

• I've renamed Even_Odd_induction into binary_induction
• I've renamed le_shiftl and shiftr_le into, respectively shiftl_lower_bound and shiftr_upper_bound
• For div2 a <= a, I prefer my naming (though it's arguably verbose) : it's consistent with le_succ_diag_r and the lemma is not precise enough to be called a canonical upper bound imho. I've added div2_le_(upper|lower)_bound consistent with div_(upper|lower)_bound
• For now, the induction lemmas cannot be used with induction, probably because of the nasty (and useless) Proper thing. TODO: try specializing them (and then hiding them) in NArith and Arith to see if induction with works.
• I don't think I get your point about bullets versus curly braces, is there a reason to use one or the other? What I usually have in mind is: when a tactic adds new subgoals which are more or less equivalently "important" steps (e.g. split) in the proof, I use bullets. When a tactic (assert, enough) needs a quick subproof, I use braces. Of course the distinction is not precise.

@andres-erbsen @JasonGross @MSoegtropIMC
Now about higher-level concerns, please let me advocate using no automation at this basic level (without discarding your valid arguments, of course).

1. I do think having a simpler dependency graph is helpful for the user. In some cases (teaching) it's important to know what exactly you will have when you Require something. It also eases browsing the sources which, at this point, is still the most efficient way to understand the stdlib.
2. Using automation for basic lemmas hides missing lemmas. My lengthy (not final) proofs show that some easy parts are still not easy enough (e.g. 1 <= a^b when a <> 0). Automation will never prove everything so these missing lemmas will bite someone at some point.
3. (Maybe I'm completely wrong here) The stdlib is compiled many times a day, using a costly hammer to prove basic things may lead to waste.
4. I guess that if someone wants to add a lemma in Arith, it's ok (we can always replace it later with a more general version in Numbers).
5. It was still fun to write :) (Maybe I'll get bored at some point, though)

[andres-erbsen]

I agree the considerations you bring up are relevant and sometimes in tension with using automation for ease of maintenance as I was advocating; we'll have to see for each proposed addition. As for the user-visible dependency graph, my preference would be for NArith to be the path for all theory about N operations and that we should make a new path for only basic theory for (probably less common) use cases that require it.

@coqbot run full ci

[andres-erbsen]

CI looks good; windows failure looks unrelated. I believe the precedent is to have a changelog entry for this. I intend to look at this again in a couple of days and to merge if it has a changelog entry by then.

[Villetaneuse]

Thank you!
If you don't mind, I would also like to:

• change binary_induction (and redefine it without the spurious Proper clause in implementations) so that it can be useful with induction with : this could be difficult (at least for me), I don't really understand what is going on in PeanoNat.Nat for instance
• double check the proofs to add missing non-controversial lemmas
• double check the Search outputs in PeanoNat and BinNat to make sure there is no obvious overlapping

I can spend a couple hour on this tomorrow

If it's ok and people use these lemmas we can easily add more for lor, lxor, etc; but this can be done in a separate PR.

[proux01]

I would be willing to assign (and merge after working out minor details) but I'll give other stdlib devs the opportunity since this design is substantially influenced by my own work and independent review is good or something.

I only had a quick look and this mostly looks reasonable. You two are certainly more knowledgable than me about that part of the library, so please go ahead.

the Numbers-based proofs here are 5x longer than the lia-based proofs versions here, and I'd guess they took more than 5x as long to create (thanks again @Villetaneuse!). I think this comparison is a clear indication that we would benefit from separate Require-able modules for as little and as much of NArith as possible, perhaps NArithMinimal (NArithBase?) and NArithMaximal (NArith?). Porting lia-based proofs to the current structure is needless friction for development and maintenance. (I don't think we should block this PR on it, but I would like to find a way forward here)

It seems we all agree. A PR clearly separating some NArithBase from some more general files that could use lia would certainly be welcome. It could for instance put the current content of theories/NArith (or a subset of it) in some theories/NArith/Base directory and we would then have a theories/NArith/All directory whose content would require lia. Ideally a CI job would check that NArith/Base can be compiled without more dependencies (but I could do that later, for instance as part of the package split while implementing the stdlib CEP coq/ceps#83 ).

[Villetaneuse]

Thank you @proux01 for your comments. I will take them carefully into account. @andres-erbsen I need to work a little bit more on it, sorry. I think I don't want to add anything more but maybe remove some of theses lemmas and there are two issues:

• it seems difficult to hide the "with Proper" versions of induction lemmas in PeanoNat and BinNat, the modules are Included, not Imported, so IIUC there is no easy way to shadow lemmas and replace them with a better version. I would never want to prove Proper when the relation is Leibniz equality (+ this prevents induction with to work correctly), so if I don't have a solution I will at least hide the two induction lemmas. Please let me know if you know some hack to solve this.
• there is a smaller issue with div2_even and div2_odd': there is already an imho not very well named lemma called div2_odd in NBits.v and div2_double and div2_succ_double directly in PeanoNat (of course, not in BinNat...); I will try to solve this, but if I can't find an easy solution, I will just drop div2_even and div2_odd' and manually inline them when needed.

I made new additions and I'm scared so don't hesitate to criticize them:

• (even|odd)_[succ_]double in NParity.v, not happy with the names, but couldn't find better ones (however, I'm convinced these lemmas are very useful)
• b2n_le_1
• testbit_div2, div2_odd', div2_even
• land_(even|odd)_[lr] to reason by case on 1 variable (these are probably better than the others, but maybe they could stay for reasoning on both variables directly)
• same for ldiff
• le_mul_l and le_mul_r in NMulOrder
• le_1_succ and neq_0_le_1 in NOrder
• pow_lower_bound in NPow
• sub_pred_l sub_pred_r and sub_sub_distr in NSub

So that's more than what you asked for... these seemed reasonable but maybe I got carried away!
Finally, I need to check that these are not already present, it's not that easy since Search seems to be broken inside modules.

[Villetaneuse]

Sorry for the noise... I made many mistakes I will fix tomorrow. My poor brain still struggles with git.

[Villetaneuse]

No real progress (except a crazy amount of git shenanigans to fix whitespace issues and errors on my part).
There are lemmas in PeanoNat which already cover some of these.

• le_div2 \approx le_div2_diag_l
• lt_div2 \approx lt_div2_diag_l
• div2_double = div2_even
• div2_odd' \approx div2_succ_double

I need to work this out. The best solution would be to move these lemmas from PeanoNat to Numbers/Natural so that we get them at least in N and Nat (maybe also in Z, but I'm scared by division in Z) without any breakage.

The naming of odd_succ_double, etc is still an issue.

I still can't figure how I could remove the "Proper" condition in PeanoNat. I'm considering killing strong_induction_le and making binary_induction Private.

[JasonGross]

I still can't figure how I could remove the "Proper" condition in PeanoNat. I'm considering killing strong_induction_le and making binary_induction Private

If you're talking about Proper (eq ==> iff) A, you don't get to remove this until you reach the level of concreteness that tells you that eq is leibniz equality. You could also remove it by phrasing the conclusion as forall n, exists m, n == m /\ A m. As a counterexample, consider trying to instantiate this module with { q : Q | q == Qround q } (the rationals representing whole numbers). If A demands that the rational is also in reduced form, then you can't just use induction to prove the property.

[Villetaneuse]

I still can't figure how I could remove the "Proper" condition in PeanoNat. I'm considering killing strong_induction_le and making binary_induction Private

If you're talking about Proper (eq ==> iff) A, you don't get to remove this until you reach the level of concreteness that tells you that eq is leibniz equality. You could also remove it by phrasing the conclusion as forall n, exists m, n == m /\ A m. As a counterexample, consider trying to instantiate this module with { q : Q | q == Qround q } (the rationals representing whole numbers). If A demands that the rational is also in reduced form, then you can't just use induction to prove the property.

Thank you for your comment! I was not saying that the Proper conditions are useless in general. There are indeed many models of this theory where equality isn't Leibniz. But I'm convinced that in this case where the actual used implementations of natural numbers and integers all use syntactic equality, it was a mistake to aim for this level of generality. All the user gets is an environment full of spurious conditions; the biggest one being Proper eq ==> A but there are many others; many lemmas about natural numbers have some 0 <= n condition; which is embarrassing.

I certainly don't want to add another one of these suboptimal lemmas, hence my problem with my binary_induction.

In the end (sorry for thinking oop too much), I really would like to specialize those inherited suboptimal lemmas. I don't know if it's possible.

[proux01]

@andres-erbsen strange, the "Maintainers are allowed to edit this pull request." box is checked and I was able to push your commit.

[andres-erbsen]

I think for Github (as opposed to Coqbot), maintainers means core devs.

[proux01]

That sounds bound, it shouldn't IMO.
Let's ping @Zimmi48 who may know better: can't maintainers push to PRs with "Maintainers are allowed to edit this pull request"?

[JasonGross]

At a glance, https://github.com/orgs/coq/teams/contributors?query=role%3Amaintainer+membership%3Achild-team and https://github.com/orgs/coq/teams/contributors?query=role%3Amaintainer indeed seem to contain only the core devs.

[proux01]

But https://github.com/orgs/coq/teams/contributors?query=role%3Amember+membership%3Achild-team seems to contain everybody. I don't understand much to those github things, let's add it to the agenda of a forthcoming call: https://github.com/coq/coq/wiki/Coq-Call-2024-04-30

[JasonGross]

But https://github.com/orgs/coq/teams/contributors?query=role%3Amember+membership%3Achild-team seems to contain everybody

Yes, that is everybody with write access I believe. There's a table of permissions here. Given that it specifically says "maintainers" in "Maintainers are allowed to edit this pull request", it's not surprising that people with only write access but not maintain access can't push.

[Zimmi48]

@andres-erbsen Can you confirm that you do not see the sentence "Add more commits by pushing to..." at the bottom of the conversation, as in this screenshot?

[andres-erbsen]

I do see that text 🤔. And apparently I can commit using the github web interface.

[JasonGross]

Did you add git@github.com:Villetaneuse/coq.git as your remote or https://github.com/Villetaneuse/coq.git, or did you try to push to refs/pull/18628/head on coq/coq? I believe only the first option (git@github.com:Villetaneuse/coq.git) will work.

[Villetaneuse]

@coqbot run full ci

[andres-erbsen]

@coqbot merge now