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.