Commit b3770156 authored by charguer's avatar charguer
Browse files

Merge branch 'master' of gitlab.inria.fr:charguer/cfml

parents e90f17d7 0e01d34e
(** Functional queue represented as a pair of lists:
- the front list stores elements in order of exit
- the back list stores elements in reverse order.
The structure maintains the front list nonempty
whenever possible. *)
(** Functional queue represented as a pair of lists.
The pair (front,back) represents the list [front ++ rev back].
The front list is maintained nonempty for nonempty queues. *)
type 'a queue = 'a list * 'a list
......@@ -14,13 +13,13 @@ let is_empty q =
| _ -> false
let check = function
| [], r -> (List.rev r, [])
| [], b -> (List.rev b, [])
| q -> q
let push (f,r) x =
check (f, x::r)
let push (f,b) x =
check (f, x::b)
let pop = function
| [], _ -> raise Not_found
| x::f, r -> (x, check (f,r))
| x::f, b -> (x, check (f,b))
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import CFML.CFLib Stdlib.
Require Import FunctionalQueue_ml.
(*******************************************************************)
(** Representation Predicate *)
Definition inv A (L:list A) (q:queue_ A) :=
let (f,r) := q in
(L = f ++ rev r)
/\ (f = nil -> r = nil).
(** [inv L (f,b)] asserts that [L] describes the items stored in
the queue represented as [(f,b)], from front to back. *)
Definition inv A (L:list A) (q:queue_ A) : Prop :=
let (f,b) := q in
(L = f ++ rev b)
/\ (f = nil -> b = nil).
(*******************************************************************)
......@@ -34,16 +36,9 @@ Lemma is_empty_spec : forall A (L:list A) q,
PRE \[]
POST (fun b => \[b = isTrue (L = nil)]).
Proof.
intros A L (f,r) [I1 I2]. xcf. dup.
(* Detailed proof *)
{ xmatch.
{ xret. xsimpl. rewrite I1. rewrite I2. auto. auto. }
{ xret. xsimpl. rewrite I1. applys app_not_empty_l.
intros E. subst. false* C. } }
(* Shorter proof *)
{ xmatch; xrets.
{ rewrite* I2 in I1. }
{ subst L. applys* app_not_empty_l. intros ->. false* C . } }
intros A L (f,b) [I1 I2]. xcf. xmatch; xrets.
{ rewrite* I2 in I1. }
{ subst L. applys* app_not_empty_l. intros ->. false* C. }
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
......@@ -52,14 +47,13 @@ Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Check *)
Lemma check_spec : forall A (f r : list A),
app check [(f,r)]
Lemma check_spec : forall A (f b:list A),
app check [(f,b)]
PRE \[]
POST (fun q => \[inv (f ++ rev r) q]).
POST (fun q => \[inv (f ++ rev b) q]).
Proof.
xcf. xmatch.
{ (* xlet as f. xret. xpull. intros E. xret. xsimpl. unfolds. rew_list*. *)
xrets. xrets. unfolds. rew_list*. }
{ xrets. xrets. unfolds. rew_list*. }
{ xrets. split. { auto. } { intros ->. false* C. } }
Qed.
......@@ -69,23 +63,40 @@ Hint Extern 1 (RegisterSpec check) => Provide check_spec.
(*******************************************************************)
(** Push *)
(** Source code desugared as
[[
let push q x =
match q with (f,b) -> check (f, x::b)
]]
*)
Lemma push_spec : forall A (L:list A) q x,
inv L q ->
app push [q x]
PRE \[]
POST (fun q' => \[inv (L ++ x::nil) q']).
Proof.
intros A L [f r] x [I1 I2]. xcf. xmatch. xapp.
xpull. intros I'. xsimpl. rewrite I1.
rew_list in *. auto.
intros A L [f b] x [I1 I2]. xcf. xmatch. xapp.
xpull. intros I'. xsimpl. subst L. rew_list in *. auto.
Qed.
(* Note: [(L ++ x::nil)] gets displayed as [L & x]. *)
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(*******************************************************************)
(** Pop *)
(** Source code desugared as
[[
let pop q =
match q with
| [], _ -> raise Not_found
| x::f, b -> let x1__ = check (f,b) in (x, x1__)
]]
*)
Lemma pop_spec : forall A (L:list A) q,
inv L q ->
L <> nil ->
......@@ -93,7 +104,7 @@ Lemma pop_spec : forall A (L:list A) q,
PRE \[]
POST (fun '(x, q') => \[exists L', L = x::L' /\ inv L' q']).
Proof.
intros A L [f r] [I1 I2] N. xcf. xmatch.
intros A L [f b] [I1 I2] N. xcf. xmatch.
{ xfail. rewrite* I2 in I1. }
{ xapp. intros I'. xrets. rew_list in *. eauto. }
Qed.
......
(** Mutable queue, represented as a record with two lists,
and a size field. *)
(** Mutable queue, represented with two lists and a size field.
The items stored in the queue [q] are described by the
list [q.front ++ rev q.back]. *)
type 'a t = {
mutable front : 'a list;
......@@ -11,12 +13,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,10 +29,16 @@ 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] *)
let transfer q1 q2 =
while not (is_empty q1) do
push (pop q1) q2
done
\ No newline at end of file
done
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import CFML.CFLib Stdlib CFMLAdditions.
Require Import MutableQueue_ml.
Require Import TLC.LibListZ.
Require Import CFMLAdditions.
Implicit Types n : int.
Implicit Types q : loc.
......@@ -12,11 +10,25 @@ Implicit Types q : loc.
(*******************************************************************)
(** Representation Predicate *)
Definition Queue A (L:list A) (q:t_ A) :=
(** [q ~> Queue L] is a notation of [Queue L q], a heap
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: 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
the type of memory locations in CFML. *)
(*******************************************************************)
(** Unfolding and folding of the representation predicate *)
......@@ -37,12 +49,7 @@ Proof using. intros. xunfolds* Queue. Qed.
Arguments Queue_close : clear implicits.
(** Customization of [xopen] and [xclose] tactics for [Stack].
These tactics avoid the need to call [hchange] or [xchange]
by providing explicitly the lemmas [Queue_open] and [Queue_close].
Note that the number of underscores avec [Queue] after the [RegisterOpen]
needs to match the number of arguments of the representation predicate
[Queue], excluding the pointer. (Here, we have one underscore for [L].) *)
(** Customization of [xopen] and [xclose] tactics for [Queue]. *)
Hint Extern 1 (RegisterOpen (Queue _)) =>
Provide Queue_open.
......@@ -53,71 +60,55 @@ Hint Extern 1 (RegisterClose (record_repr _)) =>
(*******************************************************************)
(** Create *)
(** Cusom notation for specifications:
[[
app f [x1 x2]
PRE H
POST (fun r => H')
]]
*)
Lemma create_spec : forall A,
app create [tt]
PRE \[]
POST (fun q => q ~> Queue (@nil A)).
Proof using.
xcf. xapp ;=> r. xclose* r.
(* details: xcf. xapp. intros r. xclose r. auto. xsimpl. *)
xcf. xapp. intros q. xclose q.
{ rew_list. auto. }
{ xsimpl. }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Length *)
Lemma length_spec : forall (A:Type) (L:list A) (q:loc),
app MutableQueue_ml.length [q]
INV (q ~> Queue L)
POST (fun n => \[n = length L]).
(* Details:
app MutableQueue_ml.length [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L). *)
Proof using.
xcf.
xopen q. (* details: xchange (@Stack_open s). *)
xpull ;=> f b n (I1&I2).
xapp. xpull. intros ->.
xclose q. { subst*. } (* details: xchange (@Stack_close s). *)
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 ;=> 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 *)
(**
[[
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
]]
*)
Lemma push_spec : forall A (L:list A) q x,
app push [x q]
PRE (q ~> Queue L)
POST (fun (_:unit) => q ~> Queue (L ++ x::nil)).
Proof using.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xapp. xapps. xapp.
xcf. xopen q. xpull. intros f b n (IL&In).
xapps. xapp. xapps. xapp. intros _.
xclose q. { subst. rew_list. math. }
xsimpl. subst. rew_list*.
{ xsimpl. subst. rew_list. auto. }
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
......@@ -126,6 +117,22 @@ Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(*******************************************************************)
(** Pop *)
(**
[[
let pop q =
if q.front = [] then begin
q.front <- List.rev q.back;
q.back <- [];
end;
match q.front with
| [] -> raise Not_found
| x::f ->
q.front <- f;
q.size <- q.size - 1;
x
]]
*)
Lemma pop_spec : forall A (L:list A) q,
L <> nil ->
app pop [q]
......@@ -136,12 +143,12 @@ Proof using.
xapps. xapps. xpolymorphic_eq.
xseq (fun (_:unit) => Hexists f' b',
q ~> `{ front' := f'; back' := b'; size' := n }
\* \[ L = f' ++ rev b' ] \* \[ f' = nil -> b' = nil ]).
\* \[ L = f' ++ rev b' ] \* \[ f' <> nil ]).
{ xif.
{ xapps. xrets. xapps. xapps. xsimpl. { auto. } { subst. rew_list*. } }
{ xrets. { intros. false. } { auto. } } }
{ xapps. xrets. xapps. xapps. xsimpl.
{ subst*. } { subst. rew_list*. } }
{ xrets*. } }
{ clears f b. intros f b I1 I3. xapps. xmatch.
{ xfail. rewrite I3 in I1. { rew_list in *. false. } { auto. } }
{ xapps. xapps. xapps. xret.
xclose q. { subst L. rew_list in *. math. }
xsimpl. subst L. rew_list*. } }
......@@ -150,6 +157,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 *)
......@@ -161,7 +209,8 @@ Proof using.
xcf. xwhile; [|xok]. intros R LR HR. revert L2.
induction_wf IH: (@list_sub A) L1. hide IH.
intros. applys (rm HR).
xlet (fun b => \[b = isTrue (L1 <> nil)] \* q1 ~> Queue L1 \* q2 ~> Queue L2).
xlet (fun b => \[b = isTrue (L1 <> nil)]
\* q1 ~> Queue L1 \* q2 ~> Queue L2).
{ xapps. xrets. rew_isTrue*. }
intros ->. xif.
{ destruct L1 as [|x L1']; tryfalse.
......
......@@ -6,19 +6,26 @@ Require Export TLC.LibListZ.
Require Export CFMLAdditions.
Section UF.
(** [K] denotes the types of nodes. *)
Context (K : Type) `{IK:Inhab K}.
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 +42,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 +138,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 ->
......@@ -179,7 +186,6 @@ Proof using.
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 P R,
roots P R ->
......@@ -200,7 +206,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 ->
......@@ -252,15 +258,15 @@ Qed.
(** Validity of nodes is preserved during an update operation *)
Lemma udpate_inv : forall L' P a b,
L' = P[a:=b] ->
Lemma udpate_inv : forall P' P a b,
P' = P[a:=b] ->
index P a ->
(forall i, index P i -> index L' i)
/\ (forall i, index L' i -> index P i)
/\ (forall i, index P i -> i <> a -> L'[i] = P[i])
/\ (index P a -> L'[a] = b).
(forall i, index P i -> index P' i)
/\ (forall i, index P' i -> index P i)
/\ (forall i, index P i -> i <> a -> P'[i] = P[i])
/\ (index P a -> P'[a] = b).
Proof using.
introv E Da. subst L'. splits.
introv E Da. subst P'. splits.
{ intros. rewrite index_eq_indom in *. rew_map~. }
{ introv H. applys* index_update_inv Da. }
{ introv H N. rewrite* LibMap.read_update_neq. }
......@@ -270,14 +276,13 @@ 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,
Lemma repr_update_neq : forall P a b P' x z,
repr P x z ->
index P a ->
L' = P[a:=b] ->
index P a -> (* technically not needed *)
P' = P[a:=b] ->
P[a] = a ->
z <> a ->
repr L' x z.
repr P' x z.
Proof using.
introv M Ia E R N. forwards* (I1&_&K1&_): udpate_inv (rm E).
induction M.
......@@ -288,13 +293,13 @@ Qed.
(** Lemma for link operations: case of nodes that do
belong to the component resulting of the link. *)
Lemma repr_update_eq : forall P a b L' x,
Lemma repr_update_eq : forall P a b P' x,
repr P x a ->
L' = P[a:=b] ->
P' = P[a:=b] ->
index P b ->
P[b] = b ->
a <> b ->
repr L' x b.
repr P' x b.
Proof using.
introv M E Ib Rb N. forwards* (I1&_&K1&K2): udpate_inv (rm E).
lets Ra: repr_inv_L M.
......@@ -306,14 +311,14 @@ Qed.
(** A link operation preserves the invariants. *)
Lemma roots_link : forall P L' R R' x y,
Lemma roots_link : forall P P' R R' x y,
R' = link R x y (R y) ->
roots P R ->
L' = P [R x := R y] ->
P' = P [R x := R y] ->
R x <> R y ->
index P x ->
index P y ->
roots L' R'.
roots P' R'.
Proof using. (* Note: this proof uses the hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
forwards* Hx: roots_inv_L_root x HR.
......@@ -323,16 +328,17 @@ 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. *)
Lemma roots_compress : forall P R a L',
Lemma roots_compress : forall P R a P',
roots P R ->
L' = P [a := R a] ->
P' = P [a := R a] ->