Coq에서 두 개의 'int'유형을 비교하는 방법은 무엇입니까?

Question

필자는 Coq의 사양 파일에 다음과 같은 정의를 가지고 있습니다. 두 개의 "int"유형 값을 비교하는 제안이 필요합니다. 이 두 가지는 't'와 'Int.repr (i. (period1))'입니다. (i.period1) 및 (i.period2)의 유형은 'Z'입니다.

이 내 코드입니다 : 이것은 나에게 아래의 오류를 제공

Definition trans_uni_r_reject (i: invariant) (om os: block) (rid roff rval t: int) (m: mem) := 
    (t > (Int.repr (i.(period1)))   
/\ t < (Int.repr (i.(period2))) 
/\ master_eval_reject i om os rid roff rval m). 

:

용어 "t"는이 유형의 "Z"를 것으로 예상되는 동안 "INT"를 입력있다.

(Int.cmpu Cgt t (Int.repr (i.(period1)))) 
/\ (Int.cmpu Clt t (Int.repr (i.(period2)))) 
/\ (master_eval_reject i om os rid roff rval m). 

를하지만 나에게이 오류 제공 :

---

나는 또한 시도

용어를 "Int.cmpu CGT의 t (Int.repr (기간 1의 I))" 유형이 "Prop"인 것으로 예상되는 동안 유형은 "bool"입니다.

이 두 'int'형식을 비교하거나 다른 형식으로 변환하고 '소품'유형을 반환 할 수있는 방법이 있습니까?

감사합니다,

Answer 1

모든 bool는 true에 동일시하여 Prop로 변환 할 수 있습니다. 당신이 Int.cmpu 연산자에 대한 결과를 검색하는 경우

Int.cmpu Cgt t (Int.repr (i.(period1))) = true 
/\ Int.cmpu Clt t (Int.repr (i.(period2))) = true 
/\ master_eval_reject i om os rid roff rval m. 

, 당신은 아마 Int.cmpu Cgt x y = true 약관에 명시되어있는 Int 모듈의 많은 보조 정리를 찾을 수 있습니다 : 당신의 예에서,이 이어질 것입니다.

Definition is_true (b : bool) : Prop := b = true. 
Coercion is_true : bool >-> Sortclass. 

: true에

SearchAbout Int.cmpu. (* Looks for all results on Int.cmpu *) 
SearchAbout Int.cmpu Cgt (* Looks for all results that mention 
          Int.cmpu and Cgt *) 

강제 변환

동일시 부울 사람들이 종종 제안을 것처럼 논리 값을 사용하기 강제를 선언 너무 일반적입니다 :이 경우, 당신은 SearchAbout 명령을 사용할 수 있습니다

이제 제안이 예상되는 컨텍스트에서 부울을 사용할 수 있습니다.

Int.cmpu Cgt t (Int.repr (i.(period1))) 
/\ Int.cmpu Clt t (Int.repr (i.(period2))) 
/\ master_eval_reject i om os rid roff rval m. 

Coq는 장면 뒤에서 is_true에 보이지 않는 호출을 삽입합니다. 하지만 강압은 여전히 ​​귀하의 관점에서 나타납니다. 당신은 COQ이 그것을보고로

Set Printing Coercions. 

는 당신에게 위의 코드를 보여줄 것이다, 특별한 명령을 실행하여이 문제를 볼 수 있습니다

is_true (Int.cmpu Cgt t (Int.repr (i.(period1)))) 
/\ is_true (Int.cmpu Clt t (Int.repr (i.(period2)))) 
/\ master_eval_reject i om os rid roff rval m. 

가 (이전 단계를 실행 취소하려면, 단지 Unset Printing Coercions를 실행합니다.)

강제 변환은 기본적으로 인쇄되지 않으므로 효과적으로 사용하기 위해 시간이 필요합니다. Ssreflect and MathComp Coq 라이브러리는 강제로 is_true을 많이 사용하며 사용하기 쉽도록 특별한 지원을합니다. 관심이 있다면, 당신이 그들을 살펴볼 것을 제안합니다!