3

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

在假设中。我无法将0 + 0H1 的 RHS 更改为0. 我尝试simpl in H1.了如图所示，它什么也没做。我知道实数不同于nat. 但是我应该如何简化这里的事情？

（注意：我是实数初学者。上面的代码可能很幼稚/效率低下。欢迎提出改进建议。）另外：

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

1 回答 1

3

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.
于 2015-12-20T19:49:34.230 回答