如何检查策略生成术语的可兑换性？

Question

假设我有以下策略来检查项是字面零：

Ltac isZero x := 
    match x with 
    | O => constr:true 
    | _ => constr:false 
    end. 

Goal Set. 
    let isz := isZero O in pose isz. 
    (* adds true to the context *) 

现在想象一下，我想战术接受多一点;也许任何可以用零换算的术语。如果这是作用于目标的策略，我会做

Ltac isZero x := 
    match x with 
    | ?v => unify v 0; constr:true 
    | _ => constr:false 
    end. 

，但失败的战术生产方面：

Error: Value is a term. Expected a tactic. 

我怎样才能在生产方面的策略检查可兑换？在这个减少x或计算它（let xx := eval compute in x）的特定示例中可能有效，但在更复杂的示例中，计算成本可能会过高，特别是因为我需要减少比较的两个项。

PS：作为参考，繁体字的问题是，我试图查找效率的关键可能是通过匹配调用序列建成add在FMap一个值，战术看起来像

Ltac find_key value := 
    match fmap with 
    | add ?k value _ => constr:(Some k) 
    | add _ _ ?m => find_key value m 
    | _ => constr:None 
    end 

通过这种实现，如果地图中包含的术语不是value，则该术语可转换为value，但在语法上不等于该术语，该策略将错误地返回None。

Answer 1

您可以尝试构建触发转换检查的术语;例如：

Goal 2 + 2 = 4. 

match goal with 
| |- ?a = ?b => 
    let e := constr:(eq_refl a : a = b) in 
    idtac "equal" 
| |- _ => idtac "not equal" 
end. 

通常情况下，打印“相等”。但是，如果在上述目标中将4替换为3，则内部分支失败，打印“不相等”。