From aa1fc8e535eadd53a7269088e5e2f9cf0dc3d993 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 16 Nov 2020 06:09:17 +0100
Subject: Proof of UnionFind.pathlen_union

helps to understand the difference between union and merge in the interface
---
 lib/UnionFind.v | 63 ++++++++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 53 insertions(+), 10 deletions(-)

(limited to 'lib')

diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 20bb91cd..bd1b763b 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. omega.
-  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)); omega.
-  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 omega.
+      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)); omega.
+  + 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 omega.
+      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:
-- 
cgit