Commit 0fb918f4 authored by charguer's avatar charguer
Browse files

uf progress

parent 40a34621
......@@ -16,10 +16,10 @@ let rec find t x =
r
end
let same t x y =
find t x = find t y
let union t x y =
let r = find t x in
let s = find t y in
if r <> s then t.(r) <- s
let same t x y =
find t x = find t y
......@@ -10,16 +10,80 @@ Implicit Type R : int->int.
Implicit Type x y z r s : int.
Implicit Types t : loc.
Ltac auto_star ::= jauto.
(*
(* TODO: notation to generalize and integrate *)
Notation "'\exists' x1 .. xn , H" :=
(heap_is_pack (fun x1 => .. (heap_is_pack (fun xn => H)) ..))
(at level 39, x1 binder, H at level 50, right associativity,
format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'").
Notation "'\exists' x1 , H" := (heap_is_pack (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 x3 x4 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 x3 x4 x5 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 : T1 , H" := (heap_is_pack (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) ( x5 : T5 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, Hexists x5:T5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 x3 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 x3 x4 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 x3 x4 x5 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, Hexists x5:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 , H" :=
(Hexists x1:T1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 x3 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 x3 x4 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 x3 x4 x5 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) x3 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 x5 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 x5 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
......@@ -65,7 +129,7 @@ Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
Section Reprn.
Implicit Type d : nat.
(** Copy-paste of the definition of [repr], plus a bound on the depth *)
(** 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,
......@@ -111,6 +175,8 @@ Hint Resolve repr_of_reprn.
(*******************************************************************)
(** Basic lemmas about [repr] *)
(** [repr] is injective. *)
Lemma repr_inj : forall z1 z2 L x,
repr L x z1 ->
repr L x z2 ->
......@@ -124,6 +190,8 @@ Qed.
Arguments repr_inj : clear implicits.
(** [repr] defines a function. *)
Lemma repr_functional : forall L x z1 z2,
repr L x z1 ->
repr L x z2 ->
......@@ -132,6 +200,8 @@ Proof using.
introv H1 H2. induction H1; inverts H2; try subst; auto_false.
Qed.
(** [repr] only holds of valid nodes. *)
Lemma repr_inv_index_l : forall L x z,
repr L x z ->
index L x.
......@@ -142,22 +212,34 @@ Lemma repr_inv_index_r : forall L x z,
index L z.
Proof using. introv H. induction* H. Qed.
(** [repr] relates nodes to nodes that are roots. *)
Lemma repr_inv_L : forall L x z,
repr L x z ->
L[z] = z.
Proof using. introv H. induction~ H. Qed.
Hint Resolve repr_inv_index_l repr_inv_index_r.
(*******************************************************************)
(** Basic lemmas about [roots] *)
(** Parents of valid nodes are valid nodes. *)
Lemma index_L : forall L R x,
index L x ->
roots L R ->
index L x ->
index L (L[x]).
Proof using.
introv HI HR. forwards M: HR HI. inverts M as.
introv HR HI. 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.
Hint Resolve index_L.
(** If [R x = x] then [x] is its own parent. *)
Lemma roots_inv_L : forall x L R,
roots L R ->
......@@ -169,6 +251,9 @@ Proof using.
lets Ex: repr_inv_L Hx. congruence.
Qed.
(** As corrolary, the parent of [R x] is always [R x]. *)
(* TODO: use directly roots_inv_L *)
Lemma roots_inv_L_root : forall x L R,
roots L R ->
index L x ->
......@@ -177,6 +262,8 @@ Proof using.
introv HR Ix. forwards~ Hx: HR x. applys* repr_inv_L.
Qed.
(** If [repr L x z] then [R x] is [z]. *)
Lemma roots_inv_R : forall x z L R,
roots L R ->
repr L x z ->
......@@ -204,12 +291,24 @@ Qed.
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]. *)
Hint Resolve index_of_index_length'.
(** Invariants hold for [create] operation. *)
Lemma roots_init : forall L,
(forall x, index L x -> L[x] = x) ->
roots L (fun x => x).
Proof using.
introv HL. intros x Hx. applys* repr_root. rewrite* HL.
Qed.
(** Update to [R] when the root of [x] is set to point to the root of [y]. *)
Definition link R x y :=
fun i => If (R i = R x \/ R i = R y) then R y else R i.
(** Linking of nodes in the same component is idempotent. *)
Lemma link_related : forall R x y,
R x = R y ->
link R x y = R.
......@@ -229,6 +328,8 @@ Proof using.
{ auto. }
Qed.
(** Validity of nodes is preserved during an update operation *)
Lemma udpate_inv : forall L' L a b,
L' = L[a:=b] ->
(forall i, index L i -> index L' i)
......@@ -243,6 +344,9 @@ Proof using.
{ rewrite~ @read_update_same. }
Qed.
(** Update of [repr] during a linking operation, for nodes that do not
belong to the two components involved. *)
Lemma repr_update_neq : forall L a b L' x z,
repr L x z ->
L' = L[a:=b] ->
......@@ -256,6 +360,9 @@ Proof using.
{ applys~ repr_next y. rewrite~ K1. }
Qed.
(** Update of [repr] during a linking operation, for nodes that do
belong to the component resulting of the link. *)
Lemma repr_update_eq : forall L a b L' x,
repr L x a ->
L' = L[a:=b] ->
......@@ -272,6 +379,8 @@ Proof using.
{ applys~ repr_next y. rewrite~ K1. }
Qed.
(** Putting it together: invariants are preserved by a link operation. *)
Lemma roots_link : forall L R x y L' R',
R' = link R x y ->
roots L R ->
......@@ -292,6 +401,8 @@ Proof using. (* Note: this proof uses hint [repr_inv_L] *)
{ rew_logic in C. destruct C as [C1 C2]. applys~ repr_update_neq E. }
Qed.
(* TODO: compression *)
Lemma roots_compress' : forall d L R a L' x,
roots L R ->
reprn L d x (R x) ->
......@@ -344,21 +455,34 @@ Qed.
(*******************************************************************)
(** Create *)
Lemma create_spec : forall n R p x y,
Lemma create_spec : forall n,
n >= 0 ->
triple (val_create n)
\[]
(fun t => \exists t R, UF R t \* \[forall i, index n i -> R i = i]).
app create [n]
PRE \[]
POST (fun t => \exists t R, UF n R t \*
\[forall x, index n x -> R x = x]).
Proof using.
introv Hn. xcf. xfun.
xapp (fun (L:list int) => \[forall (i:int), index L i -> L[i] = i]).
{ math. }
{ intros i L Hi Si. xpull. intros K. xapp. xrets.
intros j Hj. rew_list in *.
rewrite read_last_case. case_if.
{ math. }
{ applys K. rewrite index_eq_inbound in *. rew_list in *. math. } }
{ intros i Hi. false. rewrite index_eq_inbound in Hi. rew_list in Hi. math. }
{ intros t. xpull. intros L HL HR. xunfold UF. xsimpl t (fun x => x) L.
{ auto. } { split*. applys* roots_init. } }
Qed.
Hint Extern 1 (Register_spec create) => Provide create_spec.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
(*
Hint Rewrite @index_map_eq : rew_array. (*--TODO move *)
Hint Resolve index_map.
......@@ -419,59 +543,66 @@ Proof using.
{ xsimpl~. } }
{ xvals~. }
Qed.
*)
Lemma find_spec : forall n R p x,
Lemma find_spec : forall n R t x,
index n x ->
triple (val_find p x)
(UF n R p)
(fun r => \[r = R x] \* UF n R p).
app find [t x]
INV (UF n R t)
POST (fun r => \[r = R x]).
Proof using.
introv Ix. xcf. xapps~. xapps~. intros _. xvals~.
introv Ix. xcf.
(* xapps~. xapps~. intros _. xvals~. *) skip. (* TODO *)
Qed.
Hint Extern 1 (Register_spec find) => Provide find_spec.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
(*******************************************************************)
(** Union *)
(** Same *)
Lemma union_spec : forall n R p x y,
Lemma same_spec : forall n R t x y,
index n x ->
index n y ->
triple (val_union p x y)
(UF n R p)
(fun r => \exists R', UF n R' p \* \[R' = link R x y]).
app same [t x y]
INV (UF n R t)
POST (fun b => \[b = isTrue (R x = R y)]).
Proof using.
introv Dx Dy. xcf. xapps~. xapps~. xapps. xif ;=> C.
{ unfold UF. xtpull ;=> L (Hn&HR).
forwards~ Ix: index_of_index_length' (rm Dx) Hn.
forwards~ Iy: index_of_index_length' (rm Dy) Hn.
xapp~. (* todo: xapps does not do the right thing *)
{ xpull ;=> r Er. rewrite~ <- map_update; auto.
xsimpl~. rew_array~. split~.
{ applys~ roots_link L R x y. } } }
{ xvals~. rewrite~ link_related. }
introv Ix Iy. xcf. xapps*. xapps*. xrets.
Qed.
Hint Extern 1 (Register_spec union) => Provide union_spec.
Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Same *)
(** Union *)
Lemma same_spec : forall n R t x y,
Lemma union_spec : forall n R t x y,
index n x ->
index n y ->
app union [t x y]
(UF n R t)
(fun b => UF n R t \* \[b = isTrue (R x = R y)]).
(fun (_:unit) => \exists (R':int->int), UF n R' t \* \[R' = link R x y]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets. xif.
{ unfold UF. xpull. intros L (Hn&HR).
xapp*. xsimpl*. splits.
{ rew_array*. }
{ applys* roots_link L R x y. } }
{ xrets. rewrite* link_related. }
Qed.
Hint Extern 1 (Register_spec same) => Provide same_spec.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
*)
coqide -async-proofs off -async-proofs-command-error-resilience off $*
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