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

この実装ではvalue、マップの代わりに、変換可能で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 に答える