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

(注：我是实数初学者，上面的代码可能是naive/inefficient，欢迎提出改进建议。) 还有：

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

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.

如何简化 Coq 中的实数项？

How to simplify real number terms in Coq?

coq

real-number