如何在 Coq 中自动证明实数的简单相等性？

Question

我正在寻找的是一种类似于 auto 的策略，它可以证明简单的等式，例如：

1/2 = 2/4

到目前为止，我手动尝试的是使用 ring_simplify 和 field_simplify 来证明等式。即使这样效果也不佳（Coq 8.5b3）。下面的示例有效：

Require Export Coq.Reals.RIneq.
Local Open Scope Z_scope.
Local Open Scope R_scope.

Example test2: 1 = 1 / 1.
Proof. field_simplify. field_simplify. reflexivity.
Qed.

但是在reflexivity之前需要用field_simplfy两次。第一个 field_simplfiy 给我：

1 subgoal
______________________________________(1/1)
1 / 1 = 1 / 1 / (1 / 1)

不受自反性影响。

下面的例子不成立，field_simplify似乎对目标没有任何作用，因此，reflexivity不能使用。

Example test3: 1/2 = 2/4.
Proof. field_simplify. reflexivity.

同样，有没有自动的方法来实现这个，比如 field_auto？

Answer 1

我相信战术field就是你想要的。

Require Export Coq.Reals.RIneq.
Local Open Scope Z_scope.
Local Open Scope R_scope.


Example test3: 1/2 = 2/4.
Proof.  field. Qed.

如何在 Coq 中自动证明实数的简单相等性？

How to automatically prove simple equality of real numbers in Coq?

coq

coq-tactic

real-number