如何使用自動重複自定義策略？

Question

在我的coq開發中，我正在學習如何爲我的問題域創建新的策略，la Prof. Adam Chlipala。

在該頁面上，他描述瞭如何通過圍繞match包裝repeat來創建強大的策略，以響應各種有趣的條件。 repeat然後迭代，允許深遠的推論。

使用的repeat有一個警告（重點煤礦）：

，我們在這裏使用的repeat被稱爲戰術，或戰術組合子。 repeat t的行爲是循環運行t，在所有生成的子目標上運行t，在上運行t，它們的生成的子目標等等。當t在這個搜索樹中的任何一點都失敗時，那個特定的子目標會被稍後的策略處理。 因此，重要的是永遠不要使用repeat，這種策略總是成功的。

現在，我已經有了一個強大的戰術使用，auto。它類似地串聯在一起的步驟鏈，這次從提示數據庫中找到。從auto的頁面：

auto要麼完全解決目標，要麼保持完好無損。 auto和trivial永遠不會失敗。

噓！我已經投入了一些精力策劃auto的暗示數據庫，但似乎我使用repeat僱用他們的戰術被禁止（即，有趣的戰術。）

是否存在的auto一些變化可能出現故障，或否則可以在循環中正確使用？

例如，也許這個變體在「完成目標」時失敗。

編輯：結合auto成環是不是「正確」的方式做到這一點呢（見this），但汽車的一個失敗的版本實際的問題仍然是可能有趣。

Answer 1

正如@安頓特魯諾夫所說，如果目標沒有改變，你總是可以使用progress戰術來使戰術失敗。在auto的情況下，因爲它應該解決目標或保持不變，您還可以將其包裝在solve [ auto ]中，這將具有相同的效果，因爲如果auto完全不能完全解決目標（here is the doc for solve），它將會失敗。