コック：不等式テスト

Question

条件分岐のための簡単な構築物は、Coqの中平等テスト/ wがあります：

Check ltac:(tryif unify 1 (S 0) then idtac "success" else idtac "fail"). (*success...*) 

は<および/または<=をテストするための同様の方法はありますか？

Answer 1

標準ライブラリ（<=?と<?という表記があります）のとltb関数を使用できますか？

Require Import Arith. 

Check ltac:(match (eval cbv in (2 <? 5)) with 
      | true => idtac "success" 
      | false => idtac "fail" end). 

もちろん、関数の評価が変数に固定されていない場合、これは失敗します。文脈にxがある場合、それは3 < 5および1 < S (S x)であることを確認することができますが、​​ではそうではありません。