如何在Ltac中无需枚举构造函数，匹配构造函数的至少一层应用？

我们可以借助Coq内置的is_constructor Ltac谓词，实现一个无需枚举所有构造函数的策略，自动将指定tactic应用到等式至少一侧是构造函数应用的假设上（比如0 = m、S n = m这类假设，而n = m这类两边都是变量的假设不处理）。

核心实现 #

Ltac apply_to_constructor_hyps tac :=
  repeat match goal with
         | H: ?lhs = ?rhs |- _ =>
             (is_constructor ?lhs || is_constructor ?rhs); tac H
         end.

代码解释 #

• repeat：循环执行内部匹配逻辑，直到没有符合条件的假设可处理。
• match goal with：遍历当前证明目标中的所有假设。
• H: ?lhs = ?rhs |- _：匹配形式为等式的假设H，?lhs和?rhs分别代表等式的左右两边。
• (is_constructor ?lhs || is_constructor ?rhs)：判断等式任意一侧是否为构造函数应用（包括0元构造函数如自然数的O，以及带参数的构造函数如S n），只要满足其一就触发后续操作。
• tac H：对符合条件的假设H应用传入的指定tactic。

测试示例 #

以clear作为传入的tactic验证效果：

Goal forall n m : nat, n = m -> S n = m -> 0 = m -> True.
intros n m H1 H2 H3.
(* 当前假设：H1: n = m，H2: S n = m，H3: 0 = m *)
apply_to_constructor_hyps clear.
(* 执行后，H2和H3被清除，仅保留H1 *)
Abort.

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