如何在自定義策略中利用自動搜索和提示數據庫？

Question

在我的coq開發中，我正在學習如何創建適合我的問題域的新策略，la Prof. Adam Chlipala。在該頁面上，他描述瞭如何通過例如創建強大的自定義策略。結合repeat與match。

現在，我已經有一個強大的一次性使用戰術，auto。它將來自提示數據庫的步驟鏈串起來。我已經投入了一些精力來策劃這些提示數據庫，所以我想繼續使用它。

然而這提出了一個問題。 目前尚不清楚將「auto」的功能納入定製策略的「正確」方法是什麼。

例如，因爲（按其頁面）auto總是要麼解決目標，要麼不做任何事情，把它放在循環內不比在循環之後調用它更強大。

要明白爲什麼這不是理想的，考慮一種假設的方式來直接調用auto的單個「步驟」，如果它可以進行更改（而不是僅在解決目標時）纔會成功，否則將失敗。這樣的單步可以在匹配重複循環中與自定義行爲交織，使我們可以例如try contradiction或try congruence在搜索樹內的中間點。

將auto的功能納入自定義策略是否有良好的設計模式？

可以將auto的行爲分解爲我們可以使用的「單步」策略嗎？

Answer 1

我想要做的就是在auto中加入其他策略。 您可以通過使用Hint Extern num pat => mytactic : mybase.命令執行此操作，其中num是優先級數字（0表示最高優先級），pat應該使用提示時使用的模式，mytactic和mybase當然是您要應用的策略，而要添加提示（不要使用默認的core;建立您的自定義基地，並使用auto with mybase進行調用;如果您不想在搜索中包含來自core基地的引理，請添加假基地nocore ：auto with mybase nocore）。

如果您開始非常依賴auto，我會切換到幾乎等效但性能更好的typeclasses eauto with mybase。與其名稱相反，這是一種通用策略，與類型無關（只要您明確提供它應該工作的提示基礎）。要知道的主要行爲差異之一是默認情況下搜索深度是無限的。因此請注意可能的無限循環或修改typeclasses eauto num with mybase變體的有限極限。欲瞭解更多詳情，請閱讀the manual。