檢查evars的策略，返回一個值

Question

我試圖寫一個策略，返回一個值，並在這樣做的過程中，它需要檢查是否是一個evar。

不幸的是，我不能使用is_evar，因爲那時策略不被視爲返回一個值（而是另一種策略）。下面是一個例子。

有什麼建議嗎？

Ltac reify_wrt values ls := 
    match ls with 
    | nil => constr:(@nil nat) 
    | ?a :: ?ls' => let i := lookup a values in 
       let idx := reify_wrt values ls' in 
       constr:(i :: idx) 
    | ?e :: ?ls' => is_evar e; 
        let i := constr:(100) in 
        let idx := reify_wrt values ls' in 
        constr:(i :: idx) 
    end. 

Answer 1

有一個整潔（或討厭）的小技巧，你可以用它來插入策略執行到consq構造中，在Coq> = 8.5中：將它包裝在match goal中。

 
Ltac reify_wrt values ls := 
    match ls with 
    | nil => constr:(@nil nat) 
    | ?a :: ?ls' => let i := lookup a values in 
       let idx := reify_wrt values ls' in 
       constr:(i :: idx) 
    | ?e :: ?ls' => let check := match goal with _ => is_evar e end in 
        let i := constr:(100) in 
        let idx := reify_wrt values ls' in 
        constr:(i :: idx) 
    end. 

---

由於編程語言的奧祕讓我着迷，我現在就告訴你，比你可能是有史以來想知道LTAC的現在和過去的執行模式。

戰術評估有兩個階段：戰術表現評估和戰術運行。在戰術運行，排序，細化，重寫等過程中，執行。在策略表達式求值，下面的結構進行評估，如果在表達手法的頭部位置發現：

• 戰術呼叫解決/其次/內嵌/展開
• let ... in ...結合它的表現評價的說法的名稱，並執行替代
• constr:(...)被評估和檢查類型
• lazymaytch ... with ... end進行評估（背部跟蹤），並返回第一匹配分支成功地表達，評估
• match ... with ... end評估（回溯）和分支熱切執行。請注意，在這張圖片中，match很奇怪，因爲它強制執行策略提前。如果您見過Coq < 8.5中的「本地定義中不允許的立即匹配生成策略」，那是明確禁止我在上面利用的行爲的錯誤消息。我猜這是因爲match這個奇怪的行爲是一個實施Ltac的原始開發者想要隱藏的疣。因此，您可以在Coq 8.4中注意到的唯一地方是，如果您在lazymatch之內堅持match並使用失敗級別，並且注意lazymatch會在您通常預期失敗時在內部match內策略執行失敗時回溯。

在Coq 8.5中，戰術引擎被重寫以處理相關的子目標。這引起了;的語義的微妙變化，這些變化只有在使用在多個目標之間共享的evars時才能被觀察到。在重寫中，開發人員將lazymatch的語義更改爲「無回溯」的「match」，並取消了「立即匹配生成策略」的限制。因此，你可以做奇怪的事情，如：

let dummy := match goal with _ => rewrite H end in 
constr:(true) 

，並有副作用構造生產策略。然而，你可以不再做：

let tac := lazymatch b with 
       | true => tac1 
       | false => tac2 
       end in 
tac long args. 

因爲勒柯克> = 8.5，lazymatch也急切地評估它的分支。

Answer 2

這是LTAC的一個衆所周知的限制：你不能寫一個戰術，有時會返回一個值，有時返回另一個策略。解決方案是重寫你的戰術延續傳球風格。不幸的是，我不能給你詳細的解釋，但Adam Chlipala的CDPT有一個描述問題的chapter on Ltac;只需在文本中尋找「延續」即可。