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

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

``````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: Jun 16 2024 at 03:41 UTC