嘿，这个问题我之前写复杂策略的时候也碰到过，刚好有几个实用的方法可以帮到你！

一、在match goal中查找其他相似目标 #

其实match goal本身就支持匹配所有目标，不止当前聚焦的那个。你可以通过模式匹配遍历全部目标，甚至针对特定类型/结构的目标做筛选：

1. 基础遍历与匹配 #

比如你想找所有类型为nat的目标，可以这么写：

match goal with
| [ |- nat ] => idtac "Found a nat goal at current focus"
| [ |- nat ] => idtac "Found another nat goal"
end

match goal会按目标的顺序（从第一个到最后一个）依次匹配，每次匹配到符合模式的目标时，就会执行对应的逻辑。

2. 精准定位特定位置的目标 #

如果要匹配某个特定索引的目标，可以配合nth_goal指令（索引从0开始）：

match nth_goal 1 with  (* 匹配第二个目标 *)
| |- ?T => idtac "Second target type is" T
end

这样就能直接对指定位置的目标做模式匹配，不用遍历全部。

二、目标间的切换方法 #

在Ltac里切换目标有几种常用方式，根据你的场景选就行：

1. goto：直接跳转到指定目标 #

最直观的方法就是用goto指令，传入目标索引（从0开始）就能切换到对应目标：

goto 1;  (* 切换到第二个目标 *)
(* 在这里对第二个目标执行策略，比如auto、rewrite等 *)
goto 0;  (* 切回第一个目标 *)

2. focus + unfocus：聚焦与退出聚焦 #

focus n可以聚焦到第n个目标（n从1开始，注意和索引的区别！），操作完后用unfocus回到所有目标的视图：

focus 2;  (* 聚焦到第二个目标 *)
simpl;    (* 对这个目标执行化简 *)
unfocus;  (* 退出聚焦，回到所有目标 *)

3. swap：交换目标顺序 #

如果你想临时把某个目标移到当前位置，可以用swap交换两个目标的位置：

swap 0 1;  (* 交换第一个和第二个目标的位置 *)
(* 现在原来的第二个目标变成了当前聚焦的第一个目标 *)

三、综合示例：查找并处理相似目标 #

下面是一个简单的示例，遍历所有目标找和当前目标类型相同的目标，并打印提示：

Ltac find_similar_goals :=
  let current_type := match goal with |- ?T => T end in
  do 100 (  (* 假设最多100个目标，按需调整 *)
    next_goal;  (* 切换到下一个目标 *)
    match goal with
    | |- ?T' =>
      if current_type = T' then
        idtac "Found similar target with type" current_type
      else skip
    end
  );
  goto 0.  (* 切回第一个目标 *)

小提示 #

• Coq的目标索引容易搞混：nth_goal和goto用的是从0开始的索引，而focus用的是从1开始的序号，使用时要注意区分。
• 如果你用的是Coq 8.16及以上版本，可以用all_goals指令对所有目标批量执行策略，比如all_goals (auto with arith)会在每个目标上自动尝试算术策略。

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