diff --git a/examples/DFS/StackDFS_proof.v b/examples/DFS/StackDFS_proof.v index 7ddd368466436830d7e978857ae54a730129f4d6..0caf52f6c034fdda42ad1de8ff5f8c4c0c622fb2 100644 --- a/examples/DFS/StackDFS_proof.v +++ b/examples/DFS/StackDFS_proof.v @@ -104,7 +104,7 @@ Proof. Qed. Lemma inv_step_push : forall G n a C L i j js, - inv G n a C L ('{j} \u js) -> + inv G n a C L (js \u \{j}) -> C[i] = true -> has_edge G i j -> inv G n a (C[j:=true]) (j :: L) js. @@ -128,7 +128,7 @@ Proof. 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 (js \u \{j}) -> C[j] = true -> inv G n a C L js. Proof. @@ -173,6 +173,27 @@ Lemma remove_all : forall A (E: set A), E \- E = \{}. Proof. intros. rew_set. intros. rew_set. tauto. Qed. +Lemma iter_edges_remaining_spec : forall (I:set int->hprop) (G:graph) g f i, + i \in nodes G -> + (forall L, (g ~> RGraph G) \c (I L)) -> + (forall j E, j \notin E -> has_edge G i j -> + (app f [j] (I (E \u \{j})) (# I E))) -> + app Graph_ml.iter_edges [g i f] + PRE (I (out_edges G i)) + POST (# I \{}). +Proof. + intros. xapp_spec~ iter_edges_spec (>> (fun E => I (out_edges G i \- E)) G). + { introv Hj Hij. xapp~. + { intro HH. rew_set in HH. tauto. } + { hsimpl. match goal with |- I ?x ==> I ?y \* _ => asserts_rewrite (x = y) end. + { rew_set. intro x. rew_set. rew_logic. iff; unpack. + { tests~: (x = j). } + { tests~: (x = j). branches; [| now false]. tauto. } } + hsimpl. } } + { rewrite remove_empty. hsimpl. } + { rewrite remove_all. hsimpl. } +Qed. + Lemma reachable_imperative_spec : forall g G a b, a \in nodes G -> b \in nodes G -> @@ -206,7 +227,8 @@ Proof. 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. + xapp_spec iter_edges_remaining_spec + (>> (fun E => Hexists C2 L2, hinv E C2 L2 \* \[ C2[i] = true ]) G). { auto. } { unfold hinv. intros. skip. (* eapply heap_contains_intro. (* evar context issues? *) skip. skip. *) } @@ -216,13 +238,11 @@ Proof. 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. } + applys~ inv_step_push i. } + { xrets. unfold hinv. hsimpl. now applys~ inv_step_skip j. auto. } } + { unfold hinv. hsimpl. apply~ inv_step_pop. } { rew_bool_eq~. } - { intros r'. hpull;=> C2 L2 ?. rewrite remove_all. hsimpl. } + { hsimpl. } { intros C2 L2. xapplys~ HS. } } { (* case loop end *) xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }