Ltac中尝试策略失败后继续运行的实现及空策略查询

空策略说明 #

Ltac 中的空操作策略是 idtac，无参数调用时不会修改任何证明状态，且必然执行成功，完全满足你“什么都不做”的需求。

需求实现方案 #

你需要的「尝试执行 rewrite H，失败则跳过，之后统一执行 apply lemma1」的逻辑，最简洁的写法如下：

all: try rewrite H; apply lemma1.

语法说明： #

• try <tactic> 是 Ltac 原生支持的语法，语义就是尝试执行指定策略，如果策略执行失败就等价于执行空操作，不需要你手动拼接|| idtac的分支
• all: 前缀表示后续的策略块会作用于当前所有存在的子目标，刚好匹配你两个分支的处理需求

如果你想要显式使用空策略写也可以，效果完全一致：

all: (rewrite H || idtac); apply lemma1.

之前尝试的问题说明 #

1. 你的第一种写法try (rewrite H || nil); apply lemma1.仅需要将nil替换为idtac即可正常运行
2. 你的第二种写法do 2 try (rewrite H; apply lemma1 || apply lemma1)无法生效的核心原因是：do 2默认仅作用于当前第一个子目标，重复执行两次只会处理第一个目标，第二个子目标全程没有被操作，因此无法完成证明。

Ltac 内容查询方法 #

你可以查阅 Coq 官方参考手册的 Ltac 内置策略章节，所有标准策略的语法、语义都有完整的官方说明，常见基础用法都可以在该章节检索到。

内容的提问来源于stack exchange，提问作者sdpoll