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:

- in 8.20, add a
`mul_sub_distr_l'`

in natural types with the`Z`

interface, deprecate the other one - in 8.22 rename
`mul_sub_distr_l'`

into`mul_sub_distr_l`

, keep`mul_sub_distr_l'`

as a (deprecated?) notation - 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?

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

- in 8.20 the option defaults
`false`

- later it defaults
`true`

- even later it and the tactic are removed and mul_sub_distr_l_new is renamed to mul_sub_distr_l

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.

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.

@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?

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)

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