Commit d417b9c8 authored by charguer's avatar charguer
Browse files

cleanup

parent 8d8dff70
# /home/charguer/versions/coq-8.8.2/cfml/generator/makecmj.native -I /home/charguer/versions/coq-8.8.2/cfml/examples/Tour Stack.mli
# /home/charguer/versions/coq-8.8.2/cfml/generator/main.native -I /home/charguer/versions/coq-8.8.2/cfml/examples/Tour Stack.ml
# coqc -R /home/charguer/.opam/vocal_8.8.2/lib/coq/user-contrib/CFML/Stdlib CFML.Stdlib -R /home/charguer/versions/coq-8.8.2/cfml/examples/Tour EXAMPLE /home/charguer/versions/coq-8.8.2/cfml/examples/Tour/Stack_ml.v
......@@ -5,171 +5,20 @@ Require Import Array_proof.
Require Import UFArray_ml.
Require Import TLC.LibListZ.
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math | typeclass ] ].
Generalizable Variables B.
Lemma index_update_inv : forall A `{Inhab B} (L:map A B) (a x:A) (b:B),
index L a ->
index (L[a:=b]) x ->
index L x.
Proof using.
introv IB Ia Ix. rewrite index_eq_indom in *.
rewrite* dom_update_at_index in Ix.
Qed.
Module Import MArray.
Parameter MArray : forall A, map int A -> loc -> hprop.
Require Import TLC.LibSet.
Open Scope set_scope.
Definition conseq_dom A (n:int) (M:map int A) : Prop :=
dom M = \set{ i | 0 <= i < n }.
Parameter MArray_conseq_dom : forall A (M:map int A) p,
p ~> MArray M ==+> Hexists n, \[conseq_dom n M].
(*******************************************************************)
(** Properties of conseq *)
Lemma conseq_dom_index_eq : forall A n (L:map int A),
conseq_dom n L ->
index n = index L. (* i.e. [index L x <> index n x] *)
Proof using.
introv HD. extens. intros x. rewrite int_index_eq.
rewrite index_eq_indom. unfolds in HD. rewrite HD.
rewrite* in_set_st_eq.
Qed.
Lemma conseq_dom_index_L : forall A n (L:map int A) x,
conseq_dom n L ->
index n x ->
index L x.
Proof. introv Hd Hx. rewrites* <- (>> conseq_dom_index_eq Hd). Qed.
Hint Resolve conseq_dom_index_L.
Lemma conseq_dom_update : forall A n (L:map int A) x y,
conseq_dom n L ->
index n x ->
conseq_dom n (L[x:=y]).
Proof using.
introv HD Hx. unfolds conseq_dom.
rewrite* dom_update_at_index. typeclass.
Qed.
(* TODO: MArray domain *)
(* -------------------------------------------------------------------------- *)
(* [Array.length].
Parameter length_spec :
curried 1%nat Array_ml.length /\
forall A (xs:list A) t,
app Array_ml.length [t]
INV (t ~> Array xs)
POST (fun n => \[n = length xs]).
Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.
*)
(* -------------------------------------------------------------------------- *)
(* [Array.get]. *)
Parameter get_spec :
curried 2%nat Array_ml.get /\
forall A `{Inhab A} (xs:map int A) t i,
index xs i ->
app Array_ml.get [t i]
INV (t ~> MArray xs)
POST \[= xs[i] ].
Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.set]. *)
Parameter set_spec :
curried 2%nat Array_ml.set /\
forall A (xs:map int A) t (i:int) (x:A),
index xs i ->
app Array_ml.set [t i x]
PRE ( t ~> MArray xs)
POST (# t ~> MArray (xs[i:=x])).
Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.make].
Parameter make_spec :
curried 2%nat Array_ml.make /\
forall A n (x:A),
0 <= n ->
app Array_ml.make [n x]
PRE \[]
POST (fun t => Hexists xs, t ~> MArray xs \* \[xs = make n x]).
Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
*)
(* -------------------------------------------------------------------------- *)
(* [Array.init]. *)
Generalizable Variable A.
Axiom init_spec :
forall A (IA:Inhab A) (F : int -> A) (n : int) (f : func),
0 <= n ->
(forall (i : int),
index n i ->
app f [i]
PRE \[] (* simplified spec for now: no state carried through *)
POST (fun (x:A) => \[x = F i])) ->
app Array_ml.init [n f]
PRE \[]
POST (fun t =>
Hexists (xs:map int A), t ~> MArray xs \* \[conseq_dom n xs]
\* \[forall i, index xs i -> xs[i] = F i]).
Hint Extern 1 (RegisterSpec Array_ml.init) => Provide init_spec.
End MArray.
Section UF.
Context (K : Type) `{IK:Inhab K}.
Implicit Type L : map K K.
Implicit Type R : K->K.
Implicit Type x y z r s : K.
Implicit Type L : list int.
Implicit Type R : int->int.
Implicit Type x y z r s : int.
Implicit Types t : loc.
(*******************************************************************)
(** Union-Find Invariants *)
(** Representation Predicate *)
(** [repr L x z] asserts that [z] is the root of [x], that is,
the end of the linked path that starts from [x]. *)
Inductive repr (L:map K K) : K->K->Prop :=
Inductive repr (L:list int) : int->int->Prop :=
| repr_root : forall x,
index L x ->
x = L[x] ->
......@@ -184,9 +33,16 @@ Inductive repr (L:map K K) : K->K->Prop :=
(** [roots L R] captures the fact that [R] is the function
that computes the roots described by the table [L]. *)
Definition roots (L:map K K) (R:K->K) :=
Definition roots (L:list int) (R:int->int) :=
forall x, index L x -> repr L x (R x).
(** [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)]. *)
Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
Hexists (L:list int), t ~> Array L \* \[n = length L /\ roots L R].
......@@ -200,7 +56,7 @@ Implicit Type d : nat.
(** Copy-paste of the definition of [repr], plus a bound on the depth. *)
Inductive reprn L : nat->K->K->Prop :=
Inductive reprn L : nat->int->int->Prop :=
| reprn_root : forall d x,
index L x ->
x = L[x] ->
......@@ -238,6 +94,7 @@ Proof. introv H. induction* H. Qed.
End Reprn.
Hint Resolve repr_of_reprn.
(*******************************************************************)
......@@ -301,20 +158,12 @@ Lemma index_L : forall L R x,
index L (L[x]).
Proof using.
introv HR HI. forwards M: HR HI. inverts M as.
{ introv H1 H2 H3. rewrite* <- H2. }
{ intros. congruence. }
{ intros. applys* repr_inv_index_l. }
Qed.
Hint Resolve index_L.
(** Roots of valid nodes are valid nodes. *)
Lemma index_R : forall L R x,
roots L R ->
index L x ->
index L (R x).
Proof using. introv HR Hx. forwards*: HR Hx. Qed.
(** If [R x = x] then [x] is its own parent. *)
Lemma roots_inv_L : forall x L R,
......@@ -365,6 +214,11 @@ Qed.
(*******************************************************************)
(** Lemmas for specifying and justifying the operations *)
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math ] ].
Hint Resolve index_of_index_length'.
(** Invariants hold for [create] operation. *)
Lemma roots_init : forall L,
......@@ -384,7 +238,7 @@ Definition link R x y :=
Lemma link_related : forall R x y,
R x = R y ->
link R x y = R.
Proof using IK.
Proof using.
introv E. applys fun_ext_1 ;=> i. unfold link. case_if as C.
{ destruct~ C. }
{ auto. }
......@@ -394,7 +248,7 @@ Qed.
Lemma link_inv_related : forall R x y,
R x = R y ->
link R x y = R.
Proof using IK.
Proof using.
introv E. extens ;=> i. unfold link. case_if as C.
{ rewrite E in C. destruct~ C. }
{ auto. }
......@@ -404,38 +258,35 @@ Qed.
Lemma udpate_inv : forall L' L a b,
L' = L[a:=b] ->
index L a ->
(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.
introv E Da. subst L'. splits.
{ intros. rewrite index_eq_indom in *. rew_map~. }
{ introv H. applys~ index_update_inv Da. }
{ introv H N. rewrite* LibMap.read_update_neq. }
{ introv H. rewrite* LibMap.read_update_same. }
intros. subst. splits; intros.
{ rewrite~ @index_update_eq. }
{ rewrite~ @index_update_eq in H. }
{ rewrite~ @read_update_neq. }
{ rewrite~ @read_update_same. }
Qed.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
(* TODO: index L a is in fact not needed *)
Lemma repr_update_neq : forall L a b L' x z,
repr L x z ->
index L a ->
L' = L[a:=b] ->
L[a] = a ->
z <> a ->
repr L' x z.
Proof using.
introv M Ia E R N. forwards~ (I1&_&K1&_): udpate_inv (rm E).
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 for link operations: case of nodes that do
(** Lemma for link operations: case of nodes that do
belong to the component resulting of the link. *)
Lemma repr_update_eq : forall L a b L' x,
......@@ -446,7 +297,7 @@ Lemma repr_update_eq : forall L a b L' x,
a <> b ->
repr L' x b.
Proof using.
introv M E Ib Rb N. forwards~ (I1&_&K1&K2): udpate_inv (rm E).
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.
......@@ -468,7 +319,7 @@ 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.
forwards~ (I1&I2&_&_): udpate_inv E.
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. }
......@@ -486,8 +337,7 @@ Lemma roots_compress : forall L R a L',
Proof using.
introv HR E Da. intros x Dx.
forwards~ Ha: HR a. lets Ra: repr_inv_L Ha.
forwards~ (I1&I2&K1&K2): udpate_inv E.
forwards~ M: HR x.
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. }
......@@ -501,27 +351,6 @@ Proof using.
applys~ repr_next y. { rewrite~ K1. } } }
Qed.
End UF.
(*******************************************************************)
(** Representation predicate *)
Hint Resolve index_of_index_length'.
Implicit Type L : map int int.
Implicit Type R : int->int.
Implicit Type x y z r s : int.
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)]. *)
Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
Hexists (L:map int int), t ~> MArray L \* \[conseq_dom n L /\ roots L R].
(*******************************************************************)
......@@ -531,12 +360,18 @@ Lemma create_spec : forall n,
n >= 0 ->
app create [n]
PRE \[]
POST (fun t => Hexists t R, UF n R t \*
POST (fun t => Hexists t R, UF n R t \*
\[forall x, index n x -> R x = x]).
Proof using.
introv Hn. xcf. xfun. xapp (fun (i:int) => i).
introv Hn. xcf. xfun.
xapp (fun (L:list int) => \[forall (i:int), index L i -> L[i] = i]).
{ math. }
{ intros i Hi. xapp. xrets*. }
{ 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.
......@@ -554,18 +389,18 @@ Lemma find_spec : forall n R t x,
POST (fun r => \[r = R x]).
Proof using.
introv Ix. xunfold UF. xpull. intros L (Hn&HR).
forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx.
forwards* Hx: HR x. forwards (d&Hx'): reprn_of_repr Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros.
xcf. xapps*. xrets. xif.
{ xrets*. forwards* Ex: roots_inv_R_root x L R. congruence. }
{ inverts Hx' as. { intros. false. } intros Ix' N Hy. rename d0 into d.
sets y: (L[x]). lets Ry: repr_of_reprn Hy.
forwards* ER: roots_inv_R y (R x) HR. xapp_spec~ (IH d).
{ subst. rewrites (>> conseq_dom_index_eq Hn). applys* index_L. }
clearbody y. clears L. intros Hr L (Hn&HR).
xapp*. xrets*. splits*.
{ applys* conseq_dom_update. }
sets y: (L[x]). forwards* ER: roots_inv_R y (R x) HR.
xapp_spec* (IH d).
{ subst. applys* index_L. }
{ rewrite* ER. }
clearbody y. clears L. intros Hr L (Hn&HR).
xapp*. xrets*. splits*.
{ rewrite* length_update. }
{ rewrite Hr,ER. applys* roots_compress. } }
Qed.
......@@ -600,12 +435,10 @@ Lemma union_spec : forall n R t x y,
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets. xif.
{ unfold UF. xpull. intros L (Hn&HR).
forwards* IRx: index_R x HR.
xapp*. xsimpl*. splits.
{ applys* conseq_dom_update.
rewrites* (>> conseq_dom_index_eq Hn) in *. }
{ rew_array*. }
{ applys* roots_link L R x y. } }
{ xrets. rewrite~ link_related. }
{ xrets. rewrite* link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......
(*
Set Implicit Arguments.
Require Import CFTactics.
Require Import BatchedQueue_ml.
Module BatchedQueueSpec.
(** instantiations *)
Module Import Q := MLBatchedQueue.
(** invariant *)
Definition inv A (q:queue A) (Q:list A) :=
let (f,r) := q in
Q = (f ++ rev r)
/\ (f = nil -> r = nil).
(** automation *)
Hint Unfold inv.
Ltac auto_tilde ::= eauto.
(** useful facts *)
(** verification *)
Lemma empty_spec : forall A,
inv (@empty A) (@nil A).
Proof.
(* todo arthur: fix display of top_label, and fix tactic below *)
intros. rewrite~ empty_cf.
Qed.
Hint Extern 1 (RegisterSpec empty) => Provide empty_spec.
Lemma is_empty_spec : forall A,
Spec is_empty (q:queue A) |R>> forall Q,
inv q Q ->
R \[] (fun b => \[b = isTrue (Q = nil)]).
Proof.
xcf. intros (f,r) Q [H M].
xmatch; xrets. (* alternative: xgo. *)
fold_bool; rew_refl. (* todo: have a tactic for this *) rewrite~ M in H.
fold_bool; rew_refl. intros E. rewrite E in H.
destruct (nil_eq_app_rev_inv H). false.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
Lemma checkf_spec : forall A,
Spec checkf (q: queue A) |R>> forall Q,
(let (f,r) := q in Q = (f ++ rev r)) ->
R \[] (fun q' => \[inv q' Q]).
Proof.
xcf. intros q Q H.
xmatch.
- xlet; xret.
hsimpl. subst. rewrite~ <-app_nil_r.
- xret. hsimpl. destruct q.
assert (l <> nil) as H1 by congruence.
assert (l = nil -> l0 = nil) by (intro; false).
auto.
Qed.
Hint Extern 1 (RegisterSpec checkf) => Provide checkf_spec.
Lemma pop_spec : forall A,
Spec pop (q: queue A) |R>> forall Q,
inv q Q -> Q <> nil ->
R \[] (fun p => let '(x, q') := p in Hexists Q',
\[Q = x::Q' /\ inv q' Q']).
Proof.
xcf. intros [x q] Q [I1 I2] H.
xmatch.
- xfail. rewrite I2 in I1. apply (H I1). auto.
- xlet. xapp~.
xret. hsimpl. eauto.
Qed.
Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.
Lemma push_spec : forall A,
Spec push (q: queue A) (x: A) |R>> forall Q,
inv q Q ->
R \[] (fun p => \[inv p (Q & x)]).
Proof.
xcf. intros [x' q'] x Q [I1 I2].
xmatch; xapp~.
hsimpl. subst. rewrite~ <-app_rev_cons.
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
End BatchedQueueSpec.
*)
\ No newline at end of file
Set Implicit Arguments.
Require Export CFML.CFLib.
Require Export Stdlib.
Require Export Array_proof.
Require Import TLC.LibListZ.
Require TLC.LibSet.
Generalizable Variables A B.
Ltac auto_typeclass :=
match goal with |- Inhab _ => typeclass end.
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math | auto_typeclass ] ].
Lemma index_update_inv : forall A `{Inhab B} (L:map A B) (a x:A) (b:B),
index L a ->
index (L[a:=b]) x ->
index L x.
Proof using.
introv IB Ia Ix. rewrite index_eq_indom in *.
rewrite* dom_update_at_index in Ix.
Qed.
Module Export MArray.
Parameter MArray : forall A, map int A -> loc -> hprop.
Import TLC.LibSet.
Open Scope set_scope.
Definition conseq_dom A (n:int) (M:map int A) : Prop :=
dom M = \set{ i | 0 <= i < n }.
Parameter MArray_conseq_dom : forall A (M:map int A) p,
p ~> MArray M ==+> Hexists n, \[conseq_dom n M].
(*******************************************************************)
(** Properties of conseq *)
Lemma conseq_dom_index_eq : forall A n (L:map int A),
conseq_dom n L ->
index n = index L. (* i.e. [index L x <> index n x] *)
Proof using.