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

Question

我在使用 setoid_replace 时遇到了一个奇怪的情况，其中的证明步骤如下:

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

因错误:没有匹配目标的匹配子句而失败，但是在将额外的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.