Commit 7514e94b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Proof of union-find.

parent 34c8f154
......@@ -50,3 +50,4 @@ theories/union_find/math/UnionFind42PotentialCompress.v
theories/union_find/math/UnionFind43PotentialAnalysis.v
theories/union_find/math/UnionFind44PotentialJoin.v
theories/union_find/Code.v
theories/union_find/Proof.v
......@@ -92,13 +92,15 @@ Section TickSpec.
Timeless (TC n).
Proof. exact _. Qed.
Global Instance into_sep_TC_plus m n : IntoSep (TC (m + n)) (TC m) (TC n).
(* We give higher priorities to the (+) instances so that the (S n)
instances are not chosen when m is a constant. *)
Global Instance into_sep_TC_plus m n : IntoSep (TC (m + n)) (TC m) (TC n) | 0.
Proof. by rewrite /IntoSep TC_plus. Qed.
Global Instance from_sep_TC_plus m n : FromSep (TC (m + n)) (TC m) (TC n).
Global Instance from_sep_TC_plus m n : FromSep (TC (m + n)) (TC m) (TC n) | 0.
Proof. by rewrite /FromSep TC_plus. Qed.
Global Instance into_sep_TC_succ n : IntoSep (TC (S n)) (TC 1) (TC n).
Global Instance into_sep_TC_succ n : IntoSep (TC (S n)) (TC 1) (TC n) | 100.
Proof. by rewrite /IntoSep TC_succ. Qed.
Global Instance from_sep_TC_succ n : FromSep (TC (S n)) (TC 1) (TC n).
Global Instance from_sep_TC_succ n : FromSep (TC (S n)) (TC 1) (TC n) | 100.
Proof. by rewrite /FromSep [TC (S n)] TC_succ. Qed.
Definition timeCreditN := nroot .@ "timeCredit".
......
......@@ -56,7 +56,7 @@ Definition link : val := λ: "x" "y",
"x"
else
"y" <- LINK "x";;
"x" <- ROOT ("rx"+#1, "vx");;
"x" <- ROOT (machine_int_add "rx" #1, "vx");;
"x"
| LINK <> =>
assert: #false
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment