将模式传递给策略

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.