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:
mul_sub_distr_l'
in natural types with the Z
interface, deprecate the other onemul_sub_distr_l'
into mul_sub_distr_l
, keep mul_sub_distr_l'
as a (deprecated?) notationmul_sub_distr_l'
, then remove it in 8.24A 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
false
true
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