Set Implicit Arguments. Require Import CFML.CFLib. Require Import DFS_ml. Require Import Stdlib. Require Import TLC.LibListZ. Require Import Array_proof. Require Import List_proof. Open Scope tag_scope. 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. Global Instance incl_inst : BagIncl hprop. Proof. constructor. applys heap_contains. Defined. Lemma heap_contains_intro : forall (H H1 H2 : hprop), (H2 ==> H1 \* H) -> (H1 \* H ==> H2) -> (H1 \c H2). Proof using. introv M1 M2. hnf. exists H. apply* antisym_pred_incl. Qed. Lemma heap_contains_elim : forall (H1 H2 : hprop), (H1 \c H2) -> exists H, (H2 ==> H1 \* H) /\ (H1 \* H ==> H2). Proof using. introv (H&M). exists H. split*. Qed. Global Opaque heap_contains. (* Search noduplicates. Lemma noduplicates_app_inv : forall A (L1 L2 : list A), noduplicates (L1 ++ L2) -> noduplicates L1 /\ noduplicates L2 /\ (~ exists x, mem x L1 /\ mem x L2). Proof using. introv ND. splits. induction L1. constructors. rew_list in ND. inverts ND as ND1 ND2. rewrite mem_app_or_eq in ND1. rew_logic* in ND1. induction L1. rew_list~ in ND. rew_list in ND. inverts~ ND. introv (x&I1&I2). induction I1; rew_list in ND. inverts ND as ND1 ND2. false ND1. apply* mem_app_or. apply IHI1. inverts~ ND. Qed. *) (*************************************************************************) (** Set of list predicate : TODO: move *) Definition set_of_list_monoid A := (monoid_make (union : _ -> _ -> set A) (\{}:set A)). Definition set_of_list A (L : list A) := LibList.fold (@set_of_list_monoid A) (fun x => \{x}) L. Section SetOfList. Variables (A:Type). Implicit Types l : list A. Lemma set_of_list_monoid_Monoid : Monoid (set_of_list_monoid A). Proof using. unfold set_of_list_monoid. constructor. apply union_assoc. apply union_empty_l. apply union_empty_r. Qed. Local Hint Resolve set_of_list_monoid_Monoid. Lemma set_of_list_nil : set_of_list (@nil A) = \{}. Proof using. auto. Qed. Lemma set_of_list_cons : forall x l, set_of_list (x::l) = \{x} \u (set_of_list l). Proof using. intros. unfold set_of_list. rewrite~ fold_cons. Qed. Lemma set_of_list_last : forall x l, set_of_list (l&x) = (set_of_list l) \u \{x}. Proof using. intros. unfold set_of_list. rewrite~ fold_last. Qed. Lemma set_of_list_app : forall l1 l2, set_of_list (l1 ++ l2) = (set_of_list l1) \u (set_of_list l2). Proof using. intros. unfold set_of_list. rewrite~ fold_app. Qed. Lemma set_of_list_mem : forall l x, x \in set_of_list l -> mem x l. Proof using. introv. induction l; introv M. { false. } { rewrite set_of_list_cons in M. rew_set in M. destruct* M. } Qed. End SetOfList. Hint Rewrite set_of_list_nil set_of_list_cons set_of_list_app set_of_list_last : rew_set_of_list. Tactic Notation "rew_set_of_list" := autorewrite with rew_set_of_list. Tactic Notation "rew_set_of_list" "in" hyp(M) := autorewrite with rew_set_of_list in M. Tactic Notation "rew_set_of_list" "in" "*" := autorewrite with rew_set_of_list in *. (********************************************************************) (* ** TODO: Should be generated *) Instance color__inhab : Inhab color_. Proof. typeclass. Qed. (********************************************************************) (********************************************************************) (* START HERE *) (********************************************************************) (********************************************************************) (* ** Representation of graphs without information on the edges *) (** Axiomatization of a graph structure *) Parameter graph : Type. Parameter nodes : graph -> set int. Parameter edges : graph -> set (int*int). Parameter edges_in_nodes : forall (G : graph) x y, (x,y) \in edges G -> x \in nodes G /\ y \in nodes G. (** Derived definition for working with graphs *) Definition out_edges G i := set_st (fun j => (i,j) \in edges G). Definition has_edge (G:graph) x y := (x,y) \in edges G. Definition path := list (int*int). Inductive is_path (G:graph) : int -> int -> path -> Prop := | is_path_nil : forall x, x \in nodes G -> is_path G x x nil | is_path_cons : forall x y z p, has_edge G x y -> is_path G y z p -> is_path G x z ((x,y)::p). Definition reachable (G:graph) (i j:int) := exists p, is_path G i j p. (********************************************************************) (* ** Basic well-formedness facts on graphs *) Lemma out_edges_has_edge : forall G i j, j \in out_edges G i <-> has_edge G i j. Proof using. intros. unfold has_edge, out_edges. rewrite* in_set_st_eq. Qed. Lemma has_edge_nodes : forall (G : graph) x y, has_edge G x y -> x \in nodes G /\ y \in nodes G. Proof using. =>> M. rewrite <- out_edges_has_edge in M. applys* edges_in_nodes. Qed. 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. 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 in Separation Logic: [g ~> RGraph G]*) (** [nodes_index G n] asserts that the nodes in [G] are indexed from [0] inclusive to [n] exclusive. *) Definition nodes_index (G:graph) (n:int) := n >= 0 /\ (forall i, i \in nodes G <-> index n i). (** [nodes_edges G N] asserts that [N] describes the adjacency lists of [G], in the sense that [N[i]] gives the list of neighbors of node [i] in [G]. *) Definition nodes_edges (G:graph) (N:list(list int)) := forall i, i \in nodes G -> set_of_list (N[i]) = out_edges G i /\ noduplicates (N[i]). (** [g ~> RGraph G] asserts that at pointer [g] is an imperative array of pure lists that represents the adjacency lists of [G]. *) Definition RGraph (G:graph) (g:loc) := Hexists N, g ~> Array N \* \[ 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 ==> Hexists N, g ~> Array N \* \[nodes_index G (LibListZ.length N) /\ nodes_edges G N]. Proof using. intros. xunfolds~ RGraph. Qed. Lemma RGraph_close : forall (g:loc) (G:graph) N, nodes_index G (LibListZ.length N) -> nodes_edges G N -> g ~> Array N ==> g ~> RGraph G. Proof using. intros. xunfolds~ RGraph. Qed. Arguments RGraph_close : clear implicits. Hint Extern 1 (RegisterOpen (RGraph _)) => Provide RGraph_open. Hint Extern 1 (RegisterClose (Array _)) => Provide RGraph_close. (********************************************************************) (* ** Generic hints *) (** Hints for type-checking *) 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 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 nodes_index_index; [ try eassumption | instantiate; try eassumption | instantiate; try congruence ]. *) (*************************************************************************) (** Verification of the Graph module, with the adjacency lists representation *) 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 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_spec Sf. (* TODO: xapp *) { intros M. rewrite EN in GND. (* trivial *) lets (_&_&N3): noduplicates_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. rew_set; eauto. } (* trivial *) { 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. (********************************************************************) (* ** 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. Definition all_black_in E C := forall i, i \in E -> C[i] = Black. Definition no_gray C := forall i, index C i -> C[i] <> Gray. Definition no_black_to_white G C := forall i j, has_edge G i j -> C[i] = Black -> C[j] <> White. 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. (* trivial *) => C. splits*. Qed. Lemma evolution_trans : trans evolution. Proof using. (* trivial *) =>> (F1&G1) (F2&G2). unfolds evolution. splits. autos*. intros. rewrite~ G1. Qed. 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 *) =>> (E1&E2) Ci HN. split. { => j Hj Ej. rew_array~. case_if~. { apply~ E1. rew_array~. case_if~. } } { => j Hj. rew_array~. case_if. { subst. rename j into i. iff; auto_false. } { rewrite~ <- E2. rew_array~. case_if*. } } Qed. Lemma no_white_in_evolution : forall C C' E, no_white_in E C -> evolution C C' -> no_white_in E C'. 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. Lemma no_gray_evolution : forall C C', no_gray C -> evolution C C' -> no_gray C'. 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 -> no_gray C -> reachable G i j -> C[i] = Black -> C[j] = Black. Proof using. =>> HW HG (p&HP). induction HP; => Ci. (* trivial after induction *) { auto. } { applys IHHP. cases (C[y]). { false* HW. } { false* HG. } { auto. } } Qed. Lemma inv_empty : forall G n, nodes_index G n -> inv G \{} (make n White). Proof using. (* trivial *) =>> Hn. splits. { hnf in Hn. rew_array*. auto. (* TODO: fix tactic *) } { =>> Hi Ci. false. rew_array~ in Ci. false. } { => i Hi Ci. false. rew_array~ in Ci. false. } Qed. 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 *) =>> (I1&I2&I3). splits. { auto. } { auto. } { => j Hj Cj. forwards~ (r&Hr&Pr): I3 j. exists* r. splits*. rew_set. eauto. (* TODO: tactic *) } Qed. 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 *) =>> Ci Hi (I1&I2&I3). splits. { rew_array~. } { => j k Hjk. rew_array~. => Cjk. case_if; auto_false. case_if. applys* I2. } { => j Hj. rew_array~. case_if; auto_false. } Qed. 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_array~. } { => j k Hjk. rew_array~. => M. case_if; auto_false. case_if. { subst. applys Wi. rewrite~ out_edges_has_edge. } { applys* I2. } } { => j Hj. rew_array~. case_if; [subst|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 -> app dfs_from [g c i] PRE (hinv G R C g c) 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 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 *) xcf. unfold hinv. xpull ;=> HI. xapps~. sets_eq C1: (C0[i:=Gray]). xfun as f. set (loop_inv := fun L C => hinv G R C g c \* \[ evolution C1 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] \* (* ideally, should be computed *) \[ evolution C1 C /\ no_white_in L C]); xsimpl~. } { => j js Hj Eij. unfold loop_inv, hinv. xpull ;=> C I0 (H1&H2). xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xpost (Hexists C', hinv G R C' g c \* \[ evolution C1 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~. (* 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. } (* trivial *) { auto_false. } (* trivial *) { auto. } } (* trivial *) { xret. unfold hinv. xsimpl~. } } { unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits. { auto. } (* trivial *) { => k Hk. rew_set in Hk. destruct~ Hk. subst~. } (* trivial *) { auto. } } } (* trivial *) { clears f. unfold loop_inv, hinv. xsimpl. split. { applys evolution_refl. } { => j Hj. rew_array~. } (* trivial *) { subst C1. applys* inv_gray_root. } } { unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2). xapps~. xsimpl. split. { subst C1. applys* evolution_write_black. } { rew_array~. case_if~. } (* trivial *) { applys* inv_evolution_black. } } Qed. Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec. Lemma dfs_main_spec : forall (G:graph) g (rs:list int), app dfs_main [g rs] PRE (g ~> RGraph G) POST (fun c => Hexists C, c ~> Array C \* g ~> RGraph G \* \[ forall i, i \in nodes G -> (C[i] = Black <-> exists r, r \in set_of_list rs /\ reachable G r i)]). Proof using. xcf. xapp. => Hn. xapp. { applys (proj1 Hn). } (* trivial *) => C0 HC0. asserts N0: (no_gray C0). { subst. => i Hi. rew_array; auto_false. } (* trivial *) xfun as f. 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 T HL. lets (_&Hi): (proj2 Hn) i. unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2). xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif. { xapp G (\{i} \u set_of_list L) C. { exists i. split. { rew_set; eauto. } (* TODO: tactic *) { applys* reachable_self. } } (* trivial *) { auto. } (* 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. rew_set in Hj. destruct Hj. (* trivial *) { applys~ (proj1 F1). } { subst~. } } } (* trivial *) { rewrite~ union_comm. } } } (* trivial *) { xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split. { auto. } (* trivial *) { => j Hj. rew_set in Hj. destruct Hj. { cases (C[i]); auto_false. } (* trivial *) { subst. cases (C[i]); auto_false. (* TODO: cleanup here *) false~ N0 i. forwards* (_&?): (proj2 HC1). } } (* trivial *) { cases~ (C[i]). (* trivial *) { false. } (* trivial *) { false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } (* trivial *) { rewrite~ union_comm. applys* inv_add_root. } } } } { unfold loop_inv, hinv. rew_set_of_list. xsimpl. split. { applys* evolution_refl. } (* trivial *) { => r Hr. rew_set in Hr. 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 *) { => (r&Hr&Mr). applys* no_black_to_white_no_gray_elim. applys* no_gray_evolution. } Qed. Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.