Module IntegersC
Require
Import
Eqdep_dec
Zquot
Zwf
.
Require
Import
CoqlibC
.
Require
Archi
.
newly added *
Require
Export
Integers
.
Lemma
Ptrofs_add_repr
:
forall
x
y
,
<<
EQ
: (
Ptrofs.add
(
Ptrofs.repr
x
) (
Ptrofs.repr
y
)) =
Ptrofs.repr
(
x
+
y
)>>.
Proof.
i
.
apply
Ptrofs.eqm_repr_eq
.
eapply
Ptrofs.eqm_sym
.
eapply
Ptrofs.eqm_trans
.
-
apply
Ptrofs.eqm_sym
.
apply
Ptrofs.eqm_unsigned_repr
.
-
apply
Ptrofs.eqm_add
;
apply
Ptrofs.eqm_unsigned_repr
.
Qed.
Lemma
max_unsigned_zero
: 0 <=
Ptrofs.max_unsigned
.
Proof.
etransitivity
;
try
unshelve
apply
Ptrofs.unsigned_range_2
.
apply
Ptrofs.zero
.
Qed.
Lemma
mul_le_div
a
b
(
LE
: 4 *
a
<=
b
):
<<
LE
:
a
<=
b
/ 4>>.
Proof.
red
.
assert
(4 *
a
/ 4 =
a
).
{
rewrite
Z.mul_comm
.
rewrite
Z.div_mul
;
ss
. }
rewrite
<-
H
.
eapply
Z_div_le
;
eauto
.
xomega
.
Qed.
Lemma
Z2Nat_range
n
:
Z.of_nat
(
Z.to_nat
n
) =
if
(
zle
0
n
)
then
n
else
0.
Proof.
destruct
n
;
ss
;
try
nia
. Qed.
Hint
Rewrite
Ptrofs.unsigned_zero
Ptrofs.add_zero
Ptrofs.add_zero_l
Ptrofs.repr_unsigned
Ptrofs_add_repr
:
psimpl
.
Ltac
psimpl
:=
repeat
(
autorewrite
with
psimpl
in
*;
try
(
rewrite
Ptrofs.unsigned_repr
in
*;
ss
;
try
xomega
; [])).