Coq强制和目标匹配

Inductive exp: Set :=
| CE: nat -> exp.

Inductive adt: exp -> Prop :=
| CA: forall e, adt e.

Coercion nat_to_exp := CE.

Ltac my_tactic := match goal with
| [ |- adt (CE ?N) ] => apply (CA (CE N))
end.

我试图用自定义策略证明一个简单的定理:

Theorem silly: adt 0.
Proof.
  my_tactic. (* Error: No matching clauses for match. *)
Abort.

这失败了,因为目标不符合形式 adt (CE ?N) 但形式 adt (nat_to_exp ?N) (这在使用时明确显示。) Set Printing Coercions

Theorem silly: adt (CE 0).
Proof.
  my_tactic. (* Success. *)
Qed.

我知道可能的解决方法:

• 不使用强制手段。
• 在战术中展开胁迫(使用 unfold nat_to_exp ). 这稍微缓解了问题,但一旦引入了该策略不知道的新强制,就失败了。

理想情况下,如果模式在展开所有定义后匹配,我希望模式匹配成功(当然,定义不应该保持展开状态)。