Stream: Coq users

Topic: Proving a Real number inequality

view this post on Zulip Delta (Sep 12 2022 at 04:42):

Hi there, does anyone have any idea how I might go about proving this goal (and similar types of goals)?
This specific example can be seen to be true if you examine all of the combinations of cases for a > 0, a < 0, b > 0, b < 0. Also plotting the equation on a graphing calculator such as Desmos shows it to be true.

Goal forall a b : R, a <> 0 /\ b <> 0 ->
    Rsqr a * 1484.9 + Rsqr b * 406.1 >= a * b * 25.8.
Proof.
    intros.
    destruct H as [HA HB].
    Admitted.

view this post on Zulip Guillaume Melquiond (Sep 12 2022 at 05:02):

The usual way is to rewrite your polynomial as a weighted sum of squares. Finding the proper squares by hand can be a bit tedious. So, better use the nra tactic from the standard library. (You need to do unfold Rsqr beforehand.)

view this post on Zulip Delta (Sep 12 2022 at 06:02):

the nra tactic seems to be exactly what I was after. It worked a charm. Thanks so much!

Last updated: Sep 26 2023 at 11:01 UTC