[stdlib] stronger div, mod lemmas via module type

[mrhaandi]

This is a follow-up to uniformization of div and mod in #14086.
As a consequence, we can uniformly derive stronger lemmas for Nat and N assuming a / 0 == 0 and a mod 0 == a.

Closes #16186

The basic idea is to have an abstract, optional specification

Module Type NZDivSpec0 (Import A : Eq')(Import B : ZeroSuccPred' A)(Import C : DivMod' A).
  Axiom div_0_r : forall a, a / 0 == 0.
  Axiom mod_0_r : forall a, a mod 0 == a.
End NZDivSpec0.

In addition, modules NDiv0.NDivProp0 (as apposed to NDiv.NDivProp) and NLcm0.NLcmProp0 (as apposed to NLcm.NLcmProp) provide stronger lemmas based on NZDivSpec0. For example:

(* NDivProp  *) Lemma div_div : forall a b c, b~=0 -> c~=0 -> (a/b)/c == a/(b*c).
(* NDivProp0 *) Lemma Div0.div_div : forall a b c, (a/b)/c == a/(b*c).

Any number system which satisfies NZDivSpec0 may for free benefit from the stronger lemmas.

• We instantiate PeanoNat.Nat and BinNat.N as above.
• We do not deprecate NDivProp or NLcmProp, which are valid (and useful) for number systems that do not satisfy NZDivSpec0.
• We do not touch Z, which is a separate concern.

Deprecation Phases

We aim for maximal compatibility for each phase with deprecation warnings.

Phase 1

• Stronger lemmas are encapsulated in Div0 and Lcm0 modules.
• Weaker lemmas encapsulated in Notation with a deprecated attribute.
• Search does not display weaker lemmas due to Private_ prefix.

Phase 2

• Stronger lemmas are both top-level and in Div0 and Lcm0 modules.
• Weaker lemmas are removed.
• Div0 and Lcm0 modules are deprecated.

Phase 3

• Modules Div0 and Lcm0 are removed.

[mrhaandi]

For PeanoNat this approach seems to work really well. It provides the strongest Nat.xyz_full lemmas and uses only a single Include NDivProp0..

[olaure01]

Could it be possible to rely on the module system to keep the same name for strong statements as for weak ones? thus avoiding the use of _full.
Under a given name, you import NZDiv you get the weak statement, you import NZDiv0 you get the strong one.

[mrhaandi]

Could it be possible to rely on the module system to keep the same name for strong statements as for weak ones? thus avoiding the use of _full. Under a given name, you import NZDiv you get the weak statement, you import NZDiv0 you get the strong one.

I'm not sure what is the best way here and I am open to suggestions. Shadowing the existing Nat module by a different one upon an extra import is possible, but I rather prefer not to. This would lead to a lot of confusion.

A good compromise is still to have the weak lemmas marked as deprecated (as in the other PR) and after a transition rename the strong ones to their proper names.
At an early point one can hide weak lemmas from Search, so the user is not overwhelmed by duplicates.

[olaure01]

I'm not sure what is the best way here and I am open to suggestions. Shadowing the existing Nat module by a different one upon an extra import is possible, but I rather prefer not to. This would lead to a lot of confusion.

Talking about the final target (not considering the deprecation phase yet), I would imagine for example creating a NExtraProp0 in Numbers.Natural.Abstract.NProperties which uses NDivProp0 instead of NDivProp, and then to include NExtraProp0 instead of NExtraProp0 in PeanoNat.Nat. NDivProp0 could redefine weak statements from NDivProp into strong ones as it is the case currently for example with NDiv.mod_same : forall a, a~=0 -> a mod a == 0. overloading NZDiv.mod_same : forall a, 0<a -> a mod a == 0..

[mrhaandi]

Talking about the final target (not considering the deprecation phase yet)

Oh yes, replacing weak lemmas in PeanoNat.Nat by strong ones using the module system is easy; almost everything is already in place. So the final target is not a problem. Next week I will look deeper into the Z counterpart.

[mrhaandi]

I now added stronger _full lemmas via inclusion of ZDivFloor0.v to the Z module. This is cleaner than #16189.

@olaure01 What is the status of ZArith/Zdiv.v? It contains all kinds of (sometimes incoherently named) lemmas, sometimes just restating facts from Z. Some of the lemmas could have (without this PR) already been deprecated in favor of Z lemmas.

I see two options.

1. Deprecate as many ZArith/Zdiv.v lemmas as possible now in favor of _full lemmas.
2. Do not touch ZArith/Zdiv.v. Only deprecate weak lemmas in Z. After this first deprecation phase, rename strong lemmas (removing _full suffix). Then deprecate as many ZArith/Zdiv.v using strong lemmas (without the _full suffix).

Option 2 would be easier on the users. Option 1 would entail e.g. the Zdiv.Zdiv_0_l => Z.div_0_l_full => Z.div_0_l dance.

[olaure01]

What is the status of ZArith/Zdiv.v?

I am not sure. Similar files like ZArith/Zmin.v are explicitly mentioned as deprecated/obsolete (thus probably subject to the analogue of #14736).

1. Deprecate as many ZArith/Zdiv.v lemmas as possible now in favor of _full lemmas.

Since deprecation phases are long (in particular when we want to reuse old names), I am in general in favor of starting them as soon as possible.

2. Do not touch ZArith/Zdiv.v. Only deprecate weak lemmas in Z. After this first deprecation phase, rename strong lemmas (removing _full suffix). Then deprecate as many ZArith/Zdiv.v using strong lemmas (without the _full suffix).

I agree that in the present situation going back and forth through _full names would be painful, and option 2 looks better.

Would it be reasonable to consider settling now the architecture of the final target of the process (with strong statements available under _full-free names) and declaring temporary modules PeanoNatFull.Nat and BinIntFull.Z to make this architecture accessible immediately? This could allow users interested in adapting now their development towards the target situation to:

1. import now these new modules to directly use final names for strong statements;
2. in the next step, reach the final situation by just replacing PeanoNatFull with PeanoNat and BinIntFull with BinInt.

[mrhaandi]

PeanoNatFull.Nat and BinIntFull.Z

I'm not sure whether I like the idea. It creates a third competing module, which will surely take over a year to again deprecate.
A newcomer will have the (sometimes uninformed) choice between

1. ZDiv (currently often used, mostly deprecated)
2. BinInt.Z (partially deprecated)
3. BinIntFull.Z (handy, but will be deprecated shortly)

[olaure01]

It creates a third competing module, which will surely take over a year to again deprecate.

The idea would be to be clear about the status of these modules (and probably mention their existence in changelog only):

• to be used only by project maintainers willing to prepare for future, or by developers interested in strong statements with an easier renaming phase at deprecation of _full statements;
• not subject to deprecation phase (they will be silently deleted when corresponding PeanoNat.Nat and BinInt.Z are ready).

[mrhaandi]

to be used only by project maintainers willing to prepare for future

I am such a developer of a (undecidability) library with over 100K LOC. PeanoNatFull.Nat would shadow PeanoNat.Nat, which makes imports order sensitive (also via some transitive exports). So I would not use PeanoNatFull.Nat for reasons of error locality.

[mrhaandi]

I understand the wish to avoid in productive code xyz_full lemmas to only rename them back to xyz after deprecation.
How about the following:
In PeanoNat.Nat create a submodule Div0 with xyz lemmas. No _full suffix.
Intermediate use would be instead of Nat.xyz_full use Nat.Div0.xyz.
If a power user would like to shadow old lemmas, then simply:

Require Import PeanoNat.
Module Nat := Nat.Div0.

should locally shadow old xyz lemmas by new ones.
After deprecation it is easier to replace Nat.Div0.xyz (compared to Nat.xyz_full) by Nat.xyz.

[mrhaandi]

While trying to sideways refactor NDivProp I noticed that the whole module tower in PeanoNat is then starting to fall over. Mainly because further up module types such as NLcmProp contain weak lemmas e.g. Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)). with a dependence on the weak division lemmas. The main consequence is that NLcmProp and others will need a NLcmProp0 counterpart. Otherwise, we cannot use Notation to deprecate weak nat lemmas.

Also, we cannot deprecate the module types such as NDivProp or NLcmProp but only their use in PeanoNat.
Otherwise, the abstract module types will become incompatible with other division by zero conventions.

I will shift my focus solely on nat and N now. Z has an even larger module type tower and will require further investigation.

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[mrhaandi]

@olaure01 I finally figured out (for Nat/N) a module structure which has almost no code duplication and allows for deprecation via Notation. The overall approach is now solid for Nat/N and quire useful. I consider this close to done and will not touch Z in this PR. If ci agrees, I will switch the status to "Ready for review".

[mrhaandi]

I'm not sure why, the test-suite:base ci job runs normally until success/SchemeEquality.v and then takes forever.
When I compile locally time make -C test-suite, everything works fine and takes the same amount of time as before this PR.

[Alizter]

@mrhaandi I would suspect that some boolean equality is not found and the boolean equality scheme tries to go and derive it automatically. Are you able to observe slow down in that file when you run it manually in an editor?

cc @herbelin

[mrhaandi]

Are you able to observe slow down in that file when you run it manually in an editor?

In the editor I see no slowdown in success/SchemeEquality.v and the overall test-suite compilation time is basically the same.
To be sure, I use a clean checkout (to have no caches present). Although I doubt it, but maybe my OCaml 4.12.0 behaves differently than 4.09.0 from the ci?

[mrhaandi]

@Alizter What did you change in the ci that success/SchemeEquality.v passed? Or was it just a rerun?

[Alizter]

@mrhaandi I reran it yesterday. Sometimes the CI takes its time. It was unrelated to SchemeEquality.v.

[Alizter]

@olaure01 Did you want to have a look? Otherwise I will merge soon.

[olaure01]

@Alizter I planned to have look next week or the week after, but if it is OK with you, please go.

[Alizter]

@olaure01 In that case I will wait for your review. No rush.

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[olaure01]

I think the work on induction in NZOrder and on Bezout in NGcd should be documented in changelog.
You could also mention more about the future in changelog: planned deprecation phases, and the trick to directly go close to the end following: Module Nat := Nat.Div0.

[mrhaandi]

I think the work on induction in NZOrder and on Bezout in NGcd should be documented in changelog.

Yes, I forgot to add a note on measure_induction which is a uniform way to have Wf_nat.induction_ltof1 and is compatible with the induction tactic. I added the info to the changelog, thank you.

You could also mention more about the future in changelog: planned deprecation phases, and the trick to directly go close to the end following: Module Nat := Nat.Div0.

Yes.

[olaure01]

@coq/doc-maintainers This PR both adds, removes, changes and deprecates things. Is the changelog OK, or would it be better to split it into separated Added / Changed / Deprecated / ... entries?

[Alizter]

I think splitting up the changelog entry would be a good idea.

[mrhaandi]

I think splitting up the changelog entry would be a good idea.

I now split the changelog entries into three orthogonal bullet points. Is this the standard approach, or should I create distinct changelog files?

[proux01]

That's fine, no need for distinct files.

[Alizter]

I will merge this soon. @proux01 are you still having a look?

[mrhaandi]

I will merge this soon.

Squashed and rebased to be on the safe side.

[proux01]

I will merge this soon. @proux01 are you still having a look?

@Alizter nope, feel free to merge

[Alizter]

@coqbot merge now

[JasonGross]

@mrhaandi Has any investigation been done into removing the useless hypotheses from the Z lemmas?

[mrhaandi]

Has any investigation been done into removing the useless hypotheses from the Z lemmas?

Unfortunately, the situation with Z is more complicated than with nat. Also, the current solution for nat has drawbacks regarding usability, in order to be backwards compatible. Since for my work nat is most important, I have little motivation to put comparable (or even more) effort into Z.

[JasonGross]

@mrhaandi would you be willing to describe what the drawbacks and considerations are? I've been considering doing this work myself, if I ever find the time for it, and would be interested in not retreading known dead-ends and having a better sense up front what the rough design trade-offs are.