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

Question

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

1/2 = 2/4

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.

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.

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.

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

Rodrigo Ribeiro Rodrigo Ribeiro · Accepted Answer · 2015-12-21T01:47:01

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.

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

1 Answers