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.