Commit 5896a12b authored by charguer's avatar charguer
Browse files

DFS_ok

parent 47f31aa8
......@@ -135,15 +135,6 @@ Definition has_edge (G:graph) x y :=
Parameter has_edge_nodes : forall (G : graph) x y,
has_edge G x y -> x \in nodes G /\ y \in nodes G.
Lemma has_edge_in_nodes_l : forall (G : graph) x y,
has_edge G x y -> x \in nodes G.
Proof using. intros. forwards*: has_edge_nodes. Qed.
Lemma has_edge_in_nodes_r : forall (G : graph) x y,
has_edge G x y -> y \in nodes G.
Proof using. intros. forwards*: has_edge_nodes. Qed.
Definition path := list (int*int).
Inductive is_path (G:graph) : int -> int -> path -> Prop :=
......@@ -160,6 +151,26 @@ Definition reachable (G:graph) (i j:int) :=
(********************************************************************)
(* ** Useful facts *)
Lemma has_edge_in_nodes_l : forall (G : graph) x y,
has_edge G x y -> x \in nodes G. (* trivial *)
Proof using. intros. forwards*: has_edge_nodes. Qed.
Lemma has_edge_in_nodes_r : forall (G : graph) x y,
has_edge G x y -> y \in nodes G. (* trivial *)
Proof using. intros. forwards*: has_edge_nodes. Qed.
Lemma reachable_in_nodes_l : forall (G : graph) x y,
reachable G x y -> x \in nodes G.
Proof using.
=>> (p&M). destruct M. auto. applys* has_edge_in_nodes_l.
Qed.
Lemma reachable_in_nodes_r : forall (G : graph) x y,
reachable G x y -> y \in nodes G.
Proof using. =>> (p&M). induction* M. Qed.
(********************************************************************)
......@@ -230,7 +241,7 @@ Hint Resolve Forall_last.
Lemma graph_adj_index : forall (G:graph) n m x,
nodes_index G n -> x \in nodes G -> n = m -> index m x.
Proof. unfold nodes_index. introv N Nx L. subst. rewrite~ <- N. Qed.
Proof. introv (E&N) Nx L. subst. rewrite~ <- N. Qed.
(*
Hint Resolve @index_array_length_eq @index_make @index_update.
......@@ -261,7 +272,8 @@ Lemma reachable_edge : forall G i j,
has_edge G i j ->
reachable G i j.
Proof using.
skip.
=>> M. exists ((i,j)::nil). constructor~. constructor~.
applys* has_edge_in_nodes_r.
Qed.
Lemma reachable_trans : forall G i j k,
......@@ -269,7 +281,10 @@ Lemma reachable_trans : forall G i j k,
reachable G j k ->
reachable G i k.
Proof using.
skip.
=>> (p1&M1) (p2&M2). exists (p1++p2).
induction M1; rew_list.
{ auto. }
{ constructor~. }
Qed.
Definition evolution C C' :=
......@@ -300,11 +315,23 @@ Definition no_black_to_white G C :=
C[i] = Black ->
C[j] <> White.
(* NOT USED
Lemma all_black_in_evolution : forall C C' E,
all_black_in E C ->
evolution C C' ->
all_black_in E C'.
Proof using. =>> N (H1&H2) i Hi. auto. Qed. (* trivial *)
*)
Lemma evolution_refl : refl evolution.
Proof using. => C. splits*. Qed. (* trivial *)
Lemma evolution_trans : trans evolution.
Proof using. (* trivial *)
=>> (F1&G1) (F2&G2). unfolds evolution. splits.
autos*.
intros. rewrite~ G1.
Qed.
Lemma no_white_in_evolution : forall C C' E,
no_white_in E C ->
......@@ -317,6 +344,7 @@ Proof using. (* trivial *)
rewrite~ H1. auto_false.
Qed.
(* NOT USED
Lemma no_white_in_evolution' : forall C C' X E,
no_white_in E C ->
evolution' X C C' ->
......@@ -327,6 +355,7 @@ Proof using. (* trivial *)
{ forwards~ (H2a&_): H2 i. rewrite~ H2a. auto_false. }
rewrite~ H1. auto_false.
Qed.
*)
Lemma no_gray_evolution : forall C C',
no_gray C ->
......@@ -334,13 +363,6 @@ Lemma no_gray_evolution : forall C C',
no_gray C'.
Proof using. =>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i. Qed. (* trivial *)
Lemma evolution_trans : trans evolution.
Proof using. (* trivial *)
=>> (F1&G1) (F2&G2). unfolds evolution. splits.
autos*.
intros. rewrite~ G1.
Qed.
Lemma no_black_to_white_no_gray_elim : forall G C i j,
no_black_to_white G C ->
no_gray C ->
......@@ -481,14 +503,15 @@ Lemma dfs_from_spec : forall G R C g c i,
Proof using.
skip_goal IH. hide IH. (* TODO: set up the decreasing measure *)
=> G R C0. =>> Ri Wi.
skip Hi: (i \in nodes G). (* TODO: exploit reachable => in nodes *)
asserts Hi: (i \in nodes G).
{ destruct Ri as (r&Hr&Mr). applys* reachable_in_nodes_r. } (* trivial *)
xcf. unfold hinv. xpull ;=> HI. xapps~. xfun as f.
set (loop_inv := fun L C => hinv G R C g c
\* \[ evolution' \{i} C0 C /\ no_white_in L C ]).
xseq. xapp_no_simpl (>> (fun L => Hexists C, loop_inv L C) G).
{ auto. }
{ => L. unfold loop_inv, hinv. applys heap_contains_intro
(Hexists C, c ~> Array C \* \[ inv G R C] \* (* TODO: should be computed *)
(Hexists C, c ~> Array C \* \[ inv G R C] \* (* ideally, should be computed *)
\[ evolution' \{i} C0 C /\ no_white_in L C]); xsimpl~. }
{ => j js Hj Eij. unfold loop_inv, hinv.
xpull ;=> C I0 (H1&H2). xapp. clears f.
......@@ -497,12 +520,13 @@ Proof using.
\* \[ evolution' \{i} C0 C' /\ no_white_in js C' /\ C'[j] <> White ]).
{ xif.
{ show IH. xapply (>> IH G R C).
{ destruct Ri as (r&Pr&Mr). exists r. split~. applys* reachable_trans_edge. } (* trivial *)
{ auto. }
{ destruct Ri as (r&Pr&Mr). exists r. split~. (* trivial *)
applys* reachable_trans_edge. } (* trivial *)
{ auto. } (* trivial *)
{ unfold hinv. xsimpl~. }
unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits.
{ applys* evolution_trans'. }
{ applys* no_white_in_evolution. }
{ applys* no_white_in_evolution. } (* trivial *)
{ auto_false. } (* trivial *)
{ auto. } } (* trivial *)
{ xret. unfold hinv. xsimpl~. } }
......@@ -525,7 +549,7 @@ Proof using.
{ => j Hj. rew_array~. case_if; auto_false. } } }
{ unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2).
xapps~. xsimpl. split.
{ destruct F1 as (E1&E2). split.
{ destruct F1 as (E1&E2). split. (* trivial *)
{ => j Hj Ej. rew_array~. case_if~. } (* trivial *)
{ => j Hj. rew_array~. case_if. (* trivial *)
{ rename j into i. iff; auto_false. } (* trivial *)
......@@ -534,11 +558,11 @@ Proof using.
{ destruct I1 as (I1&I2&I3). splits.
{ rew_arr~. } (* trivial *)
(* { => r Hr. rew_array~. case_if~. } *)
{ => j k Hjk. rew_array~. => M. case_if; auto_false. case_if.
{ applys F2. rewrite~ out_edges_has_edge. }
{ applys* I2. } }
{ => j Hj. rew_array~. case_if; [|auto].
=> _. rename j into i. eauto. }
{ => j k Hjk. rew_array~. => M. case_if; auto_false. case_if. (* trivial *)
{ applys F2. rewrite~ out_edges_has_edge. } (* trivial *)
{ applys* I2. } } (* trivial *)
{ => j Hj. rew_array~. case_if; [|auto]. (* trivial *)
=> _. rename j into i. eauto. } (* trivial *)
} }
Qed.
......@@ -569,58 +593,55 @@ Proof using.
set (loop_inv := fun L C => hinv G (set_of_list L) C g c
\* \[ evolution C0 C /\ all_black_in (set_of_list L) C ]).
xapp (fun L => Hexists C, loop_inv L C).
{ => i L k HL. lets (_&Hi): (proj2 Hn) i.
{ => i L T HL. lets (_&Hi): (proj2 Hn) i.
unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2).
xapp. clears f.
xapps~.
xapps~. xpolymorphic_eq.
xpost (Hexists C', loop_inv L C' \* \[C'[i] = Black]). xif.
{ xapp (\{i} \u set_of_list L) C.
xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif.
{ xapp G (\{i} \u set_of_list L) C.
{ exists i. split~. applys* reachable_self. } (* trivial *)
{ auto. } (* trivial *)
{ exists i. split. eauto. applys* reachable_self. } (* trivial *)
{ auto. }
{ unfold hinv. xsimpl*. destruct HI as (I1&I2&I3&I4). splits.
{ auto. }
{ => r Hr. }
{ auto. }
} (* trivial *)
{ unfold loop_inv. intros u. xpull ;=> C' (H1&H2). xsimpl.
{ auto_false. } (* trivial *)
{ splits. (* trivial *)
{ applys~ evolution_trans H1. } (* trivial *)
{ applys~ all_black_in_evolution H1. } } } } (* trivial *)
{ xret. unfold loop_inv, hinv. xsimpl~.
{ 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.
{ unfold hinv. xsimpl*. destruct HI as (I1&I2&I3). splits.
{ auto. } (* trivial *)
{ => r Hr. set_in Hr; auto. } (* trivial *)
{ auto. } (* trivial *)
{ => j Hj Cj. forwards~ (r&?&?): I4 Cj. exists* r. } } } } (* trivial *)
{ unfold loop_inv, hinv. xsimpl.
{ split. (* trivial *)
{ hnfs*. } (* 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).
{ => j Hj Cj. . } } (* trivial *)
{ unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2).
rew_set_of_list. xsimpl.
{ splits. (* trivial *)
{ applys~ evolution_trans F1. } (* trivial *)
{ => j Hj. set_in Hj; eauto. applys~ (proj1 F1). } } (* trivial *)
{ destruct I1 as (I1&I2&I3). splits. (* trivial *)
{ auto. } (* trivial *)
{ auto. } (* trivial *)
{ rewrite~ union_comm. } } } } (* trivial *)
{ xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split.
{ auto. } (* trivial *)
{ => j Hj. set_in Hj; eauto. cases (C[i]); auto_false. (* trivial *)
false~ N0 i. forwards~ (_&?): (proj2 HC1). } (* trivial *)
{ cases~ (C[i]). (* trivial *)
{ false. } (* trivial *)
{ false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } (* trivial *)
{ (* todo: factorize as lemma *)
destruct HI as (I1&I2&I3). splits. (* trivial *)
{ auto. } (* trivial *)
{ auto. } (* trivial *)
{ => j Hj Cj. forwards~ (r&?&?): I3 Cj. exists* r. } } } } } (* trivial *)
{ unfold loop_inv, hinv. rew_set_of_list. xsimpl. split.
{ applys* evolution_refl. }
{ => r Hr. set_in Hr. }
{ splits.
{ subst C0. hnf in Hn. rew_arr*. } (* 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 ;=> (I1&I2&I3) (H1&H2).
xret. xsimpl. split.
{ => M. applys~ F4. } (* trivial *)
{ => M. applys~ I3. } (* trivial *)
{ => (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) *)
Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.
(*************************************************************************)
(** Alternative invariants *)
......
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