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.