Как получить предложение сравнить два типа «int» в Coq?

Question

У меня есть следующее определение в моем файле spec в Coq. Мне нужно иметь предложение, сравнивающее два значения типа «int». Эти два являются «t» и «Int.pr (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). 

Это дает мне ошибку ниже:

Термин «т» имеет тип «ИНТ» в то время, как ожидается, имеют тип «Z».

---

Я также попытался:

(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 ВКТ т (Int.repr (period1 я))" имеет тип «bool», в то время как ожидается, что он будет иметь тип «Prop».

Есть ли способ сравнить эти два типа «int» или преобразовать их в нечто другое и вернуть тип «prop»?

Спасибо,

Answer 1

Любой bool может быть преобразован в Prop путем приравнивания его к true. В вашем примере, это приведет к:

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, вы, вероятно, найдете много лемм в Int модуле, которые определены в терминах Int.cmpu Cgt x y = true. Для этого вы можете использовать SearchAbout команду:

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

Приведение

Приравнивая булевы к true настолько часто, что люди часто объявить принуждение использовать булевы, как если бы они были положения:

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

Теперь вы можете использовать любое булево значение в контексте, где ожидается предложение:

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 вокруг этих вхождений. Однако вы должны знать, что принуждения все еще появляются в ваших условиях. Вы можете увидеть это, выпустив специальную команду,

Set Printing Coercions. 

, который покажет вам выше фрагмент кода, как Coq видит:

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.)

Поскольку принуждения не печатаются по умолчанию, может потребоваться некоторое время для их эффективного использования. Библиотеки Coq Ssreflect and MathComp в значительной степени используют is_true в качестве принуждения и имеют специальную поддержку, упрощающую ее использование. Если вам интересно, я предлагаю вам взглянуть на них!