Rbar / Rbar_le / coquelicot lemma

Question

I am learning Coq via the Coq 8.12.0 reference manual, and have trouble proving the following lemma.

From Coq Require Import Lia Reals Lra List.

Lemma lemma1 : forall (x y:Rbar), Rbar_le x 0 -> Rbar_le y 0
   -> Rbar_le (Rbar_plus x y) 0.

Proof.
destruct x ; destruct y ; simpl ; intuition.
destruct H.
destruct H0.
unfold Rle.
auto with real.
right.
...

And then I get stuck to finish the proof. Any ideas ?

Answer 1

When you entered the tactic right you made a choice in the proof that is not confirmed by the facts in your hypothesis. You should remove this line, and try to find another way to prove your initial conjecture, which really seems provable.

Actually, you are entering into too much detail if you start unfolding the definition of Rle and using destruct. The goal after your ...; intuition is as follows:

1 subgoal (ID 207)

  r, r0 : R
  H : r <= 0
  H0 : r0 <= 0
  ============================
  r + r0 <= 0

This is a goal of simple linear arithmetic (because we only add variables together and use simple comparisons). This is solved by a powerful tactic called lra. Just call it. The full script for your proof is here:

Lemma lemma1 : forall (x y:Rbar), Rbar_le x 0 -> Rbar_le y 0
   -> Rbar_le (Rbar_plus x y) 0.

Proof.
destruct x ; destruct y ; simpl ; intuition.
lra.
Qed.