Commit 3bc99621 by charguer

### dfs_cleanup

parent 5896a12b
 ... ... @@ -7,12 +7,12 @@ Require Import Array_proof. Require Import List_proof. Open Scope tag_scope. Ltac auto_star ::= try solve [ subst; intuition eauto with maths ]. Definition heap_contains H1 H2 := exists H, H2 = H1 \* H. ... ... @@ -119,22 +119,26 @@ Proof. typeclass. Qed. (********************************************************************) (* ** TLC Graph without information on edges *) (* ** 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 out_edges : graph -> int -> set 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. Parameter has_edge_nodes : forall (G : graph) x y, has_edge G x y -> x \in nodes G /\ y \in nodes G. Definition path := list (int*int). Inductive is_path (G:graph) : int -> int -> path -> Prop := ... ... @@ -152,7 +156,19 @@ Definition reachable (G:graph) (i j:int) := (********************************************************************) (* ** Useful facts *) (* ** 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 *) ... ... @@ -173,10 +189,10 @@ Lemma reachable_in_nodes_r : forall (G : graph) x y, Proof using. =>> (p&M). induction* M. Qed. (********************************************************************) (* ** Graph representation predicate *) (** [nodes_index G n] asserts that the nodes in [G] are indexed from [0] inclusive to [n] exclusive. *) ... ... @@ -200,7 +216,6 @@ Definition RGraph (G:graph) (g:loc) := \* \[ nodes_index G (LibListZ.length N) /\ nodes_edges G N]. (********************************************************************) ... ... @@ -229,7 +244,11 @@ Hint Extern 1 (RegisterClose (Array _)) => (********************************************************************) (* ** Generic hints *) (** Hints for lists *) ... ... @@ -295,7 +314,7 @@ Definition evolution C C' := 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') *) ... ... @@ -405,8 +424,7 @@ Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec. Parameter out_edges_has_edge : forall G i j, j \in out_edges G i <-> has_edge G i j. Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i, ... ... @@ -505,19 +523,19 @@ Proof using. => 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~. xfun as f. set (loop_inv := fun L C => hinv G R C g c \* \[ evolution' \{i} C0 C /\ no_white_in L C ]). 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' \{i} C0 C /\ no_white_in L C]); xsimpl~. } \[ 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' \{i} C0 C' /\ no_white_in js C' /\ C'[j] <> White ]). \* \[ 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 *) ... ... @@ -525,7 +543,7 @@ Proof using. { auto. } (* trivial *) { unfold hinv. xsimpl~. } unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits. { applys* evolution_trans'. } { applys* evolution_trans. } { applys* no_white_in_evolution. } (* trivial *) { auto_false. } (* trivial *) { auto. } } (* trivial *) ... ... @@ -534,14 +552,16 @@ Proof using. { auto. } (* trivial *) { => k Hk. set_in Hk; auto. } (* trivial *) { auto. } } } (* trivial *) { clears f. unfold loop_inv, hinv. xsimpl. split. { clears f. unfold loop_inv, hinv. xsimpl. split. { applys evolution_refl. } (* { split. { => j Hj Ej. rew_array~. case_if~. } (* trivial *) { => j Hj. rew_array~. iff M. (* trivial *) { 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 *) { case_if; eauto. } } } (* trivial *) *) { => j Hj. rew_array~. } (* trivial *) { destruct HI as (I1&I2&I3). splits. { 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 *) ... ... @@ -549,11 +569,12 @@ 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. (* trivial *) { => j Hj Ej. rew_array~. case_if~. } (* trivial *) { 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. iff M. eauto. destruct M; auto_false. } } } (* trivial *) { rewrite~ <- E2. rew_array~. case_if*. } } } (* trivial *) { rew_arr~. } (* trivial *) { destruct I1 as (I1&I2&I3). splits. { rew_arr~. } (* trivial *) ... ... @@ -566,7 +587,6 @@ Proof using. } } Qed. (* { exists r0. splits~. applys* reachable_trans_edge. } (* trivial *) =>> Hi (r0&Rr0&Ri) Ci. *) Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec. ... ... @@ -584,10 +604,10 @@ Lemma dfs_main_spec : forall (G:graph) g (rs:list int), \[ 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 *) xcf. xapp. => Hn. xapp. { applys (proj1 Hn). } (* trivial *) => C0 HC0. asserts N0: (no_gray C0). { subst. => i Hi. rew_arr; auto_false. } 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 ... ... @@ -625,8 +645,8 @@ Proof using. { 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. } { 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 *) ... ... @@ -634,7 +654,8 @@ Proof using. 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. } { => (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!