为何Ltac无法匹配子句？Coq证明匹配失败问题咨询

问题原因分析 #

你遇到的匹配失败问题，核心来自两个关键点：

1. 显式/隐式参数的语法不匹配
   你定义的Ltac使用了显式的全应用模式 @eq nat t ?Y，但Coq中默认的等式写法（如 n = O）是隐式参数形式（即 eq n O，省略了类型参数 nat）。Ltac的匹配是严格语法匹配，显式的@eq模式无法匹配隐式的eq语法结构，导致找不到符合条件的假设。

2. 变量替换导致的上下文变化
   在部分旧版本Coq中，destruct n eqn: M会直接将变量n替换为构造子O或S m，原变量n会从上下文中消失。此时调用easy_ltac n时，n会被当作未绑定的新变量，而假设M是O = O或S m = S m，语法上与新变量n不匹配，自然触发匹配失败。

解决方法 #

针对上述问题，你可以通过以下方式修改代码：

方法1：使用隐式等式模式匹配

将Ltac改为匹配隐式的等式语法，同时兼容显式写法：

Ltac easy_ltac t := match goal with
  | [Z: t = ?Y |- _ ] => pose ?Y as N  (* 匹配隐式等式 *)
  | [Z: @eq nat t ?Y |- _ ] => pose ?Y as N  (* 兼容显式等式 *)
end.

这种写法能同时匹配n = O（隐式）和@eq nat n O（显式）两种形式，避免语法不匹配的问题。

方法2：保留原变量引用

如果需要确保使用原变量n，可以在destruct前先将n保存为新变量，避免原变量被替换：

Lemma easy: forall (n: nat), (n >= O)%nat.
Proof.
intros n. 
let n0 := fresh n in pose n as n0.  (* 保存原变量为n0 *)
destruct n eqn: M. 
easy_ltac n0.  (* 传入保存的变量n0 *)

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