Library IntMap
Set Implicit Arguments.
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.
Proof.
red; reflexivity.
Qed.
Lemma sym_eq_map : ∀ m1 m2, eq_map m1 m2 -> eq_map m2 m1.
Proof.
unfold eq_map; auto.
Qed.
Lemma trans_eq_map :
∀ m1 m2 m3, eq_map m1 m2 -> eq_map m2 m3 -> eq_map m1 m3.
Proof.
unfold eq_map; intros; transitivity (m2 i); trivial.
Qed.
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).
Proof.
unfold eq_map; destruct i; simpl; intros; auto.
Qed.
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)).
Proof.
red; intros.
unfold del_map, cons_map, ins_map.
destruct i; simpl ; auto; intros.
rewrite <- plus_n_Sm.
case (le_gt_dec k i); simpl; trivial.
Qed.
Lemma del_cons_map2 :
∀ n x m,
eq_map (del_map (S n) 0 (cons_map x m)) (del_map n 0 m).
Proof.
red;intros.
unfold del_map, cons_map, ins_map.
simpl.
trivial.
Qed.
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)).
Proof.
red;intros.
unfold cons_map, ins_map.
destruct i; auto.
simpl; generalize (lt_eq_lt_dec k i); intros [[H|H]|H]; simpl; trivial.
destruct i; trivial.
inversion H.
Qed.
End Map.
Hint Resolve refl_eq_map cons_map_ext.
Hint Immediate sym_eq_map.
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.
Proof.
red; reflexivity.
Qed.
Lemma sym_eq_map : ∀ m1 m2, eq_map m1 m2 -> eq_map m2 m1.
Proof.
unfold eq_map; auto.
Qed.
Lemma trans_eq_map :
∀ m1 m2 m3, eq_map m1 m2 -> eq_map m2 m3 -> eq_map m1 m3.
Proof.
unfold eq_map; intros; transitivity (m2 i); trivial.
Qed.
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).
Proof.
unfold eq_map; destruct i; simpl; intros; auto.
Qed.
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)).
Proof.
red; intros.
unfold del_map, cons_map, ins_map.
destruct i; simpl ; auto; intros.
rewrite <- plus_n_Sm.
case (le_gt_dec k i); simpl; trivial.
Qed.
Lemma del_cons_map2 :
∀ n x m,
eq_map (del_map (S n) 0 (cons_map x m)) (del_map n 0 m).
Proof.
red;intros.
unfold del_map, cons_map, ins_map.
simpl.
trivial.
Qed.
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)).
Proof.
red;intros.
unfold cons_map, ins_map.
destruct i; auto.
simpl; generalize (lt_eq_lt_dec k i); intros [[H|H]|H]; simpl; trivial.
destruct i; trivial.
inversion H.
Qed.
End Map.
Hint Resolve refl_eq_map cons_map_ext.
Hint Immediate sym_eq_map.