## Stream: Coq users

#### Karolin Varner (Apr 01 2021 at 15:18):

I can't find `forall (a b : Z) (d : positive), a=b <-> (a#d)==(b#d).`; neither can I find `forall (a b z: positive), a*z=b*z <-> a=b` nor `forall (a b z : Z), z>0 -> a*z=b*z <-> a=b` which would have been useful writing the first proof myself…am I missing something here? I would have expected to find these in the stdlib?

#### Michael Soegtrop (Apr 01 2021 at 17:30):

I proved various assorted Q lemmas when working on reals - unfortunately I didn't have time yet to put them where they belong. You find them in `theories/Reals/Cauchy/QExtra.v`.

As you can see there, such things are easy to prove by unfolding the definitions of Q arithmetic which brings you to Z arithmetic and then using lia or ring.

#### Michael Soegtrop (Apr 01 2021 at 17:40):

An example proof for your first question:

``````Goal forall (a b : Z) (d : positive),  a=b <-> (a#d)==(b#d).
intros a b d.
unfold Qeq. cbn. symmetry.
apply Z.mul_cancel_r.
lia.
Qed.
``````

#### Michael Soegtrop (Apr 01 2021 at 17:42):

And yes, the Q arithmetic in the standard library needs some enhancements.

#### Karolin Varner (Apr 01 2021 at 18:11):

Much obliged; that's about 25 lines more impressive than my proof! Would it be a bad idea for me to just open PRs for lemmas like these?

#### Michael Soegtrop (Apr 01 2021 at 19:14):

I think it would make more sense to make an inventory and a proper plan than spot issues. I actually thought about cleaning up the file I mentioned above and distributing it into the proper places and filling gaps. The QExtra file has lemmas which I needed in some Reals proofs only. If you have a list of lemmas which are missing, that would be a good start. An important question is also how to name the lemmas. I would enjoy a discussion on this topic.

#### Karolin Varner (Apr 04 2021 at 10:06):

To get the ball rolling! https://github.com/coq/coq/issues/14066

Last updated: Jun 23 2024 at 01:02 UTC