Stream: Coq users

Topic: How to prove a * a + a * b + b * a + b * b = a * a + 2 * a *


view this post on Zulip WKroneman (Aug 29 2020 at 17:52):

Hello, I am trying to prove a small lemma about some reals: https://pastebin.com/nifyhv5g

How do I proceed from here? Can I somehow unfold the 2 * a * b on the right-hand side into a sum of two terms?

view this post on Zulip Jasper Hugunin (Aug 29 2020 at 18:01):

In that context, I see a lemma double, or Reals.RIneq.double, which seems to be what you are looking for. I found that lemma with Search (2 * _).

view this post on Zulip WKroneman (Aug 29 2020 at 18:04):

Oooh, you can search like that?

view this post on Zulip Jasper Hugunin (Aug 29 2020 at 18:08):

Yep, the Search command is very useful and very powerful. See https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.search for the documentation. The one caveat I might raise is that it will only find lemmas in modules you have required (recursively).

view this post on Zulip WKroneman (Aug 29 2020 at 18:08):

Yeah, that did something. Thanks!

view this post on Zulip WKroneman (Aug 29 2020 at 18:16):

Victory! However, is there an easier way than this? https://pastebin.com/JBZHkByb

view this post on Zulip WKroneman (Aug 29 2020 at 18:16):

I kinda get the feeling that I'm missing something really silly and obvious.

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 18:16):

the ring tactic should solve this...

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 18:17):

https://coq.inria.fr/refman/addendum/ring.html?highlight=ring#coq:tacn.ring

view this post on Zulip Jasper Hugunin (Aug 29 2020 at 18:19):

Search (Rsqr (_ + _)). also brings up an interesting lemma.

view this post on Zulip WKroneman (Aug 29 2020 at 18:19):

Proof. intros.
  unfold Rsqr.
  ring.
Qed.

Oh...

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 18:20):

When doing numerical proofs, ring, field and lia are your best friends.

view this post on Zulip WKroneman (Aug 29 2020 at 18:22):

I didn't doubt there was a lemma for the whole thing at once, it's a pretty standard equality. I just haven't really worked with reals in Coq before. But thanks! I'll keep an eye on those three tactics.

view this post on Zulip WKroneman (Aug 29 2020 at 18:25):

Does Coq have library support for points/vectors and such?


Last updated: Jan 27 2023 at 01:03 UTC