Library UnionFind
A persistent union-find data structure.
Require Import Wf.
Require Recdef.
Require Setoid.
Require Coq.Program.Wf.
Require Import Coqlib.
Open Scope nat_scope.
Set Implicit Arguments.
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.
Section REPR.
Variable uf: t.
Function repr (a: elt) {wf (order uf.(m)) a} : elt :=
match M.get a uf.(m) with
| Some a' => repr a'
| None => a
end.
Lemma repr_none:
forall a,
M.get a uf.(m) = None ->
repr a = a.
Lemma repr_some:
forall a a',
M.get a uf.(m) = Some a' ->
repr a = repr a'.
Lemma repr_res_none:
forall (a: elt), M.get (repr a) uf.(m) = None.
Lemma repr_canonical:
forall (a: elt), repr (repr a) = repr a.
Lemma repr_some_diff:
forall a a', M.get a uf.(m) = Some a' -> a <> repr a'.
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.
Lemma sameclass_sym:
forall uf a b, sameclass uf a b -> sameclass uf b a.
Lemma sameclass_trans:
forall uf a b c,
sameclass uf a b -> sameclass uf b c -> sameclass uf a c.
Lemma sameclass_repr:
forall uf a, sameclass uf a (repr uf a).
Lemma wf_empty:
well_founded (order (M.empty elt)).
Definition empty : t := mk (M.empty elt) wf_empty.
Lemma repr_empty:
forall a, repr empty a = a.
Lemma sameclass_empty:
forall a b, sameclass empty a b -> a = b.
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).
Remark identify_Acc_b:
forall x,
Acc (order uf.(m)) x -> repr uf x <> a -> Acc (order (M.set a b uf.(m))) x.
Remark identify_Acc:
forall x,
Acc (order uf.(m)) x -> Acc (order (M.set a b uf.(m))) x.
Lemma identify_wf:
well_founded (order (M.set a b uf.(m))).
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.
Lemma repr_identify_2:
forall x, repr uf x = a -> repr identify x = repr uf b.
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.
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.
Lemma repr_union_2:
forall uf a b x, repr uf x = repr uf a -> repr (union uf a b) x = repr uf b.
Lemma repr_union_3:
forall uf a b, repr (union uf a b) b = repr uf b.
Lemma sameclass_union_1:
forall uf a b, sameclass (union uf a b) a b.
Lemma sameclass_union_2:
forall uf a b x y, sameclass uf x y -> sameclass (union uf a b) x y.
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.
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.
Lemma sameclass_merge:
forall uf a b x y, sameclass (merge uf a b) x y <-> sameclass (union uf a b) x y.
Definition path_ord (uf: t) : elt -> elt -> Prop := order uf.(m).
Lemma path_ord_wellfounded:
forall uf, well_founded (path_ord uf).
Lemma path_ord_canonical:
forall uf x y, repr uf x = x -> ~path_ord uf y x.
Lemma path_ord_merge_1:
forall uf a b x y,
path_ord uf x y -> path_ord (merge uf a b) x y.
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).
Section PATHLEN.
Variable uf: t.
Function pathlen (a: elt) {wf (order uf.(m)) a} : nat :=
match M.get a uf.(m) with
| Some a' => S (pathlen a')
| None => O
end.
Lemma pathlen_none:
forall a,
M.get a uf.(m) = None ->
pathlen a = 0.
Lemma pathlen_some:
forall a a',
M.get a uf.(m) = Some a' ->
pathlen a = S (pathlen a').
Lemma pathlen_zero:
forall a, repr uf a = a <-> pathlen a = O.
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.
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.
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).
Remark compress_Acc:
forall x,
Acc (order uf.(m)) x -> Acc (order (M.set a b uf.(m))) x.
Lemma compress_wf:
well_founded (order (M.set a b uf.(m))).
Definition compress := mk (M.set a b uf.(m)) compress_wf.
Lemma repr_compress:
forall x, repr compress x = repr uf x.
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.
Next Obligation.
destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
(find_x_obligation_1 a find_x a' Heq_anonymous)))
as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
apply repr_some_diff. auto.
Next Obligation.
destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
(find_x_obligation_1 a find_x a' Heq_anonymous)))
as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
rewrite B. apply repr_some. auto.
Next Obligation.
split.
destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
(find_x_obligation_1 a find_x a' Heq_anonymous)))
as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
symmetry. apply repr_some. auto.
intros. rewrite repr_compress.
destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a'
(find_x_obligation_1 a find_x a' Heq_anonymous)))
as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto.
Next Obligation.
split; auto. symmetry. apply repr_none. auto.
Next Obligation.
apply mwf.
Definition find (a: elt) : elt * t := proj1_sig (find_x a).
Lemma find_repr:
forall a, fst (find a) = repr uf a.
Lemma find_unchanged:
forall a x, repr (snd (find a)) x = repr uf x.
Lemma sameclass_find_1:
forall a x y, sameclass (snd (find a)) x y <-> sameclass uf x y.
Lemma sameclass_find_2:
forall a, sameclass uf a (fst (find a)).
Lemma sameclass_find_3:
forall a, sameclass (snd (find a)) a (fst (find a)).
End FIND.
End UF.