我正在尝试使用Coq证明实数的简单定理。例如,我希望证明两个非负数的平均值也是非负的。
Example test: forall r1 r2:R, r1 >= 0 -> r2 >= 0 -> (r1 + r2)/2 >= 0.
我的第一步是证明r1 + r2 >=0
,如下所示。
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.
然而,我只能获得
...
H1 : r1 + r2 >= 0 + 0
______________________________________(1/1)
(r1 + r2) / 2 >= 0
在这个假设中,我无法将 H1 右侧的
0 + 0
改为 0
。我尝试了如下的 simpl in H1.
,但没有任何变化。我知道实数与自然数不同。但我应该如何在这里简化呢?(注:我是实数方面的初学者。上面的代码可能很幼稚/低效。欢迎提出改进意见。)
Rplus_ge_compat
: forall r1 r2 r3 r4 : R,
r1 >= r2 ->
r3 >= r4 -> r1 + r3 >= r2 + r4