Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19 #7

Open
palmskog opened this issue Jan 3, 2024 · 18 comments
Open

Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19 #7

palmskog opened this issue Jan 3, 2024 · 18 comments

Comments

@palmskog
Copy link
Contributor

palmskog commented Jan 3, 2024

Description of the problem

Pierre Castéran and I have recently tried to fix many Stdlib arithmetic deprecation warnings in Coq 8.18 to avoid projects breaking in 8.19 due to coq/coq#18164. However, we have determined that some, specifically those related to Nat.add_sub and Nat.sub_add require significant work and are thus likely to break many projects forever. The following example is due to @Casteran:

Require Import Arith.
Require Import ArithRing.

Goal forall a b c d,  a <= d ->
                      a * b + (a * (c - b) +
                                 (d * (c - b) - a * (c - b)))
                      + d * b =
                        (d + a) * b + d * (c - b).
intros a b c d H.
rewrite (le_plus_minus_r).
(*
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
*)
  - ring.
  - now apply Nat.mul_le_mono_r.
Restart.
    (* lets apply the Hint *)
intros a b c d H.
 rewrite Nat.add_comm. (* needs more precision ! *)
 Fail rewrite Nat.sub_add.
Abort.

We believe Stdlib maintainers and release managers should seriously consider ensuring deprecated/removed lemmas requiring a combination of Nat.sub_add/Nat.add_sub and Nat.add_comm like le_plus_minus_r are added verbatim under Nat, e.g., Nat.le_plus_minus_r, cc: @SkySkimmer @olaure01

If coq/coq#18355 was implemented, the severity of this problem would be significantly reduced.

Coq Version

Deprecations show up in 8.18.0 and projects break in 8.19+rc1.
@Villetaneuse
Copy link
Contributor

I'm sorry this caused you some inconveniences. Indeed Minus.le_plus_minus_r was one of the lemmas without direct translations and caused me some problems too. Others on the top of my head are all the equivalences (e.g. Nat.succ_lt_mono).
There are 3 possible discussions happening here :

  1. how to fix this problem this time:
    I think rewrite (fun n => Nat.add_comm n (_ - n)), Nat.sub_add. should handle most cases.
  2. should we identify missing lemmas to include in 8.20? In this case, this would probably be something like add_sub_r (the idea is that plus is the symbol and add is the operation). I'd be happy to be part of this effort if there is consensus.
  3. how to handle better deprecated lemmas? I agree on the need to have better ways to handle this.

However, I certainly don't want to criticize @olaure01 and @SkySkimmer too much; the hints were already very useful and this was already quite a huge work. And of course, I'm also to blame since in the end I removed these files.

@palmskog
Copy link
Contributor Author

palmskog commented Jan 3, 2024 •
edited
Loading

@Villetaneuse to be clear, this was not at all about distributing blame, but instead about flagging up our hurdles and starting an inquiry into what we can do going forward.

In theory, "new" lemmas like Nat.add_sub_r could be introduced in 8.18.1 and also added to v8.19 before the release of 8.19.0, but I don't think @SkySkimmer would consider this feasible in practice?

In any case it makes sense to me to try to list such new "compatibility" lemmas to introduce for addition to 8.20 and then do a PR with them.

@Casteran
Copy link

Casteran commented Jan 3, 2024 via email

@SkySkimmer
Copy link
Contributor

In theory, "new" lemmas like Nat.add_sub_r could be introduced in 8.18.1 and also added to v8.19 before the release of 8.19.0, but I don't think @SkySkimmer would consider this feasible in practice?

Probably not for 8.19.0 but we could do a rapid 8.19.1.
Not sure what the status of 8.18.1 is cc @gares

@palmskog
Copy link
Contributor Author

palmskog commented Jan 3, 2024

Here is another example of an inconvenient deprecation replacement in 8.18:

Require Import Arith Lia.
Goal forall n m, S n <= m -> S n - S m = 0.
intros n m Hn.
rewrite not_le_minus_0.
(*
Warning: Notation not_le_minus_0 is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
*)
- reflexivity.
- lia.
Qed.

Just replacing not_le_minus_0 with Nat.sub_0_le gives a completely different goal, and it's difficult to see how one can apply Nat.lt_nge and Nat.lt_le_incl.

@palmskog
Copy link
Contributor Author

palmskog commented Jan 6, 2024 •
edited
Loading

I went through a lot of commits fixing deprecations, notably coq-community/coqtail-math@fcf495c coq-community/coq-art@c41affd. Here is my definitive list of the deprecated lemmas that take "too much" effort fix:

  • le_plus_minus_r (example above)
  • not_le_minus_0 (example above)
  • minus_plus
  • mult_S_lt_compat_l
  • even_2n
  • odd_S2n
  • minus_plus_simpl_l_reverse
  • mult_S_le_reg_l

If we have agreement this is a good idea, I can make a PR reintroducing these as close to verbatim as possible under appropriate new names Nat.xyz. Then we can decide if we aim for inclusion into v8.19 and maybe v8.18 as well.

@Villetaneuse
Copy link
Contributor

Villetaneuse commented Jan 6, 2024 •
edited
Loading

Are you sure about even_2n and odd_S2n? I had the impression that the newer predicates were simply better.
While I do agree something must be done, please let's not rush this... We need to look at what exists in ZArith, NArith, PArith to be consistent. I have to do study these parts thoroughly before working on Reals anyway (there is a will to make the lemmas more uniform with the Arith ones). Also, I've patched almost all the libraries in the CI, so if there are remaining libraries to work on, let me know. Imho, it's better that I spend some time patching libraries (again) than rushing a patch and adding lemmas we're not 100% happy about.

I am very busy until Wednesday, but then I'll start working on it with you. I just created this thread on zulip to coordinate work.

@palmskog
Copy link
Contributor Author

palmskog commented Jan 6, 2024

The background on even_2n and odd_S2n is that I've had to add local versions of them in several projects, since both of these are sigma types (they live in sort Set and compute) while the replacements are not. Typical code that uses even_2n and odd_S2n does some computation, and to refactor scripts between computational/non-computational behavior is more work than a deprecation should be, in my view.

@Villetaneuse
Copy link
Contributor

Villetaneuse commented Jan 6, 2024 •
edited
Loading

Aren't EvenT and OddT sufficient already? They are in Set and you can translate with even (in bool) and (Even in Prop) with dedicated lemmas (even_EvenT, Even_EvenT, etc).

@palmskog
Copy link
Contributor Author

palmskog commented Jan 6, 2024

It seems that what I was looking for was Even_EvenT and Odd_OddT as shown in this commit: coq-community/coqtail-math@1137fc2

However, these lemmas were not mentioned in the deprecation message, and it's unfortunate that EvenT doesn't use Nat.double like even_2n did before it...

So I guess even_2n and odd_S2n can be dropped from my list of additions, but I still think the deprecation message should be changed in 8.18.

@Casteran
Copy link

Casteran commented Jan 7, 2024 via email

@palmskog
Copy link
Contributor Author

palmskog commented Jan 7, 2024

I agree the app_ass deprecation message should be changed to add something like "(together with symmetry of equality)".

I believe the repetition of deprecation messages is a known problem, I think it has to do with how elaboration of syntax is currently done in different phases.

@Villetaneuse
Copy link
Contributor

Btw, a deprecation message may appear several times for the same term (e.g. rewrite app_ass). Is it a known fact?

I think this has been fixed. On which version is it observed?

@Casteran
Copy link

Casteran commented Jan 7, 2024 via email

@Villetaneuse
Copy link
Contributor

There is already this issue.

@Villetaneuse
Copy link
Contributor

Some time has passed (sorry, I'm slow...) and now I understand better the Numbers sublibrary. @palmskog Are there any updates in your list? I can start working on a PR reintroducing convenient lemmas in Numbers.

@palmskog
Copy link
Contributor Author

@Villetaneuse I have no updates, I think we have fixed all or most projects in Coq-community, so the "final" list of problematic removed lemmas is:

  • le_plus_minus_r
  • not_le_minus_0
  • minus_plus
  • mult_S_lt_compat_l
  • minus_plus_simpl_l_reverse
  • mult_S_le_reg_l

@Villetaneuse
Copy link
Contributor

Thanks!
I'll submit a PR in a weak or so. I'm a slow worker, very scared to add things in the stdlib now that I know how hard it is to remove things.

@Villetaneuse Villetaneuse mentioned this issue Mar 7, 2024
Closed
6 tasks
@proux01 proux01 transferred this issue from coq/coq Jan 13, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@palmskog @SkySkimmer @Casteran @Villetaneuse