Library IntMap
Require Export Compare_dec.
Section Map.
Variable A : Type.
Definition eq_map (m1 m2:nat->A) : Prop := ∀ i, m1 i = m2 i.
Lemma refl_eq_map : ∀ m, eq_map m m.
Lemma sym_eq_map : ∀ m1 m2, eq_map m1 m2 -> eq_map m2 m1.
Lemma trans_eq_map :
∀ 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 : ∀ 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 :
∀ 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 :
∀ n x m,
eq_map (del_map (S n) 0 (cons_map x m)) (del_map n 0 m).
Lemma ins_cons_map :
∀ 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.