如何自动证明Coq中的实数简单相等？ [英] How to automatically prove simple equality of real numbers in Coq?

问题描述

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

What I am looking for is an auto-like tactic that can prove simple equalities like:

1/2 = 2/4

到目前为止，我是手动尝试使用 ring_simplify 和 field_simplify 证明平等。即使这样也不行（Coq 8.5b3）。下面的示例起作用：

So far, what I've tried manually is to use ring_simplify and field_simplify to prove equalities. Even this doesn't work out well (Coq 8.5b3). The example below works:

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. 

但是必须使用 field_simplfy <在自反性之前先进行strong>两次操作。第一个 field_simplfiy 给我：

But it was necessary to use field_simplfy twice before reflexivity. The first field_simplfiy gives me:

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

which is not subject to reflexivity.

下面的示例不起作用， field_simplify 似乎不起作用目标，因此不能使用自反性。

The example below does not work, field_simplify seems to do nothing on the goal, and therefore, reflexivity can't be used.

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

还是有一种自动的方法来实现这一点，例如 field_auto ？

Again, is there an automatic way to achieve this, like an field_auto?

推荐答案

我相信战术字段就是您想要的。

I believe that tactic field is what you want.

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中的实数简单相等？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！