How to simplify real number terms in Coq?

Question

I am trying to do simple proofs for real numbers with Coq. For example, I want to prove the average of two non-negative numbers is also non-negative.

Example test: forall r1 r2:R, r1 >= 0 -> r2 >= 0 -> (r1 + r2)/2 >= 0.

My first step is to prove r1 + r2 >=0 as follows.

Require Export Coq.Reals.RIneq.
Require Export Coq.Reals.R_sqrt.

Local Open Scope Z_scope.
Local Open Scope R_scope.

Example test: forall r1 r2:R, r1 >= 0 -> r2 >= 0 -> (r1 + r2)/2 >= 0.
Proof. intros. 
  assert (r1 + r2 >= 0 + 0).
  apply Rplus_ge_compat; assumption. simpl in H1. 

However, I can only get

...
H1 : r1 + r2 >= 0 + 0
______________________________________(1/1)
(r1 + r2) / 2 >= 0

in the hypothesis. I can't change 0 + 0 on the RHS of H1 to 0. I tried simpl in H1. as shown and it did nothing. I understand that real numbers are different from nat. But how should I simplify things here?

(Note: I am beginner at real numbers. And the code above may be naive/inefficient. Suggestions for improvement are welcome. ) Also:

Rplus_ge_compat
     : forall r1 r2 r3 r4 : R,
       r1 >= r2 ->
       r3 >= r4 -> r1 + r3 >= r2 + r4

Answer 1

The real numbers in Coq's standard library are axiomatic and as such do not compute. But you can rewrite by some theorems to simplify the expression:

rewrite Rplus_0_r in H1.

Or rely on tactics applying various rewrite steps to turn expressions into a normal form. To simplify expressions on a ring, you may use ring_simplify.

ring_simplify in H1.

If you are not limited to ring operations but also have fractions, you can use field_simplify instead (in this case it won't lead to the normal form you are looking for):

field_simplify in H1.

Another possibility is to use replace ... with ... to state precisely what you want replaced and by what you want it replaced. If you readily know how to prove that the two expressions are equal replace ... with ... by ... will let you discharge that constraint immediately.

replace (0 + 0) with 0 in H1 by ring.