diff options
Diffstat (limited to 'lib/UnionFind.v')
-rw-r--r-- | lib/UnionFind.v | 63 |
1 files changed, 53 insertions, 10 deletions
diff --git a/lib/UnionFind.v b/lib/UnionFind.v index c4a2f5b1..ae2c30d2 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -124,6 +124,15 @@ Module Type UNIONFIND. pathlen uf x + pathlen uf b + 1 else pathlen uf x. + Axiom pathlen_union: + forall uf a b x, + pathlen (union 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)+1 + else + (pathlen uf x). Axiom pathlen_gt_merge: forall uf a b x y, repr uf x = repr uf y -> @@ -531,6 +540,7 @@ Qed. End PATHLEN. + (* Path length and merge *) Lemma pathlen_merge: @@ -549,16 +559,49 @@ Proof. set (uf' := identify uf (repr uf a) b (repr_res_none uf a) (not_eq_sym n)). pattern x. apply (well_founded_ind (mwf uf')); intros. rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G. - rewrite H; auto. simpl in G. rewrite M.gsspec in G. - destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true. - inversion G. subst x'. rewrite dec_eq_false; auto. - replace (pathlen uf (repr uf a)) with 0. lia. - symmetry. apply pathlen_none. apply repr_res_none. - rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G. - destruct (M.elt_eq (repr uf x') (repr uf a)); lia. - simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate. - rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. - symmetry. apply pathlen_zero; auto. apply repr_none; auto. + + rewrite H; auto. clear H. simpl in G. rewrite M.gsspec in G. + destruct (M.elt_eq x0 (repr uf a)). + - rewrite e, repr_canonical, dec_eq_true. + inversion G. subst x'. rewrite dec_eq_false; auto. + replace (pathlen uf (repr uf a)) with 0; try lia. + symmetry. apply pathlen_none. apply repr_res_none. + - rewrite (repr_unroll uf x0), (pathlen_unroll uf x0), G. + destruct (M.elt_eq (repr uf x') (repr uf a)); lia. + + clear H; simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate. + rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. + symmetry. apply pathlen_zero; auto. apply repr_none; auto. +Qed. + +Lemma pathlen_union: + forall uf a b x, + pathlen (union 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)+1 + else + (pathlen uf x). +Proof. + intros. unfold union. + destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. + set (uf' := identify uf _ _ _ _). + assert (LENa: pathlen uf (repr uf a) = 0). + { apply pathlen_none. apply repr_res_none. } + pattern x. apply (well_founded_ind (mwf uf')); intros. + rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G. + + rewrite H; auto. clear H. simpl in G. rewrite M.gsspec in G. + destruct (M.elt_eq x0 (repr uf a)). + - inversion G; clear G. subst. + rewrite !repr_canonical, dec_eq_true. + rewrite dec_eq_false; auto. + rewrite LENa. rewrite (pathlen_none uf (repr uf b)); try lia. + apply repr_res_none. + - rewrite (repr_unroll uf x0), G, ! (pathlen_some _ _ _ G). + destruct (M.elt_eq _ _); auto. + + clear H. simpl in G. rewrite M.gsspec in G. + destruct (M.elt_eq _ (repr uf a)); try discriminate. + rewrite (repr_none _ _ G), !(pathlen_none _ _ G), dec_eq_false; auto. Qed. Lemma pathlen_gt_merge: |