# Library VarMap

Require Import Setoid Morphisms.
Require Import Omega.

Module Type Eqv.
Parameter Inline t : Type.
Parameter Inline eq : t -> t -> Prop.
Parameter eq_equiv : Equivalence eq.
End Eqv.

Module Make (X:Eqv).
Import X.

Definition map := nat -> t.
Definition eq_map : relation map := (pointwise_relation nat eq).

Definition nil (x:t) : map := fun _ => x.
Definition cons (x:t) (i:map) : map :=
fun k => match k with
| 0 => x
| S n => i n
end.
Definition shift (n:nat) (i:map) : map := fun k => i (n+k).

Definition lams n (f:map -> map) (i:map) : map :=
fun k => if le_gt_dec n k then f (shift n i) (k-n) else i k.

Instance cons_morph : Proper (eq ==> eq_map ==> eq_map) cons.
Qed.
Instance cons_morph' :
Proper (eq ==> eq_map ==> @Logic.eq _ ==> eq) cons.
Qed.

Instance shift_morph : Proper (@Logic.eq _ ==> eq_map ==> eq_map) shift.
Qed.

Instance lams_morph :
Proper (@Logic.eq _ ==> (eq_map ==> eq_map) ==> eq_map ==> eq_map) lams.
Qed.

Lemma cons_ext : forall (x:t) i i',
eq x (i' 0) ->
eq_map i (shift 1 i') ->
eq_map (cons x i) i'.

Lemma shift0 : forall i, eq_map (shift 0 i) i.

Lemma shift_split : forall n i,
eq_map (shift (S n) i) (shift n (shift 1 i)).

Lemma shift_cons : forall x i,
eq_map (shift 1 (cons x i)) i.

Lemma lams_bv : forall m f i k,
k < m -> eq (lams m f i k) (i k).

Lemma lams_shift : forall m f i,
eq_map (shift m (lams m f i)) (f (shift m i)).

Lemma lams0 : forall f i, eq_map (lams 0 f i) (f (fun k => i k)).

Lemma shift_lams : forall k f i,
eq_map (shift 1 (lams (S k) f i)) (lams k f (shift 1 i)).

Lemma cons_lams :
forall k f i x,
Proper (eq_map ==> eq_map) f ->
eq_map (cons x (lams k f i)) (lams (S k) f (cons x i)).

End Make.