COQ : 불평등 테스트

Question

조건 분기에 대한 간단한 구조가 w COQ의 평등 테스트 /있다 :

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)을 볼 수 있지만 S x < S (S x)은 볼 수 없습니다.