Stream: Coq devs & plugin devs

Topic: Modify order of parameters in mul_sub_distr_l


view this post on Zulip Pierre Rousselin (Mar 10 2024 at 07:29):

In Coq/Coq#18761, I'm looking at subtraction on integer types. I found out that mul_sub_distr_l has different interfaces in natural types and integer types.

Require Import BinInt PeanoNat.
Check Nat.mul_sub_distr_l. (*  forall n m p : nat, p * (n - m) = p * n - p * m *)
Check Z.mul_sub_distr_l.      (*  forall n m p : Z, (n * (m - p))%Z = (n * m - n * p)%Z *)

At first, I was thinking about keeping only the Z interface, but this would break external libraries and break the contract.

Another option would be to:

  1. in 8.20, add a mul_sub_distr_l' in natural types with the Z interface, deprecate the other one
  2. in 8.22 rename mul_sub_distr_l' into mul_sub_distr_l, keep mul_sub_distr_l' as a (deprecated?) notation
  3. if we deprecate mul_sub_distr_l', then remove it in 8.24
    But, that's quite a lot of things, especially if there is a second deprecation.

A final option is to do nothing, keep inconsistent mul_sub_distr_l.

Does anyone have an opinion and/or advices on this subject?

view this post on Zulip Gaëtan Gilbert (Mar 10 2024 at 10:14):

we could replace in Nat

Lemma mul_sub_distr_l : forall n m p : nat, p * (n - m) = p * n - p * m.

with

#[deprecated(note="do not use")]
Lemma mul_sub_distr_l_old : forall n m p : nat, p * (n - m) = p * n - p * m.
#[deprecated(note="do not use")]
Lemma mul_sub_distr_l_new : forall n m p : nat, n * (m - p) = n * m - n * p.

#[warnings="-deprecated"]
Notation mul_sub_distr_l := ltac:(pick_mul_sub_distr_l mul_sub_distr_l_old mul_sub_distr_l_new).

together with some ocaml code to define the tactic pick_mul_sub_distr_l and an option Use New mul_sub_distr_l such that

and when the tactic runs if the option is false it returns its first argument and warns, otherwise return the second argument.

This should make a single deprecation wave work (the option doesn't need to be deprecated when removed as anything that breaks because of removing it is a tactic call with the option set false ie already warns).

It may be a bit heavy on the implementation side but not too bad I guess.
However it probably doesn't play nice with implicit arguments if any are used, not sure if that can be solved.

view this post on Zulip Pierre Roux (Mar 10 2024 at 10:45):

I guess most of the time, the lemma is used in rewrite without arguments. So there are high chances the deprecation strategy won't even require any action from most users. The one wave deprecations strategy sounds nice but is probably overengineered then.

view this post on Zulip Pierre Rousselin (Mar 10 2024 at 15:11):

@Gaëtan Gilbert Thank you very much for your suggestion. I'm not sure of what we're asking to the user though (with the deprecation warning). Do we want her to set the option to true and fix her library? If that's the case, then we need also to ask her to get rid of the part where she set the option to true, so it's another deprecation warning, right?

view this post on Zulip Gaëtan Gilbert (Mar 10 2024 at 15:51):

If that's the case, then we need also to ask her to get rid of the part where she set the option to true, so it's another deprecation warning

no, at that time we just remove the option
(unknown option is a warning)

view this post on Zulip Pierre Rousselin (Mar 10 2024 at 16:05):

Gaëtan Gilbert said:

If that's the case, then we need also to ask her to get rid of the part where she set the option to true, so it's another deprecation warning

no, at that time we just remove the option
(unknown option is a warning)

Thanks! I did not know it. Maybe it would be worth spending some time on it, since it is something that should arise frequently? Do you have pointers about how to write such a tactic in OCaml?


Last updated: Oct 13 2024 at 01:02 UTC