Commit 47f31aa8 authored by charguer's avatar charguer
Browse files

dFS_en_cours

parent b2981258
- xclose with args for the change.
(* 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.
*)
- xsimpl on I X ==> I Y produces X = Y.
- xapp_rm
......@@ -25,6 +30,7 @@ Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
MAJOR TODAY
MAJOR NEXT
......
......@@ -13,6 +13,101 @@ Ltac auto_star ::=
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* pred_le_extens. 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.
Lemma No_duplicates_app_inv : forall A (L1 L2 : list A),
No_duplicates (L1 ++ L2) ->
No_duplicates L1
/\ No_duplicates 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_ (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. set_in M; eauto. }
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 *.
......@@ -71,33 +166,44 @@ Definition reachable (G:graph) (i j:int) :=
(* ** Graph representation predicate *)
(** [nodes_index G n] holds if the nodes in [G] are indexed from
[0] inclusive to [n] exclusive. *)
(** [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) :=
forall i, i \in nodes G <-> index n i.
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
/\ No_duplicates (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)
/\ forall i j, i \in nodes G ->
Mem j (N[i]) = has_edge G i j].
\* \[ nodes_index G (LibListZ.length N)
/\ nodes_edges G N].
(********************************************************************)
Lemma RGraph_open : forall (g:loc) (G:graph),
g ~> RGraph G ==>
Hexists N, g ~> Array N
\* \[nodes_index G (LibListZ.length N)
/\ forall i j, i \in nodes G ->
Mem j (N[i]) = has_edge G i j].
/\ 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) ->
(forall i j, i \in nodes G -> Mem j (N[i]) = has_edge G i j) ->
nodes_edges G N ->
g ~> Array N
==>
g ~> RGraph G.
......@@ -112,8 +218,6 @@ Hint Extern 1 (RegisterClose (Array _)) =>
(********************************************************************)
(* ** Generic hints *)
......@@ -126,7 +230,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. introv N Nx L. subst. rewrite~ <- N. Qed.
Proof. unfold nodes_index. introv N Nx L. subst. rewrite~ <- N. Qed.
(*
Hint Resolve @index_array_length_eq @index_make @index_update.
......@@ -172,6 +276,12 @@ 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 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)).
(* 1 <-> (blacks C) \c (blacks C')
2 <-> (grays C) = (grays C') *)
......@@ -207,6 +317,17 @@ Proof using. (* trivial *)
rewrite~ H1. auto_false.
Qed.
Lemma no_white_in_evolution' : forall C C' X E,
no_white_in E C ->
evolution' X 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' ->
......@@ -242,46 +363,6 @@ Qed.
(*************************************************************************)
(** Set of list predicate : TODO: move *)
Definition set_of_list A (L : list A) :=
LibList.fold (monoid_ (union : _ -> _ -> set A) (\{}:set A)) (fun x => \{x}) L.
Section SetOfList.
Variables (A:Type).
Implicit Types l : list A.
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. skip. (* TODO *) Qed.
(*
Lemma fold_app : forall l1 l2,
Monoid m ->
fold m f (l1 ++ l2) = monoid_oper m (fold m f l1) (fold m f l2).
Proof using.
unfold fold. intros. rewrite fold_right_app. gen l2.
induction l1; intros.
repeat rewrite fold_right_nil. rewrite~ monoid_neutral_l.
repeat rewrite fold_right_cons. rewrite <- monoid_assoc. fequals.
Qed.
Lemma fold_last : forall x l,
Monoid m ->
fold m f (l & x) = monoid_oper m (fold m f l) (f x).
Proof using.
intros. rewrite~ fold_app. rewrite fold_cons.
rewrite fold_nil. rewrite monoid_neutral_r. auto.
Qed.
*)
End SetOfList.
(*************************************************************************)
(** Graph representation by adjacency lists *)
......@@ -299,38 +380,56 @@ Qed.
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,
i \in nodes G ->
(forall j js, j \notin js -> has_edge G i j ->
(app f [j] (g ~> RGraph G \* I js) (# g ~> RGraph G \* I (\{j} \u js)))) ->
(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 (g ~> RGraph G \* I \{})
POST (# g ~> RGraph G \* I (out_edges G i)).
PRE (I \{})
POST (# I (out_edges G i)).
Proof.
introv Gi Sf. xcf. xunfold RGraph. xpull ;=> N (GI&GN).
xapps~. xfun. xapp (fun (L:list int) => I (set_of_list L)).
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.
{ skip. (* needs no duplicate *) }
{ rewrite~ <- GN. rewrite EN. skip. (* mem *) }
{ 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. } }
{ xsimpl.
{ skip. (* set_of_list // out_edges *) }
{ split~. } }
{ 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 -> C[r] = Black)
(* /\ (forall r, r \in R -> r = i \/ C[r] = Black) *)
/\ (no_black_to_white G C)
/\ (forall i, i \in nodes G -> C[i] = Black -> exists r, r \in R /\ reachable G r i).
/\ (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). *)
......@@ -340,8 +439,40 @@ Definition hinv G R C g c :=
\* \[ inv G R C ].
(* NOT NEEDED
Lemma evolution_trans' : forall X, trans (evolution' X).
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. }
Qed.
*)
Lemma evolution_trans' : forall C2 X C1 C3,
evolution' X C1 C2 ->
evolution C2 C3 ->
evolution' X C1 C3.
Proof using. (* trivial *)
introv. =>> (F1&G1) (F2&G2). splits.
{ autos*. }
{ intros. rewrite~ <- G2. }
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.
Lemma dfs_from_spec : forall G R C g c i,
i \in nodes G ->
reachable_from G R i ->
C[i] = White ->
app dfs_from [g c i]
PRE (hinv G R C g c)
......@@ -349,37 +480,77 @@ Lemma dfs_from_spec : forall G R C g c i,
\* \[ evolution C C' /\ C'[i] = Black ]).
Proof using.
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 ]).
=> G R C0. =>> Ri Wi.
skip Hi: (i \in nodes G). (* TODO: exploit reachable => in nodes *)
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. }
{ => j js Hj Eij. unfold loop_inv.
xpull ;=> C (H1&H2&H3). xapp. clears f.
{ => L. unfold loop_inv, hinv. applys heap_contains_intro
(Hexists C, c ~> Array C \* \[ inv G R C] \* (* TODO: 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.
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 ]).
xpost (Hexists C', hinv G R C' g c
\* \[ evolution' \{i} 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. }
{ show IH. xapply (>> IH G R C).
{ destruct Ri as (r&Pr&Mr). exists r. split~. applys* reachable_trans_edge. } (* trivial *)
{ auto. }
{ unfold hinv. xsimpl~. }
unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits.
{ applys* evolution_trans'. }
{ applys* no_white_in_evolution. }
{ auto_false. } (* trivial *)
{ auto. } } (* trivial *)
{ 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 *)
{ unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits.
{ auto. } (* trivial *)
{ => k Hk. set_in Hk; auto. } (* trivial *)
{ auto. } } } (* trivial *)
{ clears f. unfold loop_inv, hinv. xsimpl. split.
{ split.
{ => j Hj Ej. rew_array~. case_if~. } (* trivial *)
{ => 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). 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. } } }
{ unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2).
xapps~. xsimpl. split.
{ destruct F1 as (E1&E2). split.
{ => j Hj Ej. rew_array~. case_if~. } (* trivial *)
{ => 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 *)
{ 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.
{ applys F2. rewrite~ out_edges_has_edge. }
{ applys* I2. } }
{ => j Hj. rew_array~. case_if; [|auto].
=> _. rename j into i. eauto. }
} }
Qed.
(* { exists r0. splits~. applys* reachable_trans_edge. } (* trivial *) =>> Hi (r0&Rr0&Ri) Ci. *)
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)
......@@ -389,23 +560,31 @@ 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. skip. => C0 HC0.
xcf. xapp. => Hn.
xapp. { applys (proj1 Hn). } (* trivial *)
=> 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 /\ 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).
{ => i L k 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 (set_of_list L) C.
{ auto. } (* trivial *)
{ unfold hinv. xsimpl*. } (* trivial *)
{ xapp (\{i} \u set_of_list L) C.
{ 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 *)
......@@ -442,7 +621,8 @@ 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