Module MutrecHeader
Require
Import
IntegersC
.
Require
Import
CoqlibC
.
Require
Import
Zwf
.
Require
Coq.Program.Wf
.
Require
Import
Recdef
.
Require
Import
Intv
.
Require
Import
AxiomsC
.
Definition
main_id
:= (77%
positive
).
Definition
f_id
:= (154%
positive
).
Definition
g_id
:= (176%
positive
).
Definition
MAX
:
Z
:= 1000%
Z
.
Definition
sum
(
i
:
int
):
int
:=
let
sumz
:
Z
:=
fold_rec
Z
Z.add
0%
Z
0%
Z
(
i
.(
Int.intval
) + 1)%
Z
in
Int.repr
sumz
.
Lemma
eta
i
iproof
j
jproof
(
EQ
:
i
=
j
)
:
Int.mkint
i
iproof
=
Int.mkint
j
jproof
.
Proof.
clarify
.
assert
(
iproof
=
jproof
).
{
eapply
proof_irr
. }
clarify
.
Qed.
Lemma
sum_recurse
i
:
(
sum
i
) =
if
Z.eqb
i
.(
Int.intval
) 0%
Z
then
Int.zero
else
Int.add
(
sum
(
Int.sub
i
Int.one
))
i
.
Proof.
des_ifs
.
-
apply
Z.eqb_eq
in
Heq
.
destruct
i
;
ss
.
clarify
.
unfold
sum
.
ss
.
rewrite
fold_rec_equation
.
des_ifs
.
zsimpl
.
rewrite
fold_rec_equation
.
des_ifs
.
-
destruct
i
;
ss
.
apply
Z.eqb_neq
in
Heq
.
assert
(
intval
>= 1)
by
xomega
.
unfold
Int.sub
.
ss
.
unfold
sum
at
1.
rewrite
fold_rec_equation
.
ss
.
des_ifs
;
try
xomega
.
assert
(
exists
j
,
j
.(
Int.intval
) =
intval
- 1).
{
unshelve
eexists
(
Int.mkint
_
_
);
simpl
;
try
reflexivity
.
xomega
.
}
des
.
rewrite
Int.unsigned_one
.
unfold
sum
.
assert
(
MOD0
:
Int.Z_mod_modulus
intval
=
intval
).
{
rewrite
Int.Z_mod_modulus_eq
.
symmetry
.
eapply
Z.mod_unique_pos
with
(
q
:= 0%
Z
);
try
xomega
.
}
assert
(
MOD1
:
Int.Z_mod_modulus
(
intval
- 1) =
intval
- 1).
{
rewrite
Int.Z_mod_modulus_eq
.
symmetry
.
eapply
Z.mod_unique_pos
with
(
q
:= 0%
Z
);
try
xomega
.
}
replace
{|
Int.intval
:=
intval
;
Int.intrange
:=
conj
intrange
intrange0
|}
with
(
Int.repr
intval
);
cycle
1.
{
Local
Transparent
Int.repr
.
eapply
eta
.
Local
Opaque
Int.repr
.
ss
.
}
rewrite
Int.Ptrofs_add_repr
.
f_equal
.
zsimpl
.
rewrite
Z.add_comm
.
f_equal
.
f_equal
.
Local
Transparent
Int.repr
.
ss
.
Local
Opaque
Int.repr
.
rewrite
MOD1
.
lia
.
Qed.
Require
AST
.
Definition
fg_sig
:
AST.signature
:= (
AST.mksignature
[
AST.Tint
] (
Some
AST.Tint
)
AST.cc_default
true
).