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?
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
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.
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.
And yes, the Q arithmetic in the standard library needs some enhancements.
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?
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.
To get the ball rolling! https://github.com/coq/coq/issues/14066
Last updated: Jan 31 2023 at 14:03 UTC