为什么使用 Coq 的 setoid_replace "by" 子句需要额外的 idtac？

Question

我在使用 setoid_replace 时遇到了一个奇怪的情况，其中证明步骤的形式为：

setoid_replace (a - c + d) with b by my_tactic

因 Error: No matching clauses for match goal 失败，但在向策略附加额外的 idtac 后：

setoid_replace (a - c + d) with b by (my_tactic; idtac)

证明成功。我对 idtac 的理解是它本质上是一个空操作。为什么 idtac 的存在在这里有所不同？

这是完整的代码。我通过 Proof General 使用 Coq 8.4pl6。

Require Import QArith.
Open Scope Q.

Lemma rearrange_eq_r a b c d :
  a == b  ->  b + d == a + c  ->  c == d.
Proof.
  intro a_eq_b; rewrite a_eq_b; symmetry; now apply Qplus_inj_l with (z := b).
Qed.

Ltac rearrange :=
  match goal with
  | [ H : _ == _ |- _ == _ ] => apply rearrange_eq_r with (1 := H); ring
  end.

Lemma test_rearrange a b c d e (H0 : e < b) (H1 : b + c == a + d) :  e < a - c + d.
Proof.
  (* Why is the extra 'idtac' required in the line below? *)
  setoid_replace (a - c + d) with b by (rearrange; idtac).
  assumption.
Qed.

注意：正如 Matt 观察到的，idtac 在这里似乎并不特别：似乎任何策略（包括 fail！）都可以用来代替 idtac使证明成功。

Answer 1

感谢 Coq 错误跟踪器上的 Jason Gross 对此进行了解释。这与 Ltac 策略语言中的求值顺序有关。在失败的情况下，rearrange 中的匹配应用于直接目标中的不等式，而不是 setoid_replace 生成的等式。以下是 Jason 对错误报告的回复：

This is because the [match] is evaluated before the [setoid_replace] is run. It is one of the unfortunate trip-ups of Ltac that things like [match] and [let ... in ...] are evaluated eagerly until a statement with semicolons, or other non-match non-let-in statement is reached. If you add [idtac; ] before the [match] in [rearrange], your problem will go away.

为什么使用 Coq 的 setoid_replace "by" 子句需要额外的 idtac？

Why does use of Coq's setoid_replace "by" clause need an extra idtac?

coq