Library IntMap

Require Export Compare_dec.

Section Map.

Variable A : Type.

Definition eq_map (m1 m2:nat->A) : Prop := forall i, m1 i = m2 i.

Lemma refl_eq_map : forall m, eq_map m m.

Lemma sym_eq_map : forall m1 m2, eq_map m1 m2 -> eq_map m2 m1.

Lemma trans_eq_map :
forall m1 m2 m3, eq_map m1 m2 -> eq_map m2 m3 -> eq_map m1 m3.

Definition cons_map (x:A) (m:nat->A) (n:nat) : A :=
match n with
| O => x
| (S k) => m k
end.

Lemma cons_map_ext : forall x y m1 m2,
x = y ->
eq_map m1 m2 ->
eq_map (cons_map x m1) (cons_map y m2).

Definition ins_map (n:nat) (x:A) (m:nat->A) (i:nat) : A :=
match lt_eq_lt_dec n i with
| inleft (left _) => m (pred i)
| inleft (right _) => x
| inright _ => m i
end.

Definition del_map (n k:nat) (m:nat->A) (i:nat) : A :=
match le_gt_dec k i with
| left _ => m (plus n i)
| right_ => m i
end.

Lemma del_cons_map :
forall x n k m,
eq_map (del_map n (S k) (cons_map x m)) (cons_map x (del_map n k m)).

Lemma del_cons_map2 :
forall n x m,
eq_map (del_map (S n) 0 (cons_map x m)) (del_map n 0 m).

Lemma ins_cons_map :
forall x y k m,
eq_map (ins_map (S k) y (cons_map x m)) (cons_map x (ins_map k y m)).

End Map.

Hint Resolve refl_eq_map cons_map_ext.
Hint Immediate sym_eq_map.