Library IntMap
Set
Implicit
Arguments
.
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
.
Proof
.
red
; reflexivity
.
Qed
.
Lemma
sym_eq_map
: forall
m1
m2
, eq_map
m1
m2
-> eq_map
m2
m1
.
Proof
.
unfold
eq_map
; auto
.
Qed
.
Lemma
trans_eq_map
:
forall
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
: forall
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
:
forall
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
:
forall
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
:
forall
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
.