勒柯克的强制和目标匹配

假设我有以下设置：勒柯克的强制和目标匹配

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）。这缓解了这个问题，但是一旦引入了新的强制措施，策略就不知道了。

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

这可能吗？如果不是，有没有理由不可能？

来源

2017-08-03 frececroka

您可以直接声明构造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-03 11:52:19 gallais

也有语法糖的情况下构造函数是强制的：'Inductive exp：Set：= | CE：> nat - > exp.'会自动声明'CE'为强制（注意我使用'：>'而不是'：'来代替'CE'）。 –

谢谢你，这些都是非常优雅的解决方案，并且明显比我在问题中使用的更好。但在我的具体情况中，我必须解决家庭作业的任务，并且必须处理由讲师提供的数据类型定义和强制。改变这些定义不是一种选择。我想我会在强制手段中使用额外的分支。 – frececroka

@frececroka你也可以使用例如'cbv delta.'在模式匹配之前展开透明定义。那么你原来的'my_tactic'就可以工作。 –

勒柯克的强制和目标匹配

回答

相关问题