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?

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

Oooh, you can search like that?

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

Yeah, that did something. Thanks!

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

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

the `ring`

tactic should solve this...

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

`Search (Rsqr (_ + _)).`

also brings up an interesting lemma.

```
Proof. intros.
unfold Rsqr.
ring.
Qed.
```

Oh...

When doing numerical proofs, `ring`

, `field`

and `lia`

are your best friends.

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.

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

Last updated: Oct 04 2023 at 23:01 UTC