当 `rewrite` 工作时 `rewrite at` 失败

Question

当我键入 rewrite <- […] 时，该命令会替换目标中引理的两次出现，当我输入 rewrite <- […] at 2 时，它会重写第二个实例。

但是，当我写 rewrite <- […] at 1 时，出现以下错误：

Error: Tactic failure: Unable to satisfy the rewriting constraints.
Unable to satisfy the following constraints:
[…]

更具体地说：

Goal: (e) · (e') = e.
Hypothesis inverse_left : forall x : G, (inv x)·x = e.

rewrite <- (inverse_left x) at 1.

编辑:

最小（最终工作）示例：

(* Required for `rewrite at`. *)
Require Setoid.

Section Whosebug.

Variable G : Set.
Variable prod : G -> G -> G.
(* I have no idea which level to choose *)
(* 80 is too much (binds weaker than `=`) *)
(* 0 is too little *)
Infix "·" := prod (at level 30).
Variable e : G.
Variable inv : G -> G.

Hypothesis inverse_left : forall x : G, (inv x)·x = e.
Goal forall x e' : G, e·e' = e.
intros x e'. rewrite <- (inverse_left x) at 1.

Coq 版本：

The Coq Proof Assistant, version 8.4pl5 (February 2015)
Architecture Linux running Unix operating system
Gtk version is 2.24.25
This is coqide.opt (opt is the best one for this architecture and OS)

Answer 1

在此处创建 post 的最小测试示例后，我注意到最小示例有效。但是，仔细检查了原代码，还是报了上面的错误。

该问题的解决方案相当平庸——在重新打开看似错误的代码并重新检查后，先前被拒绝的证明被接受了。

我想这是因为 coqide 保持打开它用于检查证明的 coq 实例，导致拒绝，因为 coq 实例可能是由于之前的输入错误。

TL;DR: 解决方案：重新打开 coqide 以解决此问题。

当 `rewrite` 工作时 `rewrite at` 失败

`rewrite at` fails when `rewrite` works

coq