勒柯克的強制和目標匹配

假設我有以下設置：勒柯克的強制和目標匹配

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'就可以工作。 –

勒柯克的強制和目標匹配

回答

相關問題