# 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.