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 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.
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: Oct 13 2024 at 01:02 UTC