Generalize mergingLogic

huynhtrankhanh · Nov 12, 2024 · 9249b90 · 9249b90
1 parent b892e27
commit 9249b90
Show file tree

Hide file tree

Showing 2 changed files with 100 additions and 97 deletions.
diff --git a/theories/DisjointSetUnionCode.v b/theories/DisjointSetUnionCode.v
@@ -514,7 +514,6 @@ Qed.
 
 Lemma doubleBangEqIfNthEq {A} (l l1 : list A) (hL : length l = length l1) d (hnth : forall x, x < length l -> nth x l d = nth x l1 d) n : l !! n = l1 !! n.
 Proof.
-Search (_ !! _).
   remember (l !! n) as target1 eqn:h1.
   remember (l1 !! n) as target2 eqn:h2.
   symmetry in h1. symmetry in h2.
@@ -524,12 +523,6 @@ Search (_ !! _).
   rewrite !nth_lookup, h1, h2 in t. simpl in t. congruence.
 Qed.
 
-Lemma pathCompressCommute (dsu : list Slot) (h1 : noIllegalIndices dsu) (h2 : withoutCyclesN dsu (length dsu)) (fuel : nat) (a b : nat) (hA : a < length dsu) (hB : b < length dsu) : pathCompress (pathCompress dsu fuel a (ancestor dsu (length dsu) a)) fuel b (ancestor dsu (length dsu) b) = pathCompress (pathCompress dsu fuel b (ancestor dsu (length dsu) b)) fuel a (ancestor dsu (length dsu) a).
-Proof.
-  apply list_eq. intro i.
-
-Admitted.
-
 Definition performMerge (dsu : list Slot) (tree1 tree2 : Tree) (u v : nat) :=
   <[u := ReferTo v]> (<[v := Ancestor (Unite tree2 tree1)]> dsu).