## Stream: Coq users

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

#### 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?

#### 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 * _).

#### WKroneman (Aug 29 2020 at 18:04):

Oooh, you can search like that?

#### 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).

#### WKroneman (Aug 29 2020 at 18:08):

Yeah, that did something. Thanks!

#### WKroneman (Aug 29 2020 at 18:16):

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

#### WKroneman (Aug 29 2020 at 18:16):

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

#### Pierre-Marie Pédrot (Aug 29 2020 at 18:16):

the ring tactic should solve this...

#### Jasper Hugunin (Aug 29 2020 at 18:19):

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

Proof. intros.
unfold Rsqr.
ring.
Qed.

Oh...

#### Pierre-Marie Pédrot (Aug 29 2020 at 18:20):

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

#### 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.

#### WKroneman (Aug 29 2020 at 18:25):

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

Last updated: Oct 04 2023 at 23:01 UTC