如何创建自定义Ltac以递归析取复合合取式？

我经常需要处理(Q /\ W) /\ (E /\ R)这类复杂合取式，手动析取并猜测方括号排列方式既繁琐又容易误删内容。我想编写一个自定义Ltac，像repeat split处理目标那样自动拆解复合合取式，期望效果如下：

Theorem test : forall {Q W E R : Prop}, (Q /\ W) /\ (E /\ R) -> True.
Proof.
  intros Q W E R.
  intro H.
  smart_destruct H.
  (*
    HQ : Q
    HW : W
    HE : E
    HR : R
    ------------------
    True
  *)
Admitted.

我编写的代码如下，但运行时出现错误Error: Expression does not evaluate to a tactic.：

Ltac smart_destruct H
  := match H with
     | _ /\ _ => destruct H as [?L ?R]; smart_destruct L; smart_destruct R
     | _ => H
     end.

我想知道是否有现成tactic可实现该功能，更重要的是希望了解如何正确编写这个自定义Ltac，我的代码哪里出错了？

现成的替代方案 #

• Coq标准库自带的destruct_all（默认导入Coq.Init.Tactics即可使用），直接执行destruct_all conj就能自动拆解所有嵌套的合取式，将每个子命题单独作为假设。
• 也可以用手动重复匹配的方式：repeat match goal with H : _ /\ _ |- _ => destruct H end，无需额外导入，同样能完成自动拆解。

代码错误原因与修正 #

你的Ltac存在两个关键问题：

1. 匹配对象错误：match H with是在匹配假设的标识符（比如H这个名字），而非假设的类型（合取式）。需要针对假设的类型进行匹配，可通过type of H获取类型。
2. 非合取分支无效：当匹配到非合取式时，返回的H不是合法tactic，这里应使用idtac（空操作tactic）表示不执行任何操作。

修正后的指定假设版本 #

Ltac smart_destruct H :=
  match type of H with
  | _ /\ _ => destruct H as [?L ?R]; smart_destruct L; smart_destruct R
  | _ => idtac
  end.

更通用的自动遍历版本 #

如果不想每次指定假设名，可以让tactic自动扫描目标中的所有合取假设并拆解：

Ltac smart_destruct :=
  repeat match goal with
         | H : _ /\ _ |- _ => destruct H as [? ?]
         end.

使用时直接输入smart_destruct即可，无需指定假设，它会自动完成所有嵌套合取的拆解。

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