將模式傳遞給策略

Question

我在寫一個策略，它查找與綁定列表中的鍵相關的值。例如：

Require Import String List Program. 

Ltac assoc needle haystack := 
    match haystack with 
    | @nil (_ * ?T) => constr:(@None T) 
    | cons (?k, ?v) ?t => let pr := constr:(eq_refl k : k = needle) in constr:(Some v) 
    | cons _  ?t => let res := assoc needle t in constr:res 
    end. 

不幸的是，我不知道密鑰的確切形式;相反，我知道一個匹配它的模式。更確切地說，我正在尋找的關鍵是調用一個類類方法的結果，但我不知道哪個實例已被使用。在下面的例子中，我知道，關鍵是要show "a"一個電話，但我不什麼情況下知道：

Open Scope string_scope. 
Open Scope list_scope. 

Class Show A := { show: A -> string }. 
Instance Show1 : Show string := {| show := fun x => x |}. 
Instance Show2 : Show string := {| show := fun x => x ++ x |}. 

Goal True. 
    (* Works (poses Some 1) *) 
    let v := assoc (show "a") [(show (Show := Show2) "a", 1); ("b", 2)] in pose v. 
    (* Does not work (poses None) *) 
    let v := assoc (show "a") [(show (Show := Show1) "a", 1); ("b", 2)] in pose v. 

有，我可以在這裏使用一個技巧，短傳assoc的LTAC的那檢查比賽？理想情況下，它看起來像(show (Show := _) "a")，或者(fun inst => show (Show := inst) "a")。

Answer 1

看起來像一個路過的功能很好地工作，實際上是：

Ltac assoc needlef haystack := 
    match haystack with 
    | @nil (_ * ?T) => constr:(@None T) 
    | cons (?k, ?v) ?t => let pr := constr:(eq_refl k : k = needlef _) in constr:(Some v) 
    | cons _  ?t => let res := assoc needlef t in constr:res 
    end. 

Goal False. 
    let v := assoc (fun i => show (Show := i) "a") [(show (Show := Show2) "a", 1); ("b", 2)] in pose v. 
    let v := assoc (fun i => show (Show := i) "a") [(show (Show := Show1) "a", 1); ("b", 2)] in pose v.