Как автоматически доказать простое равенство действительных чисел в 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. 

Но надо было использовать field_simplfy дважды до reflexivity, Первый 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.