CoqIde中的“环”策略不被接受

Question

我正在学习Coq，我需要第一次使用ring战术。我尝试在Require Ring.或Require ArithRing.之后使用它来简化作为目标的方程的右侧，但是Coq将它作为一个不存在的引用。我在这里复制我的代码(我已经尝试过多次使用ring和ring_simplify)：

Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.

(* sum_n n is inductively defined as the sum of all numbers between 1 and n *)

Proof.
intros n.
induction n as [ |m IHm].
+simpl.
reflexivity.
+assert (SnSn : S m * S m = m * m + 2 * m + 1).
ring_simplify in [S m * S m = m * m + 2 * m + 1]. (*or just ring. , neither works*)
rewrite SnSn.
rewrite <- IHm.
simpl.
ring.
Qed.

Answer 1

要调用这些策略，您需要导入这些模块，而不仅仅需要它们：

Require Import ArithRing Ring.

添加了这些行后，我试着运行您的验证，但是Coq陷入了另一个错误。在Coq接受脚本之前，您可能仍然需要调整它。