Library Coq.micromega.Env

Require Import BinInt List.
Set Implicit Arguments.
Local Open Scope positive_scope.

Section S.

  Variable D :Type.

  Definition Env := positive -> D.

  Definition jump (j:positive) (e:Env) := fun x => e (x+j).

  Definition nth (n:positive) (e:Env) := e n.

  Definition hd (e:Env) := nth 1 e.

  Definition tail (e:Env) := jump 1 e.

  Lemma jump_add i j l x : jump (i + j) l x = jump i (jump j l) x.

  Lemma jump_simpl p l 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.

  Lemma jump_tl j l x : tail (jump j l) x = jump j (tail l) x.

  Lemma jump_succ j l x : jump (Pos.succ j) l x = jump 1 (jump j l) x.

  Lemma jump_pred_double i l x :
    jump (Pos.pred_double i) (tail l) x = jump i (jump i l) x.

  Lemma nth_spec p l :
    nth p l =
    match p with
      | xH => hd l
      | xO p => nth p (jump p l)
      | xI p => nth p (jump p (tail l))
    end.

  Lemma nth_jump p l : nth p (tail l) = hd (jump p l).

  Lemma nth_pred_double p l :
    nth (Pos.pred_double p) (tail l) = nth p (jump p l).

End S.

Ltac jump_simpl :=
  repeat
    match goal with
      | |- context [jump xH] => rewrite (jump_simpl xH)
      | |- context [jump (xO ?p)] => rewrite (jump_simpl (xO p))
      | |- context [jump (xI ?p)] => rewrite (jump_simpl (xI p))
    end.