如何在Coq中简化实数项？

Question

我正在尝试使用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

- thor

Answer 1

Coq标准库中的实数是公理化定义的，因此不能进行计算。但是可以通过一些定理重写表达式以简化其形式：

rewrite Rplus_0_r in H1.

或者依靠应用各种重写步骤将表达式转化为正常形式。要简化环上的表达式，您可以使用ring_simplify。

ring_simplify in H1.

如果您不仅限于环操作还包括分数，您可以使用field_simplify代替（在这种情况下，它不会导致您正在寻找的正常形式）：

field_simplify in H1.

另一种可能性是使用replace ... with ...来精确说明您想要替换的内容以及您想要将其替换为的内容。如果您已经知道如何证明这两个表达式相等，replace ... with ... by ...将立即让您满足此约束条件。

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

- gallais