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?
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.
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.
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"
Thanks - I will try again tomorrow then.
looks like it works now
Last updated: Dec 05 2023 at 05:01 UTC