Commit 900ad9a8 by charguer

### DFS_cleanup

parent 0d728c6c
 ... ... @@ -12,6 +12,8 @@ Ltac auto_star ::= try solve [ subst; intuition eauto with maths ]. (*************************************************************************) (** Heap contains predicate : TODO: move *) Definition heap_contains H1 H2 := exists H, H2 = H1 \* H. ... ... @@ -106,11 +108,6 @@ Tactic Notation "rew_set_of_list" "in" "*" := autorewrite with rew_set_of_list in *. (********************************************************************) (* ** TODO: Should be generated *) ... ... @@ -119,6 +116,13 @@ Proof. typeclass. Qed. (********************************************************************) (********************************************************************) (* START HERE *) (********************************************************************) (********************************************************************) (* ** Representation of graphs without information on the edges *) ... ... @@ -188,10 +192,41 @@ 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. Lemma reachable_self : forall G i, i \in nodes G -> reachable G i i. Proof using. intros. exists (nil:path). constructor~. Qed. Lemma reachable_edge : forall G i j, has_edge G i j -> reachable G i j. Proof using. (* trivial *) =>> M. exists ((i,j)::nil). constructor~. constructor~. applys* has_edge_in_nodes_r. Qed. Lemma reachable_trans : forall G i j k, reachable G i j -> reachable G j k -> reachable G i k. Proof using. (* basic induction *) =>> (p1&M1) (p2&M2). exists (p1++p2). induction M1; rew_list. { auto. } { constructor~. } Qed. Lemma reachable_trans_edge : forall G i j k, reachable G i j -> has_edge G j k -> reachable G i k. Proof using. (* trivial *) =>> M1 M2. applys* reachable_trans. applys* reachable_edge. Qed. (********************************************************************) (* ** Graph representation predicate *) (* ** Graph representation predicate in Separation Logic: [g ~> RGraph G]*) (** [nodes_index G n] asserts that the nodes in [G] are indexed from [0] inclusive to [n] exclusive. *) ... ... @@ -216,9 +251,9 @@ Definition RGraph (G:graph) (g:loc) := \* \[ nodes_index G (LibListZ.length N) /\ nodes_edges G N]. (********************************************************************) (********************************************************************) (** Basic lemmas about [RGraph] -- TODO: will be generated *) Lemma RGraph_open : forall (g:loc) (G:graph), g ~> RGraph G ==> ... ... @@ -243,81 +278,90 @@ Hint Extern 1 (RegisterClose (Array _)) => Provide RGraph_close. (********************************************************************) (* ** Generic hints *) (** Hints for lists *) (** Hints for type-checking *) Hint Constructors Forall. Hint Resolve Forall_last. Implicit Types G : graph. Implicit Types i j k : int. Implicit Types p : path. Implicit Types C : list color_. Implicit Types R E F : set int. (** Hints for indices *) Lemma graph_adj_index : forall (G:graph) n m x, Lemma nodes_index_index : forall G n m x, nodes_index G n -> x \in nodes G -> n = m -> index m x. Proof. introv (E&N) Nx L. subst. rewrite~ <- N. Qed. (* Hint Extern 1 (index ?n ?x) => skip. (* TODO: for now, we skip these trivial goals about indices being in the bounds of the array *) (* Hints for solving [index n x] goals automatically Hint Resolve @index_array_length_eq @index_make @index_update. Hint Immediate has_edge_in_nodes_l has_edge_in_nodes_r. Hint Extern 1 (nodes_index _ _) => congruence. Hint Extern 1 (index ?n ?x) => eapply graph_adj_index; eapply nodes_index_index; [ try eassumption | instantiate; try eassumption | instantiate; try congruence ]. *) Hint Extern 1 (nodes_index _ _) => skip. (* TODO *) Hint Extern 1 (index ?n ?x) => skip. (* TODO *) (********************************************************************) (* ** Facts *) (*************************************************************************) (** Verification of the Graph module, with the adjacency lists representation *) Implicit Types G : graph. Implicit Types i j k : int. Implicit Types p : path. Implicit Types C : list color_. Implicit Types R E F : set int. Lemma nb_nodes_spec : forall (G:graph) g, app Graph_ml.nb_nodes [g] PRE (g ~> RGraph G) POST (fun n => g ~> RGraph G \* \[nodes_index G n]). Proof using. xcf. xunfold RGraph. xpull ;=> N (HN1&HN2). xapp. xsimpl*. Qed. Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec. Lemma reachable_edge : forall G i j, has_edge G i j -> reachable G i j. Proof using. =>> M. exists ((i,j)::nil). constructor~. constructor~. applys* has_edge_in_nodes_r. Qed. Lemma reachable_trans : forall G i j k, reachable G i j -> reachable G j k -> reachable G i k. Proof using. =>> (p1&M1) (p2&M2). exists (p1++p2). induction M1; rew_list. { auto. } { constructor~. } Qed. Lemma iter_edges_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) (# I (\{j} \u E)))) -> app Graph_ml.iter_edges [f g i] PRE (I \{}) POST (# I (out_edges G i)). Proof. introv Gi Ginc Sf. xcf. forwards (H&HO&HC): heap_contains_elim ((rm Ginc) \{}). xchange (rm HO). xopen g. xpull ;=> N (GI&GN). forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC). xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)). { introv EN. rewrite set_of_list_last. xapp. xapp. { intros M. rewrite EN in GND. (* trivial *) lets (_&_&N3): No_duplicates_app_inv GND. applys (rm N3). (* trivial *) exists x. forwards*: set_of_list_Mem M. } (* trivial *) { rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN. (* trivial *) rew_set_of_list. eauto. } (* trivial *) { xsimpl. } { rewrite union_comm. xsimpl. } } { rew_set_of_list. xsimpl. } { rewrite GNE. xsimpl. } Qed. Definition evolution C C' := (forall i, index C i -> C[i] = Black -> C'[i] = Black) /\ (forall i, index C i -> (C[i] = Gray <-> C'[i] = Gray)). Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec. Definition evolution' (X:set int) C C' := (forall i, index C i -> C[i] = Black -> C'[i] = Black) /\ (forall i, index C i -> ((C[i] = Gray \/ i \in X) <-> C'[i] = Gray)). (* EASIER: consider evolution wrt C[i:=Gray] *) (* 1 <-> (blacks C) \c (blacks C') 2 <-> (grays C) = (grays C') *) (********************************************************************) (* ** Auxiliary definitions for the invariants of DFS *) Definition evolution C C' := (forall i, index C i -> C[i] = Black -> C'[i] = Black) /\ (forall i, index C i -> (C[i] = Gray <-> C'[i] = Gray)). Definition no_white_in E C := forall i, i \in E -> C[i] <> White. ... ... @@ -334,16 +378,30 @@ 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 *) *) Definition reachable_from G R i := exists r, r \in R /\ reachable G r i. Definition inv G R C := (nodes_index G (length C)) /\ (no_black_to_white G C) /\ (forall j, j \in nodes G -> C[j] = Black -> reachable_from G R j). (* TODO: above, might need to maintain that [R \c nodes G] in order to prove facts of the form [r \in nodes G] *) Definition hinv G R C g c := g ~> RGraph G \* c ~> Array C \* \[ inv G R C ]. (********************************************************************) (* ** Auxiliary lemmas *) Lemma evolution_refl : refl evolution. Proof using. => C. splits*. Qed. (* trivial *) Proof using. (* trivial *) => C. splits*. Qed. Lemma evolution_trans : trans evolution. Proof using. (* trivial *) ... ... @@ -352,21 +410,23 @@ Proof using. (* trivial *) intros. rewrite~ G1. Qed. Lemma no_white_in_evolution : forall C C' E, no_white_in E C -> evolution C C' -> no_white_in E C'. Lemma evolution_write_black : forall G i C C', evolution (C[i := Gray]) C' -> C[i] = White -> no_white_in (out_edges G i) C' -> evolution C C'[i := Black]. Proof using. (* trivial *) =>> N (H1&H2) i Hi. cases (C[i]) as Ci. { false* N. } { forwards~ (H2a&_): H2 i. rewrite~ H2a. auto_false. } rewrite~ H1. auto_false. Qed. =>> (E1&E2) Ci HN. split. { => j Hj Ej. rew_array~. case_if~. { apply~ E1. rew_array~. case_if~. } } { => j Hj. rew_array~. case_if. { rename j into i. iff; auto_false. } { rewrite~ <- E2. rew_array~. case_if*. } } Qed. (* NOT USED Lemma no_white_in_evolution' : forall C C' X E, Lemma no_white_in_evolution : forall C C' E, no_white_in E C -> evolution' X C C' -> evolution C C' -> no_white_in E C'. Proof using. (* trivial *) =>> N (H1&H2) i Hi. cases (C[i]) as Ci. ... ... @@ -374,13 +434,14 @@ 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 -> evolution C C' -> no_gray C'. Proof using. =>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i. Qed. (* trivial *) Proof using. (* trivial *) =>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i. Qed. Lemma no_black_to_white_no_gray_elim : forall G C i j, no_black_to_white G C -> ... ... @@ -398,119 +459,58 @@ Proof using. { auto. } } Qed. (* 2 <-> grays C = \{} 5 <-> i \in blacks C 6 <-> j \notin white C <-> j \in (blacks C \u grays C) *) (*************************************************************************) (** Graph representation by adjacency lists *) (* Import Graph_ml. *) Lemma nb_nodes_spec : forall (G:graph) g, app Graph_ml.nb_nodes [g] PRE (g ~> RGraph G) POST (fun n => g ~> RGraph G \* \[nodes_index G n]). Proof using. (* TODO: app_keep *) xcf. xunfold RGraph. xpull ;=> N (HN1&HN2). xapp. xsimpl*. Lemma inv_empty : forall G n, nodes_index G n -> inv G \{} (make n White). Proof using. (* trivial *) =>> Hn. splits. { hnf in Hn. rew_arr*. } { =>> Hi Ci. false. rew_arr~ in Ci. false. } { => i Hi Ci. false. rew_arr~ in Ci. false. } Qed. 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 L, (g ~> RGraph G) \c (I L)) -> (forall j E, j \notin E -> has_edge G i j -> (app f [j] (I E) (# I (\{j} \u E)))) -> app Graph_ml.iter_edges [f g i] PRE (I \{}) POST (# I (out_edges G i)). Proof. introv Gi Ginc Sf. xcf. forwards (H&HO&HC): heap_contains_elim ((rm Ginc) \{}). xchange (rm HO). xopen g. xpull ;=> N (GI&GN). forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC). xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)). { introv EN. rewrite set_of_list_last. xapp. xapp. { intros M. rewrite EN in GND. (* trivial *) lets (_&_&N3): No_duplicates_app_inv GND. applys (rm N3). (* trivial *) exists x. forwards*: set_of_list_Mem M. } (* trivial *) { rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN. (* trivial *) rew_set_of_list. eauto. } (* trivial *) { xsimpl. } { rewrite union_comm. xsimpl. } } { rew_set_of_list. xsimpl. } { rewrite GNE. xsimpl. } Qed. Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec. (*************************************************************************) (** DFS *) Definition reachable_from G R i := exists r, r \in R /\ reachable G r i. Definition inv G R C := (nodes_index G (length C)) (* /\ (forall r, r \in R -> r = i \/ C[r] = Black) *) /\ (no_black_to_white G C) /\ (forall j, j \in nodes G -> C[j] = Black -> reachable_from G R j). (* TODO: need to maintain that R \c nodes G *) (* 2 <-> R \c (blacks C) 4 <-> reachables G R (blacks C). *) Definition hinv G R C g c := g ~> RGraph G \* c ~> Array C \* \[ inv G R C ]. (* NOT NEEDED Lemma evolution_trans' : forall X, trans (evolution' X). Lemma inv_add_root : forall G L C i, inv G (set_of_list L) C -> inv G ('{i} \u set_of_list L) C. Proof using. (* trivial *) intros X. =>> (F1&G1) (F2&G2). unfolds evolution'. splits. autos*. intros. iff M. { rewrite~ <- G2. destruct~ M. left. rewrite~ <- G1. } { rewrite~ <- G2 in M. destruct~ M as [M|M]. rewrite~ <- G1 in M. } =>> (I1&I2&I3). splits. { auto. } { auto. } { => j Hj Cj. forwards~ (r&Hr&Pr): I3 j. exists* r. } Qed. *) Lemma evolution_trans' : forall C2 X C1 C3, evolution' X C1 C2 -> evolution C2 C3 -> evolution' X C1 C3. Lemma inv_gray_root : forall G R C i, C[i] = White -> i \in nodes G -> inv G R C -> inv G R (C[i := Gray]). Proof using. (* trivial *) introv. =>> (F1&G1) (F2&G2). splits. { autos*. } { intros. rewrite~ <- G2. } =>> Ci Hi (I1&I2&I3). splits. { rew_arr~. } { => j k Hjk. rew_array~. => Cjk. case_if; auto_false. case_if. applys* I2. } { => j Hj. rew_array~. case_if; auto_false. } Qed. Lemma reachable_trans_edge : forall G i j k, reachable G i j -> has_edge G j k -> reachable G i k. Proof using. (* trivial *) =>> M1 M2. applys* reachable_trans. applys* reachable_edge. Lemma inv_evolution_black : forall G R C' i, inv G R C' -> reachable_from G R i -> no_white_in (out_edges G i) C' -> inv G R (C'[i := Black]). Proof using. (* trivial *) =>> (I1&I2&I3) Ri Wi. splits. { rew_arr~. } { => j k Hjk. rew_array~. => M. case_if; auto_false. case_if. { applys Wi. rewrite~ out_edges_has_edge. } { applys* I2. } } { => j Hj. rew_array~. case_if; [|auto]. => _. rename j into i. eauto. } Qed. (*************************************************************************) (** Verification of DFS *) Lemma dfs_from_spec : forall G R C g c i, reachable_from G R i -> C[i] = White -> ... ... @@ -519,7 +519,7 @@ Lemma dfs_from_spec : forall G R C g c i, POST (# Hexists C', hinv G R C' g c \* \[ evolution C C' /\ C'[i] = Black ]). Proof using. skip_goal IH. hide IH. (* TODO: set up the decreasing measure *) skip_goal IH. hide IH. (* TODO: set up the decreasing measure to prove termination *) => G R C0. =>> Ri Wi. asserts Hi: (i \in nodes G). { destruct Ri as (r&Hr&Mr). applys* reachable_in_nodes_r. } (* trivial *) ... ... @@ -554,47 +554,17 @@ Proof using. { auto. } } } (* trivial *) { clears f. unfold loop_inv, hinv. xsimpl. split. { applys evolution_refl. } (* { split. { auto. (* => j Hj Ej. rew_array~. case_if~. *) } (* trivial *) { autos* => j Hj. rew_array~. iff M. (* trivial *) { case_if. auto. destruct M as [M|M]; auto_false. } (* trivial *) { case_if; eauto. } } } (* trivial *) *) { => j Hj. rew_array~. } (* trivial *) { destruct HI as (I1&I2&I3). subst C1. splits. { rew_arr~. } (* trivial *) (* { => r Hr. specializes I2 Hr. rew_array~. case_if; auto_false. } *) { => j k Hjk. rew_array~. => Cjk. case_if; auto_false. (* trivial *) case_if. applys* I2. } (* trivial *) { => j Hj. rew_array~. case_if; auto_false. } } } { subst C1. applys* inv_gray_root. } } { unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2). xapps~. xsimpl. split. { subst C1. destruct F1 as (E1&E2). split. (* trivial *) { => j Hj Ej. rew_array~. case_if~. { apply~ E1. rew_array~. case_if~. } } { => j Hj. rew_array~. case_if. (* trivial *) { rename j into i. iff; auto_false. } (* trivial *) { rewrite~ <- E2. rew_array~. case_if*. } } } (* trivial *) { subst C1. applys* evolution_write_black. } { rew_arr~. } (* trivial *) { 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. (* 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 *) } } { applys* inv_evolution_black. } } Qed. Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec. Lemma reachable_self : forall G i, i \in nodes G -> reachable G i i. Proof using. intros. exists (nil:path). constructor~. Qed. Lemma dfs_main_spec : forall (G:graph) g (rs:list int), app dfs_main [g rs] PRE (g ~> RGraph G) ... ... @@ -609,7 +579,6 @@ Proof using. => C0 HC0. asserts N0: (no_gray C0). { subst. => i Hi. rew_arr; auto_false. } (* trivial *) 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 /\ all_black_in (set_of_list L) C ]). xapp (fun L => Hexists C, loop_inv L C). ... ... @@ -619,19 +588,13 @@ Proof using. { xapp G (\{i} \u set_of_list L) C. { exists i. split~. applys* reachable_self. } (* trivial *) { auto. } (* trivial *) { unfold hinv. xsimpl*. destruct HI as (I1&I2&I3). splits. { auto. } (* trivial *) { auto. } (* trivial *) { => j Hj Cj. forwards~ (r&Hr&Pr): I3 j. exists* r. } } (* trivial *) { unfold hinv. xsimpl*. applys* inv_add_root. } { 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 *) { 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 *) ... ... @@ -639,18 +602,11 @@ Proof using. { 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 *) { rewrite~ union_comm. applys* inv_add_root. } } } } { unfold loop_inv, hinv. rew_set_of_list. xsimpl. split. { applys* evolution_refl. } (* trivial *) { => r Hr. set_in Hr. } (* trivial *) { 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 *) { subst C0. applys* inv_empty. } } (* trivial *) unfold loop_inv, hinv. => C1. xpull ;=> (I1&I2&I3) (H1&H2). xret. xsimpl. split. { => M. applys~ I3. } (* trivial *) ... ... @@ -658,19 +614,10 @@ Proof using. applys* no_gray_evolution. } Qed.