From 31f036c9fc391f12c077f78027a73a93c3898560 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?= Date: Sat, 16 Nov 2024 15:06:07 +0000 Subject: [PATCH] Add an if guard in dsuFromInteractions --- theories/DisjointSetUnionCode.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/DisjointSetUnionCode.v b/theories/DisjointSetUnionCode.v index f59b90f..e298dc8 100644 --- a/theories/DisjointSetUnionCode.v +++ b/theories/DisjointSetUnionCode.v @@ -569,7 +569,7 @@ Definition unite (dsu : list Slot) (a b : nat) := Fixpoint dsuFromInteractions (dsu : list Slot) (interactions : list (nat * nat)) := match interactions with | [] => dsu - | (a, b)::tail => dsuFromInteractions (unite dsu a b) tail + | (a, b)::tail => if decide (a < length dsu /\ b < length dsu) then dsuFromInteractions (unite dsu a b) tail else dsuFromInteractions dsu tail end. Lemma pathCompressPreservesLength (dsu : list Slot) (n a b : nat) : length (pathCompress dsu n a b) = length dsu.