Commit dd60afd4 authored by Armaël Guéneau's avatar Armaël Guéneau

Progress on examples/DFS/StackDFS_proof.v

parent 442326ee
......@@ -75,9 +75,8 @@ let reachable_imperative g a b =
let i = Stack.pop s in
Graph.iter_edges g i (fun j ->
if not c.(j) then begin
c.(i) <- true;
Stack.push i s;
c.(j) <- true;
Stack.push j s;
end);
done;
c.(b)
......@@ -18,6 +18,15 @@ Import Stack_ml.
Definition Stack A (L:list A) (p:loc) :=
p ~~> L.
Lemma affine_Stack : forall A p (L: list A),
affine (p ~> Stack L).
Proof.
intros. unfold Stack, hdata. affine.
Qed.
(* Hint Resolve affine_Stack : affine. *)
(* Transparency issues... FIXME? *)
Lemma create_spec : forall A,
app create [tt]
PRE \[]
......@@ -59,7 +68,7 @@ End Stack_proof.
(* Note: [E] describes set of edges left to process in the loop *)
(* - [L] describes the contents of the stack
(* - [L] describes the contents of the stack
- [a] describes the source
- [n] describes the number of nodes in [G]
- [E] describes a set of vertices: the neighbors of the currently processed vertex *)
......@@ -75,37 +84,51 @@ Record inv (G:graph) (n:int) (a:int) (C:list bool) (L:list int) (E:set int) := {
mem i L \/ C[j] = true \/ j \in E }.
Lemma inv_init : forall G n a C,
C = LibListZ.make n false ->
index a n ->
C = LibListZ.make n false ->
a \in nodes G ->
inv G n a (C[a:=true]) (a :: nil) \{}.
Proof.
introv EC Ga. constructors.
{ skip. }
{ skip. }
{ introv H. inverts H as H. skip. inverts H. }
{ introv Gi H. skip_rewrite (i = a).
exists (nil:path). constructors*. }
{ introv Ci E. skip_rewrite (i = a). left*. }
introv Ha EC Ga. constructors.
{ subst C. rew_array~. destruct~ Ha. }
{ rew_array. case_if~. subst C. apply~ index_make. }
{ introv H. inverts H as H.
{ splits~. rew_array~. case_if~. }
{ inverts H. } }
{ introv Gi H. assert (i = a) as ->.
{ subst C. rew_array~ in H. case_if~. }
exists (nil:path). constructors*. }
{ introv Ci E. assert (i = a) as ->.
{ subst C. rew_array~ in Ci. case_if~. }
left*. }
Qed.
Lemma inv_step_push : forall G n a C L i j js,
inv G n a C L ('{j} \u js) ->
C[i] = true ->
C[i] = true ->
has_edge G i j ->
inv G n a (C[i:=true]) (i :: L) js.
inv G n a (C[j:=true]) (j :: L) js.
Proof.
introv I Ci M. inverts I. constructors.
{ skip. }
{ skip. }
{ intros i' M'. skip. }
{ skip. (* extend path with edge at end *) }
{ intros i' j' Ci' E.
(* two cases: i is i' or not. If so, wrote true *)
skip. }
{ rew_array~. }
{ rew_array~. case_if~. }
{ intros i' M'. rew_listx in M'. destruct M' as [-> | M'].
- splits. now applys~ (>> has_edge_nodes i j). rew_array~. case_if~.
- rew_array~. case_if~. splits~. subst i'. applys~ has_edge_nodes i j. }
{ intros k Hk Ck. rew_array~ in Ck. case_if~. subst k.
forwards~ Ri: inv_true_reachable0 i. { applys~ has_edge_nodes i j. }
skip. (* use rtclosure from LibRelation *) }
{ intros i' j' Ci' E.
rewrite read_update_case in Ci' by skip.
case_if~. { subst i'. rew_listx~. }
forwards~ [H|[H|H]]: inv_true_edges0 i' j'.
- rew_array~. case_if~.
- rew_set in H. branches; auto_tilde. subst j'.
rewrite~ read_update_same. }
Qed.
Lemma inv_step_skip : forall G n a C L j js,
inv G n a C L ('{j} \u js) ->
inv G n a C L ('{j} \u js) ->
C[j] = true ->
inv G n a C L js.
Proof.
......@@ -131,19 +154,37 @@ Proof.
{ applys* inv_true_reachable. }
Qed.
Lemma inv_step_pop : forall G n a C i L,
inv G n a C (i :: L) \{} ->
inv G n a C L (out_edges G i).
Proof.
introv I. destruct I. constructors~.
intros i' j ? ?.
forwards~ [M|[M|M]]: inv_true_edges0 i' j.
rew_listx in M. branches; try tauto. subst i'.
right. right. Search out_edges. rewrite~ out_edges_has_edge.
Qed.
Lemma remove_empty : forall A (E: set A),
E \- \{} = E.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
Lemma remove_all : forall A (E: set A),
E \- E = \{}.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
Lemma reachable_imperative_spec : forall g G a b,
a \in nodes G ->
a \in nodes G ->
b \in nodes G ->
app reachable_imperative [g a b]
INV (g ~> RGraph G)
INV (g ~> RGraph G)
POST (fun (r:bool) => \[r = isTrue (reachable G a b)]).
Proof.
introv Ga Gb. xcf.
xapp. intros Gn. xapp. { skip. (* index *) }
xapp. intros Gn. xapp. { unfold nodes_index in Gn. math. }
intros C0 HC0.
xapp. xapp*. xseq. xapp.
set (hinv := fun E CL =>
let '(C,L) := CL in
set (hinv := fun E C L =>
g ~> RGraph G
\* c ~> Array C
\* s ~> Stack L
......@@ -151,42 +192,42 @@ Proof.
(* TODO: fix termination
set (W := lexico2 (binary_map (count (= true)) (upto n))
(binary_map (fun L:list int => LibList.length L) (downto 0))). *)
set (K := (fun CL => bool_of (let '(C,L) := CL : array bool * list int in
L <> nil))).
xseq (# Hexists C, hinv \{} (C,nil)).
xwhile_inv_skip (fun (b:bool) => Hexists C L, hinv \{} (C,L) \* \[b = isTrue (L<>nil)]).
(* TODO: xwhile_inv_basic (hinv \{}) W *)
{ unfold hinv.
evar (X:list bool); evar (Y:list int); hsimpl (X,Y); subst X Y; eauto.
apply* inv_init. }
{ intros S LS r HS. xpull ;=> C L I Er. (* TODO: why is hinv unfolded ?*)
set (K := (fun (C: array bool) (L: list int) => bool_of (L <> nil))).
xseq (# Hexists C, hinv \{} C nil).
xwhile_inv_skip (fun (b:bool) => Hexists C L, hinv \{} C L \* \[b = isTrue (L<>nil)]).
(* TODO: xwhile_inv_basic (hinv \{}) W *)
{ unfold hinv. hsimpl~. apply* inv_init. }
{ intros S LS r HS. unfold hinv at 1. xpull ;=> C L I Er.
(* while condition *)
xlet. xapps. xret. xpull ;=> E.
xlet. xapps. xret. xpull ;=> E.
(* todo: simplify E *)
xif.
{ (* case loop step *)
xseq. xapp*. intros L' HL'. subst L.
xfun as f. forwards~ [Gi Ci]: inv_stack I i.
xapp (fun E => Hexists CL, hinv E CL) G.
xseq (Hexists C L, hinv \{} C L).
xapp*. intros L' HL'. subst L.
xfun as f. forwards~ [Gi Ci]: inv_stack I i.
xapp (fun E => Hexists C2 L2, hinv (out_edges G i \- E) C2 L2 \* \[ C2[i] = true ]) G.
{ auto. }
{ unfold hinv. intros. skip. (* applys heap_contains_intro. *) }
{ introv N Hij. xpull. intros (C2&L2). xapp_spec Sf.
skip. (* loop *) }
{ skip. (* unfold hinv. hsimpl (C,L'). *) }
{ skip. }
{ skip. (* xapplys HS. *) }
(* Notes...
{ intros E. xapp_body. clear Sf. intros ?. intro_subst.
clears W K C. clears L'. unfold hinv at 1. xextract. intros [C L]. xextract as I.
xapps. skip. xif.
xapp*. skip. xapp. unfold hinv. hsimpl (C[i:=true],i::L).
applys inv_step_push. eauto. skip. (* come from pop of L' *) eauto.
xret. unfold hinv. hsimpl (C,L). apply* inv_step_skip. *)
}
{ unfold hinv. intros. skip.
(* eapply heap_contains_intro. (* evar context issues? *) skip. skip. *) }
{ introv N Hij. xpull. intros C2 L2 ?. xapp_spec Sf.
unfold hinv at 1. xpull. intros I'.
xapps. skip.
xif.
{ xapps. skip. xapp. intros _. unfold hinv. hsimpl.
{ rewrite read_update_case. case_if~. skip. }
applys~ inv_step_push i. equates 1. applys~ I'. skip. }
{ xrets. unfold hinv. hsimpl.
{ applys~ inv_step_skip j. equates 1. applys~ I'. skip. }
auto. } }
{ unfold hinv. hsimpl. rewrite remove_empty. apply~ inv_step_pop. }
{ rew_bool_eq~. }
{ intros r'. hpull;=> C2 L2 ?. rewrite remove_all. hsimpl. }
{ intros C2 L2. xapplys~ HS. } }
{ (* case loop end *)
xret. subst L. hsimpl*. { rew_bool_eq*. } } }
xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }
{ intros r. hpull ;=> C L E. rew_bool_eq in *. subst L. hsimpl C. }
{ clear hinv K. intros C I. lets: inv_length_C I.
xapp*. hsimpl. skip. (* TODO affine *)
{ unfolds hinv. clear hinv K. intro C. xpull. intros I. lets: inv_length_C I.
xapp*. hsimpl. apply affine_Stack.
forwards R: inv_end I Gb. subst r. extens. rew_bool_eq*. }
Admitted.
Admitted.
\ No newline at end of file
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