Library Coq.micromega.Env
Require Import ZArith.
Require Import Coq.Arith.Max.
Require Import List.
Section S.
Variable D :
Type.
Definition Env :=
positive ->
D.
Definition jump (
j:
positive) (
e:
Env) :=
fun x =>
e (
Pplus x j).
Definition nth (
n:
positive) (
e :
Env ) :=
e n.
Definition hd (
x:
D) (
e:
Env) :=
nth xH e.
Definition tail (
e:
Env) :=
jump xH e.
Lemma psucc :
forall p,
(match p with
|
xI y' =>
xO (
Psucc y')
|
xO y' =>
xI y'
| 1%
positive => 2%
positive
end) = (
p+1)%
positive.
Lemma jump_Pplus :
forall i j l,
forall x,
jump (
i + j)
l x = jump i (
jump j l)
x.
Lemma jump_simpl :
forall p l,
forall 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.
Ltac jump_s :=
repeat
match goal with
| |-
context [
jump xH ?
e] =>
rewrite (
jump_simpl xH)
| |-
context [
jump (
xO ?
p) ?
e] =>
rewrite (
jump_simpl (
xO p))
| |-
context [
jump (
xI ?
p) ?
e] =>
rewrite (
jump_simpl (
xI p))
end.
Lemma jump_tl :
forall j l,
forall x,
tail (
jump j l)
x = jump j (
tail l)
x.
Lemma jump_Psucc :
forall j l,
forall x,
(jump (
Psucc j)
l x) = (jump 1 (
jump j l)
x).
Lemma jump_Pdouble_minus_one :
forall i l,
forall x, (
jump (
Pdouble_minus_one i) (
tail l))
x = (
jump i (
jump i l))
x.
Lemma jump_x0_tail :
forall p l,
forall x,
jump (
xO p) (
tail l)
x = jump (
xI p)
l x.
Lemma nth_spec :
forall p l x,
nth p l =
match p with
|
xH =>
hd x l
|
xO p =>
nth p (
jump p l)
|
xI p =>
nth p (
jump p (
tail l))
end.
Lemma nth_jump :
forall p l x,
nth p (
tail l)
= hd x (
jump p l).
Lemma nth_Pdouble_minus_one :
forall p l,
nth (
Pdouble_minus_one p) (
tail l)
= nth p (
jump p l).
End S.