Library Coq.micromega.Env
Require
Import
BinInt
List
.
Set Implicit Arguments
.
Local Open
Scope
positive_scope
.
Section
S
.
Variable
D
:
Type
.
Definition
Env
:=
positive
->
D
.
Definition
jump
(
j
:
positive
) (
e
:
Env
) :=
fun
x
=>
e
(
x
+
j
).
Definition
nth
(
n
:
positive
) (
e
:
Env
) :=
e
n
.
Definition
hd
(
e
:
Env
) :=
nth
1
e
.
Definition
tail
(
e
:
Env
) :=
jump
1
e
.
Lemma
jump_add
i
j
l
x
:
jump
(
i
+
j
)
l
x
=
jump
i
(
jump
j
l
)
x
.
Lemma
jump_simpl
p
l
x
:
jump
p
l
x
=
match
p
with
|
xH
=>
tail
l
x
|
xO
p
=>
jump
p
(
jump
p
l
)
x
|
xI
p
=>
jump
p
(
jump
p
(
tail
l
))
x
end
.
Lemma
jump_tl
j
l
x
:
tail
(
jump
j
l
)
x
=
jump
j
(
tail
l
)
x
.
Lemma
jump_succ
j
l
x
:
jump
(
Pos.succ
j
)
l
x
=
jump
1 (
jump
j
l
)
x
.
Lemma
jump_pred_double
i
l
x
:
jump
(
Pos.pred_double
i
) (
tail
l
)
x
=
jump
i
(
jump
i
l
)
x
.
Lemma
nth_spec
p
l
:
nth
p
l
=
match
p
with
|
xH
=>
hd
l
|
xO
p
=>
nth
p
(
jump
p
l
)
|
xI
p
=>
nth
p
(
jump
p
(
tail
l
))
end
.
Lemma
nth_jump
p
l
:
nth
p
(
tail
l
)
=
hd
(
jump
p
l
).
Lemma
nth_pred_double
p
l
:
nth
(
Pos.pred_double
p
) (
tail
l
)
=
nth
p
(
jump
p
l
).
End
S
.
Ltac
jump_simpl
:=
repeat
match
goal
with
| |-
context
[
jump
xH
] =>
rewrite
(
jump_simpl
xH
)
| |-
context
[
jump
(
xO
?
p
)] =>
rewrite
(
jump_simpl
(
xO
p
))
| |-
context
[
jump
(
xI
?
p
)] =>
rewrite
(
jump_simpl
(
xI
p
))
end
.