Stream: Coq devs & plugin devs

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

view this post on Zulip 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_incl0: forall a b amin amax bmin bmax : Z,
  0 <= amin ->
  b <> 0 ->
  bmin < 0 < bmax ->
  amin <= a <= amax ->
  bmin <= b <= bmax ->
  Z.min (amin / bmax) (-amax) <= a / b <= Z.max (amin / bmin) amax.

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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Michael Soegtrop (Jun 02 2021 at 08:39):

Thanks - I will try again tomorrow then.

view this post on Zulip Gaëtan Gilbert (Jun 02 2021 at 09:01):

looks like it works now

Last updated: Oct 13 2024 at 01:02 UTC