How to have a proposition of comparing two 'int' types in Coq?

Question

I have the following Definition in my spec file in Coq. I need to have a proposition comparing two "int" type values. These two are 't' and 'Int.repr (i.(period1))'.(i.period1) and (i.period2) have type 'Z'.

This is my code snippet:

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

This gives me the error below:

The term "t" has type "int" while it is expected to have type "Z".

---

I also tried:

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

but it gives me this error:

The term "Int.cmpu Cgt t (Int.repr (period1 i))" has type "bool" while it is expected to have type "Prop".

Is there any way I can compare these two 'int' types or convert them to something else and return 'prop' type?

Thanks,

Answer 1

Any bool can be converted to a Prop by equating it to true. In your example, this would lead to:

   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.

If you search results on the Int.cmpu operator, you'll probably find many lemmas in the Int module that are stated in terms of Int.cmpu Cgt x y = true. For this, you can use the SearchAbout command:

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

Coercions

Equating booleans to true is so common that people often declare a coercion to use booleans as if they were propositions:

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

Now, you can use any boolean in a context where a proposition is expected:

   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.

Behind the scenes, Coq inserts invisible calls to is_true around those occurrences. You should be aware, though, that the coercions still appear in your terms. You can see this by issuing a special command,

Set Printing Coercions.

which would show you the above snippet as Coq sees it:

   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.

(To undo the previous step, just run Unset Printing Coercions.)

Because coercions are not printed by default, it can take you some time to use them effectively. The Ssreflect and MathComp Coq libraries make heavy use of is_true as a coercion, and have special support for making it simpler to use. If you're interested, I suggest you have a look at them!