A persistent union-find data structure.
Require Coq.Program.Wf.
Require Import Coqlib.
Open Scope nat_scope.
Set Implicit Arguments.
Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.
Module Type MAP.
Variable elt:
Type.
Variable elt_eq:
forall (
x y:
elt), {
x=
y} + {
x<>
y}.
Variable t:
Type ->
Type.
Variable empty:
forall (
A:
Type),
t A.
Variable get:
forall (
A:
Type),
elt ->
t A ->
option A.
Variable set:
forall (
A:
Type),
elt ->
A ->
t A ->
t A.
Hypothesis gempty:
forall (
A:
Type) (
x:
elt),
get x (
empty A) =
None.
Hypothesis gsspec:
forall (
A:
Type) (
x y:
elt) (
v:
A) (
m:
t A),
get x (
set y v m) =
if elt_eq x y then Some v else get x m.
End MAP.
Unset Implicit Arguments.
Module Type UNIONFIND.
Variable elt:
Type.
Variable elt_eq:
forall (
x y:
elt), {
x=
y} + {
x<>
y}.
Variable t:
Type.
Variable repr:
t ->
elt ->
elt.
Hypothesis repr_canonical:
forall uf a,
repr uf (
repr uf a) =
repr uf a.
Definition sameclass (
uf:
t) (
a b:
elt) :
Prop :=
repr uf a =
repr uf b.
Hypothesis sameclass_refl:
forall uf a,
sameclass uf a a.
Hypothesis sameclass_sym:
forall uf a b,
sameclass uf a b ->
sameclass uf b a.
Hypothesis sameclass_trans:
forall uf a b c,
sameclass uf a b ->
sameclass uf b c ->
sameclass uf a c.
Hypothesis sameclass_repr:
forall uf a,
sameclass uf a (
repr uf a).
Variable empty:
t.
Hypothesis repr_empty:
forall a,
repr empty a =
a.
Hypothesis sameclass_empty:
forall a b,
sameclass empty a b ->
a =
b.
Variable find:
t ->
elt ->
elt *
t.
Hypothesis find_repr:
forall uf a,
fst (
find uf a) =
repr uf a.
Hypothesis find_unchanged:
forall uf a x,
repr (
snd (
find uf a))
x =
repr uf x.
Hypothesis sameclass_find_1:
forall uf a x y,
sameclass (
snd (
find uf a))
x y <->
sameclass uf x y.
Hypothesis sameclass_find_2:
forall uf a,
sameclass uf a (
fst (
find uf a)).
Hypothesis sameclass_find_3:
forall uf a,
sameclass (
snd (
find uf a))
a (
fst (
find uf a)).
Variable union:
t ->
elt ->
elt ->
t.
Hypothesis repr_union_1:
forall uf a b x,
repr uf x <>
repr uf a ->
repr (
union uf a b)
x =
repr uf x.
Hypothesis repr_union_2:
forall uf a b x,
repr uf x =
repr uf a ->
repr (
union uf a b)
x =
repr uf b.
Hypothesis repr_union_3:
forall uf a b,
repr (
union uf a b)
b =
repr uf b.
Hypothesis sameclass_union_1:
forall uf a b,
sameclass (
union uf a b)
a b.
Hypothesis sameclass_union_2:
forall uf a b x y,
sameclass uf x y ->
sameclass (
union uf a b)
x y.
Hypothesis sameclass_union_3:
forall uf a b x y,
sameclass (
union uf a b)
x y ->
sameclass uf x y
\/
sameclass uf x a /\
sameclass uf y b
\/
sameclass uf x b /\
sameclass uf y a.
Variable merge:
t ->
elt ->
elt ->
t.
Hypothesis repr_merge:
forall uf a b x,
repr (
merge uf a b)
x =
repr (
union uf a b)
x.
Hypothesis sameclass_merge:
forall uf a b x y,
sameclass (
merge uf a b)
x y <->
sameclass (
union uf a b)
x y.
Variable path_ord:
t ->
elt ->
elt ->
Prop.
Hypothesis path_ord_wellfounded:
forall uf,
well_founded (
path_ord uf).
Hypothesis path_ord_canonical:
forall uf x y,
repr uf x =
x -> ~
path_ord uf y x.
Hypothesis path_ord_merge_1:
forall uf a b x y,
path_ord uf x y ->
path_ord (
merge uf a b)
x y.
Hypothesis path_ord_merge_2:
forall uf a b,
repr uf a <>
repr uf b ->
path_ord (
merge uf a b)
b (
repr uf a).
Variable pathlen:
t ->
elt ->
nat.
Hypothesis pathlen_zero:
forall uf a,
repr uf a =
a <->
pathlen uf a =
O.
Hypothesis pathlen_merge:
forall uf a b x,
pathlen (
merge uf a b)
x =
if elt_eq (
repr uf a) (
repr uf b)
then
pathlen uf x
else if elt_eq (
repr uf x) (
repr uf a)
then
pathlen uf x +
pathlen uf b + 1
else
pathlen uf x.
Hypothesis pathlen_gt_merge:
forall uf a b x y,
repr uf x =
repr uf y ->
pathlen uf x >
pathlen uf y ->
pathlen (
merge uf a b)
x >
pathlen (
merge uf a b)
y.
End UNIONFIND.
Module UF (
M:
MAP) :
UNIONFIND with Definition elt :=
M.elt.
Definition elt :=
M.elt.
Definition elt_eq :=
M.elt_eq.
Definition order (
m:
M.t elt) (
a a':
elt) :
Prop :=
M.get a'
m =
Some a.
Record unionfind :
Type :=
mk {
m:
M.t elt;
mwf:
well_founded (
order m) }.
Definition t :=
unionfind.
Definition getlink (
m:
M.t elt) (
a:
elt) : {
a' |
M.get a m =
Some a'} + {
M.get a m =
None}.
Proof.
destruct (
M.get a m).
left.
exists e;
auto.
right;
auto.
Defined.
Section REPR.
Variable uf:
t.
Definition F_repr (
a:
elt) (
rec:
forall b,
order uf.(
m)
b a ->
elt) :
elt :=
match getlink uf.(
m)
a with
|
inleft (
exist a'
P) =>
rec a'
P
|
inright _ =>
a
end.
Definition repr (
a:
elt) :
elt :=
Fix uf.(
mwf) (
fun _ =>
elt)
F_repr a.
Lemma repr_unroll:
forall a,
repr a =
match M.get a uf.(
m)
with Some a' =>
repr a' |
None =>
a end.
Proof.
intros.
unfold repr at 1.
rewrite Fix_eq.
unfold F_repr.
destruct (
getlink uf.(
m)
a)
as [[
a'
P] |
Q].
rewrite P;
auto.
rewrite Q;
auto.
intros.
unfold F_repr.
destruct (
getlink (
m uf)
x)
as [[
a'
P] |
Q];
auto.
Qed.
Lemma repr_none:
forall a,
M.get a uf.(
m) =
None ->
repr a =
a.
Proof.
Lemma repr_some:
forall a a',
M.get a uf.(
m) =
Some a' ->
repr a =
repr a'.
Proof.
Lemma repr_res_none:
forall (
a:
elt),
M.get (
repr a)
uf.(
m) =
None.
Proof.
Lemma repr_canonical:
forall (
a:
elt),
repr (
repr a) =
repr a.
Proof.
Lemma repr_some_diff:
forall a a',
M.get a uf.(
m) =
Some a' ->
a <>
repr a'.
Proof.
End REPR.
Definition sameclass (
uf:
t) (
a b:
elt) :
Prop :=
repr uf a =
repr uf b.
Lemma sameclass_refl:
forall uf a,
sameclass uf a a.
Proof.
intros. red. auto.
Qed.
Lemma sameclass_sym:
forall uf a b,
sameclass uf a b ->
sameclass uf b a.
Proof.
intros. red. symmetry. exact H.
Qed.
Lemma sameclass_trans:
forall uf a b c,
sameclass uf a b ->
sameclass uf b c ->
sameclass uf a c.
Proof.
intros.
red.
transitivity (
repr uf b).
exact H.
exact H0.
Qed.
Lemma sameclass_repr:
forall uf a,
sameclass uf a (
repr uf a).
Proof.
Lemma wf_empty:
well_founded (
order (
M.empty elt)).
Proof.
red.
intros.
apply Acc_intro.
intros b RO.
red in RO.
rewrite M.gempty in RO.
discriminate.
Qed.
Definition empty :
t :=
mk (
M.empty elt)
wf_empty.
Lemma repr_empty:
forall a,
repr empty a =
a.
Proof.
Lemma sameclass_empty:
forall a b,
sameclass empty a b ->
a =
b.
Proof.
intros.
red in H.
repeat rewrite repr_empty in H.
auto.
Qed.
Section IDENTIFY.
Variable uf:
t.
Variables a b:
elt.
Hypothesis a_canon:
M.get a uf.(
m) =
None.
Hypothesis not_same_class:
repr uf b <>
a.
Lemma identify_order:
forall x y,
order (
M.set a b uf.(
m))
y x <->
order uf.(
m)
y x \/ (
x =
a /\
y =
b).
Proof.
intros until y.
unfold order.
rewrite M.gsspec.
destruct (
M.elt_eq x a).
intuition congruence.
intuition congruence.
Qed.
Remark identify_Acc_b:
forall x,
Acc (
order uf.(
m))
x ->
repr uf x <>
a ->
Acc (
order (
M.set a b uf.(
m)))
x.
Proof.
induction 1;
intros.
constructor;
intros.
rewrite identify_order in H2.
destruct H2 as [
A | [
A B]].
apply H0;
auto.
rewrite <- (
repr_some uf _ _ A).
auto.
subst.
elim H1.
apply repr_none.
auto.
Qed.
Remark identify_Acc:
forall x,
Acc (
order uf.(
m))
x ->
Acc (
order (
M.set a b uf.(
m)))
x.
Proof.
Lemma identify_wf:
well_founded (
order (
M.set a b uf.(
m))).
Proof.
Definition identify :=
mk (
M.set a b uf.(
m))
identify_wf.
Lemma repr_identify_1:
forall x,
repr uf x <>
a ->
repr identify x =
repr uf x.
Proof.
Lemma repr_identify_2:
forall x,
repr uf x =
a ->
repr identify x =
repr uf b.
Proof.
End IDENTIFY.
Remark union_not_same_class:
forall uf a b,
repr uf a <>
repr uf b ->
repr uf (
repr uf b) <>
repr uf a.
Proof.
Definition union (
uf:
t) (
a b:
elt) :
t :=
let a' :=
repr uf a in
let b' :=
repr uf b in
match M.elt_eq a'
b'
with
|
left EQ =>
uf
|
right NEQ =>
identify uf a'
b' (
repr_res_none uf a) (
union_not_same_class uf a b NEQ)
end.
Lemma repr_union_1:
forall uf a b x,
repr uf x <>
repr uf a ->
repr (
union uf a b)
x =
repr uf x.
Proof.
Lemma repr_union_2:
forall uf a b x,
repr uf x =
repr uf a ->
repr (
union uf a b)
x =
repr uf b.
Proof.
Lemma repr_union_3:
forall uf a b,
repr (
union uf a b)
b =
repr uf b.
Proof.
Lemma sameclass_union_1:
forall uf a b,
sameclass (
union uf a b)
a b.
Proof.
Lemma sameclass_union_2:
forall uf a b x y,
sameclass uf x y ->
sameclass (
union uf a b)
x y.
Proof.
Lemma sameclass_union_3:
forall uf a b x y,
sameclass (
union uf a b)
x y ->
sameclass uf x y
\/
sameclass uf x a /\
sameclass uf y b
\/
sameclass uf x b /\
sameclass uf y a.
Proof.
Definition merge (
uf:
t) (
a b:
elt) :
t :=
let a' :=
repr uf a in
let b' :=
repr uf b in
match M.elt_eq a'
b'
with
|
left EQ =>
uf
|
right NEQ =>
identify uf a'
b (
repr_res_none uf a) (
sym_not_equal NEQ)
end.
Lemma repr_merge:
forall uf a b x,
repr (
merge uf a b)
x =
repr (
union uf a b)
x.
Proof.
Lemma sameclass_merge:
forall uf a b x y,
sameclass (
merge uf a b)
x y <->
sameclass (
union uf a b)
x y.
Proof.
Definition path_ord (
uf:
t) :
elt ->
elt ->
Prop :=
order uf.(
m).
Lemma path_ord_wellfounded:
forall uf,
well_founded (
path_ord uf).
Proof.
Lemma path_ord_canonical:
forall uf x y,
repr uf x =
x -> ~
path_ord uf y x.
Proof.
intros;
red;
intros.
hnf in H0.
assert (
M.get x (
m uf) =
None).
rewrite <-
H.
apply repr_res_none.
congruence.
Qed.
Lemma path_ord_merge_1:
forall uf a b x y,
path_ord uf x y ->
path_ord (
merge uf a b)
x y.
Proof.
Lemma path_ord_merge_2:
forall uf a b,
repr uf a <>
repr uf b ->
path_ord (
merge uf a b)
b (
repr uf a).
Proof.
Section PATHLEN.
Variable uf:
t.
Definition F_pathlen (
a:
elt) (
rec:
forall b,
order uf.(
m)
b a ->
nat) :
nat :=
match getlink uf.(
m)
a with
|
inleft (
exist a'
P) =>
S (
rec a'
P)
|
inright _ =>
O
end.
Definition pathlen (
a:
elt) :
nat :=
Fix uf.(
mwf) (
fun _ =>
nat)
F_pathlen a.
Lemma pathlen_unroll:
forall a,
pathlen a =
match M.get a uf.(
m)
with Some a' =>
S(
pathlen a') |
None =>
O end.
Proof.
Lemma pathlen_none:
forall a,
M.get a uf.(
m) =
None ->
pathlen a = 0.
Proof.
Lemma pathlen_some:
forall a a',
M.get a uf.(
m) =
Some a' ->
pathlen a =
S (
pathlen a').
Proof.
Lemma pathlen_zero:
forall a,
repr uf a =
a <->
pathlen a =
O.
Proof.
End PATHLEN.
Lemma pathlen_merge:
forall uf a b x,
pathlen (
merge uf a b)
x =
if M.elt_eq (
repr uf a) (
repr uf b)
then
pathlen uf x
else if M.elt_eq (
repr uf x) (
repr uf a)
then
pathlen uf x +
pathlen uf b + 1
else
pathlen uf x.
Proof.
Lemma pathlen_gt_merge:
forall uf a b x y,
repr uf x =
repr uf y ->
pathlen uf x >
pathlen uf y ->
pathlen (
merge uf a b)
x >
pathlen (
merge uf a b)
y.
Proof.
Section COMPRESS.
Variable uf:
t.
Variable a b:
elt.
Hypothesis a_diff_b:
a <>
b.
Hypothesis a_repr_b:
repr uf a =
b.
Lemma compress_order:
forall x y,
order (
M.set a b uf.(
m))
y x ->
order uf.(
m)
y x \/ (
x =
a /\
y =
b).
Proof.
Remark compress_Acc:
forall x,
Acc (
order uf.(
m))
x ->
Acc (
order (
M.set a b uf.(
m)))
x.
Proof.
induction 1.
constructor;
intros.
destruct (
compress_order _ _ H1)
as [
A | [
A B]].
auto.
subst x y.
constructor;
intros.
destruct (
compress_order _ _ H2)
as [
A | [
A B]].
red in A.
generalize (
repr_res_none uf a).
congruence.
congruence.
Qed.
Lemma compress_wf:
well_founded (
order (
M.set a b uf.(
m))).
Proof.
Definition compress :=
mk (
M.set a b uf.(
m))
compress_wf.
Lemma repr_compress:
forall x,
repr compress x =
repr uf x.
Proof.
End COMPRESS.
Section FIND.
Variable uf:
t.
Program Fixpoint find_x (
a:
elt) {
wf (
order uf.(
m))
a} :
{
r:
elt *
t |
fst r =
repr uf a /\
forall x,
repr (
snd r)
x =
repr uf x } :=
match M.get a uf.(
m)
with
|
Some a' =>
match find_x a'
with
|
pair b uf' => (
b,
compress uf'
a b _ _)
end
|
None => (
a,
uf)
end.
Next Obligation.
red. auto.
Qed.
Next Obligation.
a <> b*)
destruct (
find_x a')
as [[
b'
uf''] [
A B]].
simpl in *.
inv Heq_anonymous0.
apply repr_some_diff.
auto.
Qed.
Next Obligation.
destruct (
find_x a')
as [[
b'
uf''] [
A B]].
simpl in *.
inv Heq_anonymous0.
rewrite B.
apply repr_some.
auto.
Qed.
Next Obligation.
split.
destruct (
find_x a')
as [[
b'
uf''] [
A B]].
simpl in *.
inv Heq_anonymous0.
symmetry.
apply repr_some.
auto.
intros.
rewrite repr_compress.
destruct (
find_x a')
as [[
b'
uf''] [
A B]].
simpl in *.
inv Heq_anonymous0.
auto.
Qed.
Next Obligation.
split;
auto.
symmetry.
apply repr_none.
auto.
Qed.
Next Obligation.
Definition find (
a:
elt) :
elt *
t :=
proj1_sig (
find_x a).
Lemma find_repr:
forall a,
fst (
find a) =
repr uf a.
Proof.
unfold find;
intros.
destruct (
find_x a)
as [[
b uf'] [
A B]].
simpl.
auto.
Qed.
Lemma find_unchanged:
forall a x,
repr (
snd (
find a))
x =
repr uf x.
Proof.
unfold find;
intros.
destruct (
find_x a)
as [[
b uf'] [
A B]].
simpl.
auto.
Qed.
Lemma sameclass_find_1:
forall a x y,
sameclass (
snd (
find a))
x y <->
sameclass uf x y.
Proof.
Lemma sameclass_find_2:
forall a,
sameclass uf a (
fst (
find a)).
Proof.
Lemma sameclass_find_3:
forall a,
sameclass (
snd (
find a))
a (
fst (
find a)).
Proof.
End FIND.
End UF.