Commit 6d631152 authored by charguer's avatar charguer
Browse files

cleanup

parent 0801f9a4
......@@ -11,12 +11,6 @@ let create () =
back = [];
size = 0 }
let length q =
q.size
let is_empty q =
q.size = 0
let push x q =
q.back <- x :: q.back;
q.size <- q.size + 1
......@@ -33,6 +27,12 @@ let pop q =
q.size <- q.size - 1;
x
let length q =
q.size
let is_empty q =
q.size = 0
(** [transfer q1 q2] adds all of [q1]'s elements at the end
of the queue [q2], then clears [q1] *)
......
......@@ -11,16 +11,19 @@ Implicit Types q : loc.
(** Representation Predicate *)
(** [q ~> Queue L] is a notation of [Queue L q], a heap
predicate describing a mutable queue at location [q]
with contents [L]. *)
predicate that describes a mutable queue at location [q]
with items represented by the list [L]. *)
Definition Queue A (L:list A) (q:t_ A) : hprop :=
Hexists (f:list A) (b:list A) (n:int),
q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b /\ n = length L ].
(** Note: to reduce name clashes, field names are suffixed
with a quote symbol. *)
(** Note: OCaml features different namespaces for values,
types, and record fields, but all fall in the same
namespace in Coq. To avoid clashes,
- types are suffixed with a underscore symbol
- field names are suffixed with a quote symbol. *)
(** Note: [q] has type ['a t] is OCaml, translated as [t_ A]
in Coq. The type [t_ A] is defined as [loc], which is
......@@ -74,48 +77,23 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Length *)
(** Push *)
Lemma length_spec : forall (A:Type) (L:list A) (q:loc),
(* app MutableQueue_ml.length [s]
PRE (q ~> Queue L)
POST (fun n => \[n = length L] \* q ~> Queue L).
(**
[[
let push x q =
q.back <- x :: q.back;
q.size <- q.size + 1
]]
The code is A-normalized by CFML as:
[[
let push x q =
let x0__ = q.back in
q.back <- x :: x0__;
let x1__ = q.size in
q.size <- x1__ + 1
]]
*)
app MutableQueue_ml.length [q]
INV (q ~> Queue L)
POST (fun n => \[n = length L]).
Proof using.
xcf.
xopen q. xpull. intros f b n (I1&I2).
xapp. xpull. intros ->.
xclose q. { subst*. }
xsimpl*.
(* Here we have an issue because Coq is unable to infer a type. *)
Unshelve. solve_type.
Qed.
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
(*******************************************************************)
(** Is_empty *)
Lemma is_empty_spec : forall A (L:list A) q,
app is_empty [q]
INV (q ~> Queue L)
POST (fun b => \[b = isTrue (L = nil)]).
Proof using.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xclose* q. xrets.
subst n. rewrite lengthZ_zero_eq_eq_nil. tauto.
Unshelve. solve_type.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Push *)
Lemma push_spec : forall A (L:list A) q x,
app push [x q]
......@@ -174,6 +152,47 @@ Qed.
Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.
(*******************************************************************)
(** Length *)
Lemma length_spec : forall (A:Type) (L:list A) (q:loc),
(* app MutableQueue_ml.length [s]
PRE (q ~> Queue L)
POST (fun n => \[n = length L] \* q ~> Queue L).
*)
app MutableQueue_ml.length [q]
INV (q ~> Queue L)
POST (fun n => \[n = length L]).
Proof using.
xcf.
xopen q. xpull. intros f b n (I1&I2).
xapp. xpull. intros ->.
xclose q. { subst*. }
xsimpl*.
(* Here we have an issue because Coq is unable to infer a type. *)
Unshelve. solve_type.
Qed.
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
(*******************************************************************)
(** Is_empty *)
Lemma is_empty_spec : forall A (L:list A) q,
app is_empty [q]
INV (q ~> Queue L)
POST (fun b => \[b = isTrue (L = nil)]).
Proof using.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xclose* q. xrets.
subst n. rewrite lengthZ_zero_eq_eq_nil. tauto.
Unshelve. solve_type.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Transfer *)
......
......@@ -6,7 +6,6 @@ Require Export TLC.LibListZ.
Require Export CFMLAdditions.
Section UF.
Context (K : Type) `{IK:Inhab K}.
......@@ -14,11 +13,16 @@ Implicit Type P : map K K.
Implicit Type R : K->K.
Implicit Type x y z r s : K.
(*******************************************************************)
(** Union-Find Invariants *)
(** Thereafter, [P] is a map representing the graph made by
"parent" pointers, i.e. Union-Find links. A root is its
own parent.
Thereafter, [R] is a logical function that maps every node
to the root of its component. *)
(** [repr P x z] asserts that [z] is the root of [x], that is,
the end of the linked path that starts from [x]. *)
......@@ -35,9 +39,9 @@ Inductive repr (P:map K K) : K->K->Prop :=
repr P x z.
(** [roots P R] captures the fact that [R] is the function
that computes the roots described by the table [P]. *)
that computes the roots described by the parent table [P]. *)
Definition roots (P:map K K) (R:K->K) :=
Definition roots (P:map K K) (R:K->K) : Prop :=
forall x, index P x -> repr P x (R x).
......@@ -131,7 +135,7 @@ Lemma repr_inv_index_r : forall P x z,
index P z.
Proof using. introv H. induction* H. Qed.
(** [repr] relates nodes to nodes that are roots. *)
(** [repr] relates nodes to nodes that are their own parent. *)
Lemma repr_inv_L : forall P x z,
repr P x z ->
......@@ -200,7 +204,7 @@ Proof using.
forwards~: repr_functional Hx Hx'.
Qed.
(** If [P x = x], then [x] is a root. *)
(** If the parent of [x] is [x], then [x] is a root. *)
Lemma roots_inv_R_root : forall x P R,
roots P R ->
......@@ -270,10 +274,9 @@ Qed.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
(* TODO: index P a is in fact not needed *)
Lemma repr_update_neq : forall P a b L' x z,
repr P x z ->
index P a ->
index P a -> (* technically not needed *)
L' = P[a:=b] ->
P[a] = a ->
z <> a ->
......@@ -323,7 +326,8 @@ Proof using. (* Note: this proof uses the hint [repr_inv_L] *)
{ 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. }
{ rew_logic in C. destruct C as [C1 C2].
applys* repr_update_neq E. }
Qed.
(** A path compression preserves the invariants. *)
......@@ -351,9 +355,9 @@ Proof using.
applys* repr_next y. { rewrite* K1. } } }
Qed.
(*******************************************************************)
(** Lemmas only for UFPointer, for which the domain grows dynamically *)
(** Lemmas only for UFPointer, for which the domain
grows dynamically *)
Lemma index_extends : forall P x a b,
index P x ->
......@@ -364,6 +368,8 @@ Proof using IK.
rewrite LibMap.dom_update. rewrite* @in_union_eq. typeclass.
Qed.
(** Adding a fresh node does not alter existing links. *)
Lemma repr_extends : forall P a b x r,
a \notindom P ->
x \indom P ->
......@@ -372,11 +378,13 @@ Lemma repr_extends : forall P a b x r,
Proof using.
introv Ha Hx HR. gen Hx. induction HR; intros.
{ applys* repr_root. { applys* index_extends. }
rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
rewrite* LibMap.read_update_neq.
{ intro_subst. false* Ha. } }
{ applys* repr_next y.
{ applys* index_extends. }
{ rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
{ applys* IHHR. rewrite* <- index_eq_indom. (* applys* repr_inv_index_l. *) } }
{ rewrite* LibMap.read_update_neq.
{ intro_subst. false* Ha. } }
{ applys* IHHR. rewrite* <- index_eq_indom. } }
Qed.
End UF.
......@@ -14,13 +14,16 @@ Implicit Types t : loc.
(** [UF n R t] is a heap predicate that describes an array [t]
of size [n] representing an instance of the union-find data
structure with respect to the root function [R], with elements
indexed in the range [0...(n-1)]. *)
structure with respect to the root function [R], with
elements indexed in the range [0...(n-1)]. *)
Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
Hexists (P:map int int), t ~> ArrayMap P
\* \[conseq_dom n P /\ roots P R].
(** Note: [conseq_dom n P] asserts that [dom P] is equal to
the range from [0...(n-1)]. *)
(*******************************************************************)
(** Create *)
......
(* Union-find: pointer-based implementation,
simplified by omiting the union-by-rank mechanism *)
(*
type contents = Root | Link of node
and node = contents ref
*)
type contents = Root | Link of contents ref
type node = contents ref
......
(* Union-find: pointer-based implementation *)
(* Union-find: pointer-based implementation
including union-by-rank *)
type rank = int
type contents = Root of rank | Link of contents ref
type contents = Root of int | Link of contents ref
type node = contents ref
......
......@@ -28,8 +28,8 @@ Definition parent (x:loc) (c:contents_) : loc :=
| Link y => y
end.
(** [no_self_link D P] asserts that the target of a [Link] always differs
from the node itself. *)
(** [no_self_link D P] asserts that the target of a [Link]
always differs from the node itself. *)
Definition no_self_link (D:set loc) (P:map loc contents_) : Prop :=
forall x y, x \in D -> P[x] = Link y -> x <> y.
......@@ -69,7 +69,8 @@ Proof using.
applys* index_R. rewrite* index_map_parent_eq.
Qed.
Hint Extern 1 (index (LibMaps.map_ parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (index (LibMaps.map_ parent ?L) ?x) =>
rewrite index_map_parent_eq.
Hint Extern 1 (?x \in dom ?L) => congruence.
Hint Resolve indom_root.
......@@ -87,15 +88,16 @@ Lemma roots_create : forall P R x,
Proof using.
introv HR Hx Rx. unfolds roots.
intros y Hy.
rewrite index_eq_indom in Hy. rewrite LibMaps.dom_map in Hy. rewrite dom_update in Hy.
rewrite in_union_eq in Hy. destruct Hy.
{ forwards* Ry: HR y. rewrite LibMaps.map_update. applys* repr_extends.
rewrite index_eq_indom in Hy. rewrite LibMaps.dom_map in Hy.
rewrite dom_update in Hy. rewrite in_union_eq in Hy. destruct Hy.
{ forwards* Ry: HR y. rewrite LibMaps.map_update.
applys* repr_extends.
{ rewrite* LibMaps.dom_map. }
{ rewrite* LibMaps.dom_map. } }
{ rewrite* @in_single_eq in H. subst y. rewrite LibMaps.map_update. rewrite Rx.
applys repr_root.
{ rewrite* @in_single_eq in H. subst y. rewrite LibMaps.map_update.
rewrite Rx. applys repr_root.
{ rewrite index_eq_indom. rewrite LibMap.dom_update, LibMaps.dom_map.
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. } (* TODO: simpler *)
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. }
{ rewrite* LibMap.read_update_same. }
{ typeclass. } }
Qed.
......@@ -184,7 +186,8 @@ Proof using.
rewrite <- index_map_parent_eq. applys* repr_inv_index_l. }
asserts Ryx: (R y <> x).
{ intros E. forwards* HL'x: roots_inv_L x HR. subst P'.
rewrite* LibMaps.read_map in HL'x. rewrite Hy in HL'x. simpls. false. }
rewrite* LibMaps.read_map in HL'x. rewrite Hy in HL'x.
simpls. false. }
clears P P'. clear P HN. intros Hr P HI. lets (HD&HR&HN&HL): HI.
xapp*. xrets*. applys* inv_compress. } }
Qed.
......@@ -216,15 +219,15 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' P P' x y,
inv D R P ->
R' = link R x y (R y) ->
P' = P[(R x) := Link (R y)] ->
inv D R P ->
x \in D ->
y \in D ->
R x <> R y ->
inv D R' P'.
Proof using.
introv HI ER' EL' Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
introv ER' EL' HI Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D P'. rewrite* dom_update_at_index. }
......@@ -252,12 +255,12 @@ Qed.
(** [inv] is preserved by updating the rank information. *)
Lemma inv_rerank : forall x D P P' R n,
P' = P[R x := Root n] ->
inv D R P ->
x \in D ->
P' = P[R x := Root n] ->
inv D R P'.
Proof using.
introv HI Hd EL'. lets (HD&HR&HN&HL): HI.
introv Hd HI EL'. lets (HD&HR&HN&HL): HI.
asserts ED: (dom P = dom P').
{ subst P'. rewrite* dom_update_at_index.
rewrite* index_eq_indom. rewrite* <- HD. }
......@@ -266,9 +269,11 @@ Proof using.
{ asserts_rewrite* (LibMaps.map_ parent P' = LibMaps.map_ parent P).
{ applys LibMaps.extens. { repeat rewrite LibMaps.dom_map. auto. }
{ intros a Ha. rewrite LibMaps.dom_map in Ha.
rewrite* LibMaps.read_map. rewrite* LibMaps.read_map; [| rewrite* ED].
rewrite* LibMaps.read_map.
rewrite* LibMaps.read_map; [| rewrite* ED].
subst P'. rewrite read_update. case_if.
{ forwards* (m&Hm): roots_inv_L_Root x HI. subst a. rewrite Hm. simple*. }
{ forwards* (m&Hm): roots_inv_L_Root x HI.
subst a. rewrite Hm. simple*. }
{ auto. } } } }
{ auto. }
{ subst P'. unfolds no_self_link. intros a b Ha HLa.
......@@ -283,19 +288,22 @@ Lemma union_spec : forall D R x y,
(fun z => Hexists R', UF D R' \* \[R' = link R x y z]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros P HI. lets (HD&HR&HN&HL): HI.
{ unfold UF.
xpull. intros P HI. lets (HD&HR&HN&HL): HI.
xapps*. xapps*. xmatch.
{ xif.
{ xapps*. xrets*. applys* link_correct. }
{ xif.
{ xapp*. xrets*. rewrite link_sym. applys* link_correct. }
{ xapp*. xrets*. rewrite link_sym.
applys* link_correct. }
{ xapp*. sets P': (P[R x:=Root (n + 1)%I]).
asserts ED: (dom P = dom P').
{ unfold P'. rewrite* dom_update_at_index.
rewrite* index_eq_indom. rewrite* <- HD. }
forwards* HRy: indom_root y HI.
xapp*. xrets*. rewrite link_sym. applys* link_correct P'.
subst P'. applys* inv_rerank x. } } }
xapp*. xrets*. rewrite link_sym.
applys* link_correct.
subst P'. applys* inv_rerank. } } }
{ xfail. (* false C0 *)
forwards* (n&En): roots_inv_L_Root x D.
forwards* (m&Em): roots_inv_L_Root y D. } }
......
......@@ -215,15 +215,15 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' P P' x y,
inv D R P ->
R' = link R x y (R y) ->
P' = P[(R x) := Link (R y)] ->
inv D R P ->
x \in D ->
y \in D ->
R x <> R y ->
inv D R' P'.
Proof using.
introv HI ER' EL' Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
introv ER' EL' HI Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D P'. rewrite* dom_update_at_index. }
......@@ -245,7 +245,7 @@ Lemma union_spec : forall D R x y,
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros P HI. lets (HD&HR&HN&HL): HI.
xapp*. xrets*. applys* link_correct x y HI. }
xapp*. xrets*. applys* link_correct. }
{ xrets. rewrite* link_related. }
Qed.
......
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