## Stream: Coq devs & plugin devs

### Topic: Should my Z lemmas go into the standard library?

#### Michael Soegtrop (May 30 2021 at 07:57):

I have quite a few lemmas on Z, e.g. a complete set of interval arithmetic lemmas for known signs and unknown signs for multiplication and division e.g.:

``````Lemma Z_mult_bounds: forall a b amin amax bmin bmax : Z,
amin <= a <= amax ->
bmin <= b <= bmax ->
Z_min4 (amin*bmin) (amin*bmax) (amax*bmin) (amax*bmax) <= a*b <= Z_max4 (amin*bmin) (amin*bmax) (amax*bmin) (amax*bmax).

Lemma Z_div_bounds_nonneg_neg: forall a b amin amax bmin bmax : Z,
0 <= amin ->
bmax < 0 ->
amin <= a <= amax ->
bmin <= b <= bmax ->
(amax + bmax - bmin) / bmax <= a/b <= (amin + bmin - bmax) / bmin.
``````

or things like:

``````Lemma Z_div_den_opp_pos: forall a b : Z,
b > 0 ->
a / - b = - ((a + b - 1)/ b).

Lemma Z_div_den_opp_neg: forall a b : Z,
b < 0 ->
a / - b = - ((a + b + 1)/ b).
``````

(the standard library has lemmas for `a/-b` but one needs to know if `a mod b` is zero, while for mine one needs to know the sign of b). I find such stuff surprisingly tedious to prove, even with lia.

I wonder if I should put this into the standard library, or if this is too specific. Is there something like a "standard library call" as there is a "Coq call" where such things are discussed?

#### Théo Zimmermann (May 30 2021 at 10:15):

Is there something like a "standard library call" as there is a "Coq call" where such things are discussed?

There could be. @Emilio Jesús Gallego Arias has proposed the idea of having regular thematic WG. See https://github.com/coq/coq/wiki/Topic-Working-Groups. You could launch one with interested stakeholders.

#### Michael Soegtrop (Jun 02 2021 at 08:36):

I tried 2x to create a new Wiki page for a new group but either I am doing something silly or it is broken - if I go to the preview for a new page it says "preview generation failed" and when I save the page I get an error. I really do only very simple markdown. Any ideas? I am using Safari on macOS btw.

#### Gaëtan Gilbert (Jun 02 2021 at 08:37):

I think github is bugging, I tried to subscribe to an issue (on a non coq repo) and github ignored me
I tried starring a repo and github said "you are not allowed at this time"

#### Michael Soegtrop (Jun 02 2021 at 08:39):

Thanks - I will try again tomorrow then.

#### Gaëtan Gilbert (Jun 02 2021 at 09:01):

looks like it works now

Last updated: Oct 16 2021 at 07:02 UTC