Library Coq.setoid_ring.BinList
Require
Import
BinPos
.
Require
Export
List
.
Set Implicit Arguments
.
Local Open
Scope
positive_scope
.
Section
MakeBinList
.
Variable
A
:
Type
.
Variable
default
:
A
.
Fixpoint
jump
(
p
:
positive
) (
l
:
list
A
) {
struct
p
} :
list
A
:=
match
p
with
|
xH
=>
tl
l
|
xO
p
=>
jump
p
(
jump
p
l
)
|
xI
p
=>
jump
p
(
jump
p
(
tl
l
))
end
.
Fixpoint
nth
(
p
:
positive
) (
l
:
list
A
) {
struct
p
} :
A
:=
match
p
with
|
xH
=>
hd
default
l
|
xO
p
=>
nth
p
(
jump
p
l
)
|
xI
p
=>
nth
p
(
jump
p
(
tl
l
))
end
.
Lemma
jump_tl
:
forall
j
l
,
tl
(
jump
j
l
)
=
jump
j
(
tl
l
).
Lemma
jump_succ
:
forall
j
l
,
jump
(
Pos.succ
j
)
l
=
jump
1 (
jump
j
l
).
Lemma
jump_add
:
forall
i
j
l
,
jump
(
i
+
j
)
l
=
jump
i
(
jump
j
l
).
Lemma
jump_pred_double
:
forall
i
l
,
jump
(
Pos.pred_double
i
) (
tl
l
)
=
jump
i
(
jump
i
l
).
Lemma
nth_jump
:
forall
p
l
,
nth
p
(
tl
l
)
=
hd
default
(
jump
p
l
).
Lemma
nth_pred_double
:
forall
p
l
,
nth
(
Pos.pred_double
p
) (
tl
l
)
=
nth
p
(
jump
p
l
).
End
MakeBinList
.