为什么 Ltac 不匹配该子句？

Question

在以下 Coq 证明中：

Ltac easy_ltac t  := match goal with
  | [Z: @eq nat t ?Y |- _ ] => pose ?Y as N 
  end.

Lemma easy: forall (n: nat), (n >= O)%nat.
Proof.
intros n. destruct n eqn: M.  easy_ltac n. 

我收到错误消息：“没有匹配的匹配子句。”，虽然我有假设

M : @eq nat n O

我不懂为什么。

Answer 1

罪魁祸首是 Y 第二次出现之前的无关?。

如果你只是写它应该工作：

Ltac easy_ltac t := match goal with
  | [Z: @eq nat t ?Y |- _ ] => pose Y as N 
  end.