Module ErrorsC
Require
Import
CoqlibC
Errors
Compiler
.
Lemma
mmap_app
A
B
(
f
:
A
->
res
B
)
l0
l1
:
mmap
f
(
l0
++
l1
) =
bind
(
mmap
f
l0
) (
fun
hds
=>
bind
(
mmap
f
l1
) (
fun
tl
=>
OK
(
hds
++
tl
))).
Proof.
induction
l0
;
ss
;
i
;
unfold
bind
at
1;
des_ifs
.
rewrite
IHl0
.
unfold
bind
.
des_ifs
.
Qed.
Lemma
mmap_partial
A
B
C
(
f
:
A
->
res
B
) (
g
:
B
->
res
C
)
la
lc
(
MMAP
:
mmap
(
fun
a
=>
OK
a
@@@
f
@@@
g
)
la
=
OK
lc
):
exists
lb
, (<<
MMAP0
:
mmap
f
la
=
OK
lb
>>) /\ (<<
MMAP1
:
mmap
g
lb
=
OK
lc
>>).
Proof.
ginduction
la
;
ss
;
i
;
clarify
.
-
esplits
;
eauto
.
-
unfold
bind
in
*.
des_ifs_safe
.
exploit
IHla
;
eauto
.
i
.
des
.
rewrite
MMAP0
.
esplits
;
eauto
.
ss
.
unfold
bind
.
rewrite
MMAP1
.
des_ifs
.
Qed.