我正在寻找的是auto类似的策略可以证明简单的等式，例如：
1/2 = 2/4
到目前为止，我手动尝试过的是使用ring_simplify and 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 twice before 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?
我相信这个战术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.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
