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

Question

У меня есть следующее определение в моем spec-файле в 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" имеет тип "int", в то время как ожидается, что он будет иметь тип "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 Cgt t (Int.repr (period1 i))" имеет тип "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.)

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