Stream: Coq users

Topic: Q_ad_equiv_bd_elim


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

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

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

view this post on Zulip Michael Soegtrop (Apr 01 2021 at 17:42):

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

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

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

view this post on Zulip Karolin Varner (Apr 04 2021 at 10:06):

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


Last updated: Jan 31 2023 at 14:03 UTC