Resolve "Add correct compare definitions"
This MR got longer than I expected. The main changes are:
- having a correct definition of the
compare
primitive for integers: it should only return-1
,0
or+1
and not be the difference inZ
of the two inputs like we did before. This was wrong both because it is not the OCaml behavior and it could exceed the bounds ofint
,int32
orint64
; - removing the
Compare.wrap_compare
usage in many places, as this function to normalize the output of comparison functions to-1
,0
or+1
is not needed anymore in many places; - having more direct definitions for the various comparison operators (
<i
,>=i64
, ...), using the>?
,>=?
, ... Coq primitives instead of going through thecompare
operator; - fixing some conversion functions between the various kinds of integers, to normalize the results.
These changes broke one proof in Saturation_repr.v
about the multiplication. Hopefully with these changes we should be fully correct now for our definitions of integers.
Closes #34 (closed)
Edited by Guillaume Claret