Library Coq.setoid_ring.BinList
Require
Import
BinPos
.
Require
Export
List
.
Require
Export
ListTactics
.
Open
Local
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
=>
tail
l
|
xO
p
=>
jump
p
(
jump
p
l
)
|
xI
p
=>
jump
p
(
jump
p
(
tail
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
(
tail
l
))
end
.
Lemma
jump_tl
:
forall
j
l
,
tail
(
jump
j
l
)
=
jump
j
(
tail
l
).
Lemma
jump_Psucc
:
forall
j
l
,
(
jump
(
Psucc
j
)
l
)
=
(
jump
1 (
jump
j
l
)
)
.
Lemma
jump_Pplus
:
forall
i
j
l
,
(
jump
(
i
+
j
)
l
)
=
(
jump
i
(
jump
j
l
)
)
.
Lemma
jump_Pdouble_minus_one
:
forall
i
l
,
(
jump
(
Pdouble_minus_one
i
) (
tail
l
)
)
=
(
jump
i
(
jump
i
l
)
)
.
Lemma
nth_jump
:
forall
p
l
,
nth
p
(
tail
l
)
=
hd
default
(
jump
p
l
).
Lemma
nth_Pdouble_minus_one
:
forall
p
l
,
nth
(
Pdouble_minus_one
p
) (
tail
l
)
=
nth
p
(
jump
p
l
).
End
MakeBinList
.