Commit b2981258 authored by charguer's avatar charguer
Browse files

DFS_progres

parent 6b75aae1
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
(at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
- xapp_rm
......
(*************************************************************************)
(** Graph representation by adjacency lists *)
......
......@@ -12,6 +12,10 @@ Ltac auto_star ::=
(********************************************************************)
(* ** TODO: Should be generated *)
......@@ -298,7 +302,7 @@ Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec.
Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i,
i \in nodes G ->
(forall j js, j \notin js -> has_edge G i j ->
(app f [j] (I js) (# I (\{j} \u js)))) ->
(app f [j] (g ~> RGraph G \* I js) (# g ~> RGraph G \* I (\{j} \u js)))) ->
app Graph_ml.iter_edges [f g i]
PRE (g ~> RGraph G \* I \{})
POST (# g ~> RGraph G \* I (out_edges G i)).
......@@ -321,12 +325,6 @@ Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.
(*************************************************************************)
(** DFS *)
(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
(at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)
Definition inv G R C :=
(nodes_index G (length C))
/\ (forall r, r \in R -> C[r] = Black)
......@@ -342,16 +340,42 @@ Definition hinv G R C g c :=
\* \[ inv G R C ].
Lemma dfs_from_spec : forall G R C g c i,
i \in nodes G ->
C[i] = White ->
app dfs_from [g c i]
PRE (hinv G R C g c)
POST (# Hexists C', hinv G R C' g c
\* \[ C'[i] = Black
/\ evolution C C' ]).
\* \[ evolution C C' /\ C'[i] = Black ]).
Proof using.
xcf. skip.
skip_goal IH. hide IH. (* TODO: set up the decreasing measure *)
=> G R C0. =>> Hi Ci. xcf. unfold hinv. xpull ;=> HI.
xapps~.
xfun as f.
set (loop_inv := fun L C => c ~> Array C
\* \[ inv G R C /\ evolution C0 C /\ no_white_in L C ]).
xseq. xapp_no_simpl (>> (fun L => Hexists C, loop_inv L C) G).
{ auto. }
{ => j js Hj Eij. unfold loop_inv.
xpull ;=> C (H1&H2&H3). xapp. clears f.
xapps~. xapps~. xpolymorphic_eq.
xpost (Hexists C', g ~> RGraph G \* c ~> Array C'
\* \[ inv G R C /\ evolution C0 C' /\ no_white_in js C' /\ C'[j] <> White ]).
{ xif.
{ show IH. xapply (>> IH G R C). skip. auto. unfold hinv. xsimpl~.
xpull ;=> C' (H1'&H2'). unfold hinv. xsimpl. splits.
auto.
applys* evolution_trans.
applys* no_white_in_evolution.
auto_false. }
{ xret. unfold hinv. xsimpl~. } }
{ xpull ;=> C' (H1'&H2'&H3'&H4'). xsimpl. splits.
{ skip. } (* TODO *)
{ auto. }
{ => k Hk. set_in Hk; auto. } } } (* trivial *)
{ unfold loop_inv. xsimpl. skip. } (* TODO *)
{ unfold loop_inv. xpull ;=> C' (F1&F2&F3). xapps~. xsimpl.
split. skip. skip. skip. } (* TODO *)
Qed.
Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec.
......@@ -368,11 +392,13 @@ Proof using.
xcf.
xapp. => Hn.
xapp. skip. => C0 HC0.
asserts N0: (no_gray C0). { subst. => i Hi. rew_arr; auto_false. }
xfun as f.
(* TODO: take the graph out of hinv *)
set (loop_inv := fun L C => hinv G (set_of_list L) C g c
\* \[ evolution C0 C /\ no_gray C /\ all_black_in (set_of_list L) C ]).
\* \[ evolution C0 C /\ all_black_in (set_of_list L) C ]).
xapp (fun L => Hexists C, loop_inv L C).
{ intros i L k HL. unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2&HC3).
{ intros i L k HL. unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2).
xapp. clears f.
xapps~.
xapps~. xpolymorphic_eq.
......@@ -383,12 +409,11 @@ Proof using.
{ unfold loop_inv. intros u. xpull ;=> C' (H1&H2). xsimpl.
{ auto_false. } (* trivial *)
{ splits. (* trivial *)
{ applys~ evolution_trans H2. } (* trivial *)
{ applys~ no_gray_evolution H2. } (* trivial *)
{ applys~ all_black_in_evolution H2. } } } } (* trivial *)
{ applys~ evolution_trans H1. } (* trivial *)
{ applys~ all_black_in_evolution H1. } } } } (* trivial *)
{ xret. unfold loop_inv, hinv. xsimpl~.
{ cases~ (C[i]). false. false* HC2. } } (* trivial *)
{ unfold loop_inv, hinv. => u. xpull ;=> C' HI' (H1&H2&H3) Hi.
{ cases~ (C[i]). false. false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } } (* trivial *)
{ unfold loop_inv, hinv. => u. xpull ;=> C' HI' (H1&H2) Hi.
rewrite set_of_list_last. xsimpl~.
{ splits~. { => j Rj. set_in Rj; auto. } } (* trivial *)
{ destruct HI' as (I1&I2&I3&I4). splits.
......@@ -399,18 +424,16 @@ Proof using.
{ unfold loop_inv, hinv. xsimpl.
{ split. (* trivial *)
{ hnfs*. } (* trivial *)
{ split. (* trivial *)
{ => j Hj. subst C0. rew_arr; auto_false. } (* trivial *)
{ => i Hi. false. } } } (* trivial *)
{ => i Hi. false. } } (* trivial *)
{ splits.
{ subst C0. rew_arr. hnf in Hn. skip. skip. } (* trivial *)
{ => r Hr. rewrite set_of_list_nil in Hr. false. } (* trivial *)
{ =>> Hi Ci. false. subst C0. rew_arr~ in Ci. false. } (* trivial *)
{ => i Hi Ci. false. subst C0. rew_arr~ in Ci. false. } } } (* trivial *)
unfold loop_inv, hinv. => C1. xpull ;=> (F1&F2&F3&F4) (H1&H2&H3).
unfold loop_inv, hinv. => C1. xpull ;=> (F1&F2&F3&F4) (H1&H2).
xret. xsimpl. split.
{ => M. applys~ F4. } (* trivial *)
{ => (r&Hr&Mr). applys* no_black_to_white_no_gray_elim. }
{ => (r&Hr&Mr). applys* no_black_to_white_no_gray_elim. applys* no_gray_evolution. }
Qed.
(* conclusion <-> reachables G (set_of_list r) (blacks C) *)
......
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