1

假设我有以下策略来检查一个术语是否是文字零：

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：作为参考，未简化的问题是我正在尝试有效地查找一个键，该键可能与FMap由调用序列构建的值匹配add，并且该策略看起来像

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

在这个实现中，如果不是valuemap 包含一个可转换为value但在语法上不等于它的术语，则该策略将错误地返回None.

4

1 回答 1

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在上面的目标中，内部分支会失败，打印“不等于”。

于 2015-10-10T00:54:55.923 回答