Как автоматически доказать простое равенство действительных чисел в Coq?

Я ищу 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?


coq coq-tactic real-number
person tinlyx    schedule 21.12.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Я считаю, что эта тактика 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.
person Rodrigo Ribeiro    schedule 21.12.2015