ExampleUnionFind.v 12.9 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10
(**

This file formalizes Union-Find in plain Separation Logic, 
using characteristic formulae.

Author: Arthur Charguéraud.
License: MIT.

*)

charguer's avatar
charguer committed
11

charguer's avatar
charguer committed
12 13 14 15 16 17
Set Implicit Arguments.
Require Import LambdaCF LambdaStruct.
Generalizable Variables A B.

Ltac auto_star ::= jauto.

charguer's avatar
charguer committed
18
Implicit Type p q : loc.
charguer's avatar
charguer committed
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
Implicit Types n : int.


(* ********************************************************************** *)
(* * Union find *)

Require Import LibListZ.

(* ---------------------------------------------------------------------- *)
(** Invariants *)

Implicit Type L : list int.
Implicit Type R : int->int.
Implicit Type x y z : int.

(** [repr L x z] asserts that [z] is the end of the
    path that starts from [x]. *)

Inductive repr L : int->int->Prop := 
  | repr_root : forall x, 
      index L x ->
      x = L[x] ->
      repr L x x
  | repr_next : forall x y z,
      index L x ->
      y = L[x] ->
      x <> y ->
      repr L y z ->
      repr L x z.

(** [roots L R] captures the fact that [R] is the function
    that computes the roots described by the table [L]. *)

Definition roots L R :=
  forall x, index L x -> repr L x (R x).

(** [UF B] is a heap predicate that corresponds to a set of 
    cells describing the union-find structure associated with
    the PER [R], which is a binary relation over locations. *)

Definition UF (n:int) (R:int->int) (p:loc) : hprop :=
  Hexists (L:list int),
     Array (map val_int L) p 
  \* \[n = length L /\ roots L R].


(* ---------------------------------------------------------------------- *)
(** Induction principle on the height of a [repr] derivation *)

(** Ideally, would be automatically generated by Coq *)

Section Reprn.
Implicit Type d : nat.

(** Copy-paste of the definition of [repr], plus a bound on the depth *)

Inductive reprn L : nat->int->int->Prop := 
  | reprn_root : forall d x, 
      index L x ->
      x = L[x] ->
      reprn L d x x
  | reprn_next : forall d x y z,
      index L x ->
      y = L[x] ->
      x <> y ->
      reprn L d y z ->
      reprn L (S d) x z.

Hint Constructors repr reprn.
Hint Extern 1 (_ < _) => math.

Lemma reprn_lt : forall d d' L x z,
  reprn L d x z -> 
  d < d' -> 
  reprn L d' x z.
Proof.
  introv H. gen d'. induction H; introv N; 
   (destruct d' as [|d']; [ false; math | autos* ]).
Qed.

Lemma reprn_of_repr : forall L x z, 
  repr L x z -> 
  exists d, reprn L d x z.
Proof.
  hint reprn_lt. introv H. induction H; try induct_height.
Qed.

Lemma repr_of_reprn : forall L d x z,
  reprn L d x z -> 
  repr L x z. 
Proof. introv H. induction* H. Qed.

End Reprn.

Hint Resolve repr_of_reprn.


(* ---------------------------------------------------------------------- *)
(** Basic lemmas about [repr] *)

Lemma repr_inj : forall z1 z2 L x,
  repr L x z1 -> 
  repr L x z2 -> 
  z1 = z2.
Proof using.
  introv H1 H2. gen z2. 
  induction H1 as [x1 HI1 HE1 | x1 y1 z1 HI1 HE1 HN1 IH]; intros.
  { inverts H2; auto_false. }
  { inverts H2; auto_false. subst y1. applys* IHIH. }
Qed.

charguer's avatar
charguer committed
130
Arguments repr_inj : clear implicits.
charguer's avatar
charguer committed
131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221

Lemma repr_functional : forall L x z1 z2, 
  repr L x z1 -> 
  repr L x z2 -> 
  z1 = z2.
Proof using. 
  introv H1 H2. induction H1; inverts H2; try subst; auto_false. 
Qed.

Lemma repr_inv_index_l : forall L x z, 
  repr L x z -> 
  index L x.
Proof using. introv H. inverts* H. Qed. 

Lemma repr_inv_index_r : forall L x z, 
  repr L x z -> 
  index L z.
Proof using. introv H. induction* H. Qed. 

Lemma repr_inv_L : forall L x z, 
  repr L x z ->
  L[z] = z.
Proof using. introv H. induction~ H. Qed.

Lemma index_L : forall L R x, 
  index L x ->
  roots L R ->
  index L (L[x]).
Proof using.
  introv HI HR. forwards M: HR HI. inverts M as. 
  { congruence. }
  { intros. applys* repr_inv_index_l. }
Qed.

Hint Resolve repr_inv_index_l repr_inv_index_r index_L.

Lemma roots_inv_L : forall x L R,
  roots L R ->
  R x = x ->
  index L x ->
  L[x] = x.
Proof using. 
  introv HR E Ix. forwards~ Hx: HR x.
  lets Ex: repr_inv_L Hx. congruence.
Qed.

Lemma roots_inv_L_root : forall x L R,
  roots L R ->
  index L x ->
  L[R x] = R x.
Proof using. 
  introv HR Ix. forwards~ Hx: HR x. applys* repr_inv_L.
Qed.

Lemma roots_inv_R : forall x z L R,
  roots L R ->
  repr L x z ->
  R x = z.
Proof using.
  introv HR Hx. forwards* Hx': HR x.
  forwards~: repr_functional Hx Hx'.
Qed.

(* not used? *)
Lemma roots_inv_R_root : forall x L R,
  roots L R ->
  L[x] = x ->
  index L x ->
  R x = x.
Proof using.
  introv HR Lx Ix. forwards* Hx': HR x.
  inverts Hx'; congruence.
Qed.


(* ---------------------------------------------------------------------- *)
(** Lemmas for specifying and justifying the operations *)

Ltac auto_tilde ::= 
  try solve [ jauto_set; solve [ eauto | congruence | math ] ].

(** Result of a link operation between [x] and [y] that results
    in establishing a link between the roots of [x] and [y]. *)

Definition link R x y :=
  fun i => If (R i = R x \/ R i = R y) then R y else R i.

Lemma link_related : forall R x y,
  R x = R y ->
  link R x y = R.
Proof using.
charguer's avatar
charguer committed
222
  introv E. applys fun_ext_1 ;=> i. unfold link. case_if as C.
charguer's avatar
charguer committed
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
  { destruct~ C. }
  { auto. }
Qed.

(* TODO: not used? *)
Lemma link_inv_related : forall R x y,
  R x = R y ->
  link R x y = R.
Proof using.
  introv E. extens ;=> i. unfold link. case_if as C.
  { rewrite E in C. destruct~ C. }
  { auto. }
Qed.

Lemma udpate_inv : forall L' L a b,
  L' = L[a:=b] ->
     (forall i, index L i -> index L' i)
  /\ (forall i, index L' i -> index L i)
  /\ (forall i, index L i -> i <> a -> L'[i] = L[i])
  /\ (index L a -> L'[a] = b).
Proof using.
  intros. subst. splits; intros.
  { rewrite~ @index_update_eq. }
  { rewrite~ @index_update_eq in H. }
  { rewrite~ @read_update_neq. }
charguer's avatar
compile  
charguer committed
248
  { rewrite~ @read_update_same. }
charguer's avatar
charguer committed
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
Qed.

Lemma repr_update_neq : forall L a b L' x z,
  repr L x z ->
  L' = L[a:=b] ->
  L[a] = a ->
  z <> a ->
  repr L' x z.
Proof using.
  introv M E R N. lets (I1&_&K1&_): udpate_inv (rm E).
  induction M.
  { applys~ repr_root. rewrite~ K1. }
  { applys~ repr_next y. rewrite~ K1. }
Qed.

Lemma repr_update_eq : forall L a b L' x,
  repr L x a ->
  L' = L[a:=b] ->
  index L b ->
  L[b] = b ->
  a <> b ->
  repr L' x b.
Proof using.
  introv M E Ib Rb N. lets (I1&_&K1&K2): udpate_inv (rm E).
  lets Ra: repr_inv_L M.
  gen_eq a': a. induction M; intros E. 
  { subst x. applys~ repr_next b. rewrite~ K2. 
    applys* repr_root. rewrite~ K1. }
  { applys~ repr_next y. rewrite~ K1. }
Qed.

Lemma roots_link : forall L R x y L' R',
  R' = link R x y ->
  roots L R ->
  L' = L [R x := R y] ->
  R x <> R y ->
  index L x ->
  index L y ->
  roots L' R'.
Proof using. (* Note: this proof uses hint [repr_inv_L] *)
  introv M HR E N Dx Dy. intros u Du.
  forwards~ Hx: roots_inv_L_root x HR. 
  forwards~ Hy: roots_inv_L_root y HR. 
  lets (I1&I2&_&_): udpate_inv E.
  rewrites (rm M). unfold link. case_if as C.
  { destruct C as [C|C].
    { rewrite <- C in E. applys~ repr_update_eq E. }
    { rewrite <- C. applys~ repr_update_neq E. } }
  { rew_logic in C. destruct C as [C1 C2]. applys~ repr_update_neq E. }
Qed.

Lemma roots_compress' : forall d L R a L' x,
  roots L R ->
  reprn L d x (R x) ->
  L' = L [a := R a] ->
  index L x ->
  index L a ->
  reprn L' d x (R x).
Proof using.
  introv HR M E Dx Da. 
  forwards~ Ha: HR a. lets Ra: repr_inv_L Ha. 
  lets (I1&I2&K1&K2): udpate_inv E.
  gen_eq z: (R x). induction M; introv Ez.
  { applys~ reprn_root. tests C: (x = a).
    { rewrite~ K2. }
    { rewrite~ K1. } }
  { tests C: (x = a).
    { subst z. asserts~ Na: (a <> R a).
      applys~ reprn_next (R a).
      { rewrite~ K2. }
      { applys~ reprn_root. rewrite~ K1. } }
    { forwards~ Ez': roots_inv_R y z HR.
      applys~ reprn_next y. { rewrite~ K1. } } }
Qed.

(* derivable from above *)
Lemma roots_compress : forall L R a L',
  roots L R ->
  L' = L [a := R a] ->
  index L a ->
  roots L' R.
Proof using.
  introv HR E Da. intros x Dx.
  forwards~ Ha: HR a. lets Ra: repr_inv_L Ha. 
  lets (I1&I2&K1&K2): udpate_inv E. forwards~ M: HR x.
  gen_eq z: (R x). induction M; introv Ez.
  { applys~ repr_root. tests C: (x = a).
    { rewrite~ K2. }
    { rewrite~ K1. } }
  { tests C: (x = a).
    { subst z. asserts~ Na: (a <> R a).
      applys~ repr_next (R a).
      { rewrite~ K2. }
      { applys~ repr_root. rewrite~ K1. } }
    { forwards~ Ez': roots_inv_R y z HR.
      applys~ repr_next y. { rewrite~ K1. } } }
Qed.



(* ---------------------------------------------------------------------- *)
(** Function to get the root *)

Definition P : var := 0%nat.
Definition X : var := 1%nat.
Definition F : var := 2%nat.
Definition Y : var := 3%nat.
Definition Z : var := 4%nat.

Definition val_root :=
charguer's avatar
charguer committed
359
  (* Vars P, X, F, Y in *)
charguer's avatar
charguer committed
360 361 362 363 364 365 366 367 368
  ValFun P X :=
    LetFix F X :=
      Let Y := val_array_get P X in
      If_ val_eq X Y   
        Then X 
        Else F Y
      in
    F X.

charguer's avatar
compile  
charguer committed
369 370 371
Hint Rewrite @index_map_eq : rew_array. (*--TODO  move *)


charguer's avatar
charguer committed
372 373 374 375 376 377 378 379
Lemma rule_root : forall n R p x,
  index n x ->
  triple (val_root p x)
    (UF n R p)
    (fun r => \[r = R x] \* UF n R p).
Proof using.
  introv Dx. xcf. xval as F ;=> EF.
  unfold UF. xpull ;=> L (Hn&HR).
charguer's avatar
compile  
charguer committed
380
  forwards~ Ix: index_of_index_length' (rm Dx) Hn.
charguer's avatar
charguer committed
381 382 383 384 385
  forwards~ Hx: HR x.
  forwards (d&Hx'): reprn_of_repr Hx.
  applys local_erase. 
  gen x. induction_wf IH: lt_wf d. hide IH. intros. 
  rewrite EF. xcf. rewrite <- EF.
charguer's avatar
compile  
charguer committed
386 387 388
  xapp as vy. rew_array~. rewrite (@read_map int _ val _); auto.
  (* --todo: should be rewrite read_map. *)
  intros Evy. subst vy.
charguer's avatar
charguer committed
389 390 391 392
  xapps. xif ;=> C; inverts Hx' as; try solve [ intros; false ].
  { introv _ _ Ex. xvals~. }
  { rename d0 into d. introv _ _ Nx. sets y: (L[x]).
    forwards~ ER: roots_inv_R y (R x) HR.
charguer's avatar
charguer committed
393
    xapp~ (>> IH d). hsimpl~. }
charguer's avatar
charguer committed
394 395
Qed.

charguer's avatar
charguer committed
396
Hint Extern 1 (Register_spec val_root) => Provide rule_root. 
charguer's avatar
charguer committed
397 398 399 400 401 402


(* ---------------------------------------------------------------------- *)
(** Compression function *)

Definition val_compress :=
charguer's avatar
charguer committed
403
  (* Vars P, X, Z, F, Y in *)
charguer's avatar
charguer committed
404 405 406 407 408 409 410 411 412
  ValFun P X Z :=
    LetFix F X :=
      If_ val_neq X Z Then
        Let Y := val_array_get P X in
        val_array_set P X Z ;;
        F Y
      End in
    F X.

charguer's avatar
charguer committed
413
Hint Resolve index_map. 
charguer's avatar
charguer committed
414 415 416 417 418 419 420 421 422 423

Lemma rule_compress : forall n R p x z,
  index n x ->
  z = R x ->
  triple (val_compress p x z)
    (UF n R p)
    (fun r => \[r = val_unit] \* UF n R p).
Proof using.
  introv Dx Ez. xcf. xval as F ;=> EF.
  unfold UF. xpull ;=> L (Hn&HR).
charguer's avatar
compile  
charguer committed
424
  forwards~ Ix: index_of_index_length' (rm Dx) Hn.
charguer's avatar
charguer committed
425 426 427 428 429 430
  forwards~ Hx: HR x.
  applys local_erase. (* TODO: avoid *)
  forwards (d&Hx'): reprn_of_repr Hx.
  gen L x. induction_wf IH: lt_wf d. hide IH. intros. 
  rewrite EF. xcf. rewrite <- EF.
  xapps. xif ;=> C.
charguer's avatar
compile  
charguer committed
431 432
  { xapps~. xapp~. rewrite (@read_map int _ val _); auto.
    (* --todo: should be rewrite read_map. *)
charguer's avatar
charguer committed
433 434 435
    inverts Hx' as; try solve [ intros; false ].
    introv _ Nx Ry. sets y: (L[x]). rename d0 into d.
    forwards~ ER: roots_inv_R y (R x) HR. 
charguer's avatar
compile  
charguer committed
436
    rewrite <- map_update; auto.
charguer's avatar
charguer committed
437 438 439 440
    sets_eq L': (L[x:=z]).
    forwards~ (I1&I2&K1&K2): udpate_inv L' L x z.
    subst z. forwards~ HR': roots_compress L' HR.
    forwards~ Hy: HR' y.
charguer's avatar
charguer committed
441
    xapp~ (>> IH d). 
charguer's avatar
compile  
charguer committed
442
    { subst L'. rew_array~. } 
charguer's avatar
charguer committed
443 444
    { applys~ roots_compress' HR. } 
    { hsimpl~. } }
charguer's avatar
charguer committed
445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
  { xvals~. }
Qed.

Hint Extern 1 (Register_spec val_compress) => Provide rule_compress.


(** TODO: compress and find revisited using a loop *)

(* ---------------------------------------------------------------------- *)
(** Find function, with path compression *)

Definition val_find :=
  Vars P, X, R in
  ValFun P X :=
    Let R := val_root P X in
    val_compress P X R ;;
    R.

Lemma rule_find : forall n R p x,
  index n x ->
  triple (val_find p x)
    (UF n R p)
    (fun r => \[r = R x] \* UF n R p).
Proof using.
  introv Ix. xcf. xapps~. xapps~. xvals~.
Qed.

Hint Extern 1 (Register_spec val_find) => Provide rule_find.


(* ---------------------------------------------------------------------- *)
(** Union function, with naive linking strategy *)

Definition val_union :=
  Vars P, X, Y, RX, RY in
  ValFun P X Y :=
    Let RX := val_find P X in
    Let RY := val_find P Y in
    If_ val_neq RX RY Then 
      val_array_set P RX RY 
    End.

Lemma rule_union : forall n R p x y,
  index n x ->
  index n y ->
  triple (val_union p x y)
    (UF n R p)
    (fun r => \[r = val_unit] \* Hexists R', UF n R' p \* \[R' = link R x y]).
Proof using.
  introv Dx Dy. xcf. xapps~. xapps~. xapps. xif ;=> C.
  { unfold UF. xpull ;=> L (Hn&HR).
charguer's avatar
compile  
charguer committed
496 497
    forwards~ Ix: index_of_index_length' (rm Dx) Hn.
    forwards~ Iy: index_of_index_length' (rm Dy) Hn.
charguer's avatar
charguer committed
498
    xapp~. (* todo: xapps does not do the right thing *)
charguer's avatar
compile  
charguer committed
499 500
    { hpull ;=> r Er. rewrite~ <- map_update; auto.
      hsimpl~. rew_array~. split~.
charguer's avatar
charguer committed
501 502 503 504 505 506
      { applys~ roots_link L R x y. } } }
  { xvals~. rewrite~ link_related. }
Qed.

Hint Extern 1 (Register_spec val_union) => Provide rule_union.

charguer's avatar
charguer committed
507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535









(* ---------------------------------------------------------------------- *)
(** Initialization function *)

(* LATER

  let val_create = 
    Vars N, I in
    Fun N := 
      val_array_init (Fun I := I) N.

Parameter val_create : val.

Parameter rule_create : forall n,
  n >= 0 ->
  triple (val_create n)
    \[]
    (fun r => Hexists p R, \[r = val_loc p] \*
              UF R p \* \[forall i, index n i -> R i = i]).

*)