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