WKroneman (Aug 29 2020 at 17:52): 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...
Pierre-Marie Pédrot (Aug 29 2020 at 18:17):https://coq.inria.fr/refman/addendum/ring.html?highlight=ring#coq:tacn.ring
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: Oct 13 2024 at 01:02 UTC