如何简化 Coq 中的实数项？答案

【问题标题】：How to simplify real number terms in Coq?如何简化 Coq 中的实数项？
【发布时间】：2015-12-20 19:32:13
【问题描述】：

我正在尝试用 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 的 RHS 上的 0 + 0 更改为 0。如图所示，我尝试了simpl in H1.，但它什么也没做。我知道实数与nat 不同。但是我应该如何简化这里的事情呢？

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

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

【问题讨论】：

标签： coq real-number

【解决方案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.

【讨论】：