1

假设我有以下设置：

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）。这稍微缓解了问题，但是一旦引入了该策略不知道的新强制，就会失败。

理想情况下，如果在展开所有定义后模式匹配，我希望模式匹配成功（当然，定义不应保持展开）。

这可能吗？如果不是，有什么理由不可以吗？

4

1 回答 1

2

您可以直接将构造函数声明CE为强制，而不是nat_to_exp像这样包装它：

Coercion CE : nat >-> exp.

然后证明通过，没有任何问题。如果你坚持命名你的强制转换（例如，因为它是一个复合表达式而不是单个构造函数），你可以改变你的策略，让它显式地处理非展开的强制转换：

Ltac my_tactic := match goal with
| [ |- adt (CE ?N) ] => apply (CA (CE N))
| [ |- adt (nat_to_exp ?N) ] => apply (CA (CE N))
end.
于 2017-08-03T11:52:19.990 回答