Coq战术是右联想还是左联想?

问题描述

我正在经历软件基础，并得到了示例:

I was going through software foundations and got the example:

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

，这很困惑.例如，我们得到了吗?

and was confused what this meant. For example do we get:

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.

推荐答案

自行解决这些问题的一种好方法是使用idtac(总是成功)和fail(总是失败)之类的策略来消除歧义:

A good way of solving those problems on your own is to use tactics like idtac (always succeeds) and fail (always fails) to disambiguate:

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

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

So indeed, the application of try binds tighter than the semicolon:

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

这篇关于Coq战术是右联想还是左联想?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！