coq - Coq 战术是右联想还是左联想？

Question

我正在研究软件基础并得到了这个例子：

repeat (try (left; reflexivity); right).

并对这意味着什么感到困惑。例如，我们得到：

try [ (left; reflexivity); right ]

或者

[try (left; reflexivity);] right

第二还是第一？

特别是我试图理解：

Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right).
Qed.

score 3 · Accepted Answer

自己解决这些问题的一个好方法是使用像idtac（总是成功）和fail（总是失败）这样的策略来消除歧义：

try (idtac; idtac); fail.     (* FAILS *)
try ((idtac; idtac); fail).   (* SUCCEEDS *)
(try (idtac; idtac)); fail.   (* FAILS *)

所以确实，try绑定的应用比分号更紧密：

try (idtac; idtac); fail.   is the same as   (try (idtac; idtac)); fail.

1 回答 1