Coq：可變參數列表中的Ltac定義？

Question

當試圖創建一個循環可變長度參數列表的Ltac定義時，我在Coq 8.4pl2上遇到以下意外行爲。任何人都可以解釋給我嗎？

Ltac ltac_loop X := 
    match X with 
    | 0 => idtac "done" 
    | _ => (fun Y => idtac "hello"; ltac_loop Y) 
    end. 

Goal True. 
    ltac_loop 0. (* prints "done" as expected *) 
    ltac_loop 1 0. (* prints "hello" then "done" as expected *) 
    ltac_loop 1 1 0. (* unexpectedly yields "Error: Illegal tactic application." *) 

Answer 1

讓我們擴展的ltac_loop最後調用，看看發生了什麼：

ltac_loop 1 1 0 
-> (fun Y => idtac "hello"; ltac_loop Y) 1 0 
-> (idtac "hello"; ltac_loop 1) 0 

在那裏，你可以看到這個問題：你想申請的東西是不是一個說法，這將導致功能在你看到的錯誤中。解決的辦法是改寫延續傳遞風格的戰術：

Ltac ltac_loop_aux k X := 
    match X with 
    | 0 => k 
    | _ => (fun Y => ltac_loop_aux ltac:(idtac "hello"; k) Y) 
    end. 

Ltac ltac_loop X := ltac_loop_aux ltac:(idtac "done") X.