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

  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

  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

  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.